Os Métodos Formais são métodos utilizados para elaboração de sistemas computacionais, dando prioridade a sua coesão, porque existem softwares cujo área de atuação é crítica, tornando o processo de desenvolvimento bastante rigoroso, isto porque estes métodos são desenvolvidos a partir de princípios matemáticos que garantem a sua exatidão na capacidade de expressão das ideias vinculadas ao projeto de software. Assim, estes métodos ajudam a garantir uma maior correspondência entre o programa elaborado com a sua especificação. Um destes tipo de métodos é anotação formal B.

Fique por dentro das novidadas que a DevMedia lança para seus leitores da Revista Engenharia de Software e de seus cursos online de Engenharia de Software.

Notação B

A notação formal B foi desenvolvida em meados dos anos 80 pela Universidade de Oxford e trata-se de uma notação simples cuja principal aplicação era para especificação e desenvolvimento de APIs (Application Programming Interface). Em geral, a notação B é utilizada para as etapas de Especificação Formal, Refinamento e Geração de Código, já tendo sido aplicada em projetos de larga escala. Esta linguagem é estruturada nos seguintes fundamentos teóricos:


  • Lógica de Predicados: trata-se do uso de lógica matemática para estruturação de sentenças lógicas, fazendo uso de objetos, predicados, variáveis e quantificadores;
  • Teoria dos Conjuntos: é o estudo de conjuntos, elementos e suas relações. A linguagem da Teoria dos Conjuntos pode ser usada nas definições de quase todos os elementos matemáticos;
  • Aritmética de Inteiros: também conhecida como aritmética modular ou do relógio, fazendo uso de números inteiros que voltam ao seu valor inicial quando chegam em um determinado valor estabelecido como limite;
  • Notação de Máquina Abstrata: uso de modelo teórico de um sistema computacional de hardware ou software usado para detalhar o funcionamento do sistema.

A Figura 1 ilustra como ocorre o processo de desenvolvimento pela notação B. Como pode ser observado, a etapa de Especificação é utilizada para a criação da máquina abstrata do sistema que se deseja projetar. Após esta etapa, a máquina passa para a etapa de Refinamento, onde a máquina vai sendo mais detalhada em sua arquitetura, funcionalidades, processos e etc. Por último vem a fase final Implementação, onde são definidas estruturas algorítmicas referente as funcionalidades do sistema. Todas estas fases são criadas através das ferramentas de suporte ao desenvolvimento na notação B.

Processo
de desenvolvimento em notação B

Figura 1. Processo de desenvolvimento em notação B.

De um modo geral, a verificação da máquina pode ocorrer na própria etapa, na etapa de refinamento e na etapa de implementação (Figura 2). A verificação consiste em verificar a consistência das especificações e se as mesmas estão corretas. Estas verificações são realizadas sempre tendo como base a máquina em seu estado atual e comparando com o estado anterior. Na etapa de Refinamento podem ser realizadas vários refinamentos e a verificação na etapa de Implementação é sempre realizada comparando com o último refinamento realizado.

Funcionamento do procedimento de verificação nas etapas de desenvolvimento

Figura 2. Funcionamento do procedimento de verificação nas etapas de desenvolvimento.

Especificação

Na etapa de especificação é realizada a Elicitação dos Requisitos Funcionais sobre o que o sistema deverá fazer e as suas restrições. Nesta etapa deverá ser criada uma Máquina de Estados Abstrata. Esta máquina consiste em um modelo abstrato de como será o sistema, junto a sua estrutura interna e seus comportamentos. Esta máquina é composta de três itens:


  • Estados: consiste nos comportamentos do sistema mediante o resultado da análise das variáveis de estado frente a invariante;
  • Invariante: Consiste nos estados válidos do sistema e os predicados lógicos utilizados para sustentar e chegar nestes estados válidos, ou seja, são restrições que são impostas para o correto funcionamento do sistema;
  • Operações: Modificam ou consultam estados do sistema. São semelhantes a funcionalidades.

A Listagem 1 ilustra como é formada uma cláusula de uma máquina abstrata. Como pode ser observado, uma cláusula é composta dos componentes:


  • Machine: o nome da máquina abstrata;
  • Constraints: são as restrições e os tipos de elementos utilizados;
  • Sets: são os conjuntos de elementos utilizados;
  • Variables: são elementos comuns, conjuntos de elementos;
  • Invariant, que são predicados ou sentenças lógicas;
  • Initialisation: como a máquina abstrata estará em seu estado inicial;
  • Operations: são as operações realizadas nos estados da máquina.

Listagem 1. Cláusula de uma máquina de estados abstrata.

MACHINE <Nome da especificação> (Parâmetros) <devem ser passados parâmetros>
  CONSTRAINTS <tipagem e restrição aos valores dos parâmetros da máquina>
  SETS <definição de conjuntos>
  VARIABLES <definição das variáveis utilizadas (apenas nomes)>
  INVARIANT <definição dos predicados aplicados as variáveis (tipos das variáveis e suas restrições)>
  INITIALISATION <estabelece valores iniciais para as variáveis>
  OPERATIONS <definição das operações utilizadas>
  END

Substituições e Verificação

São conceitos utilizados pela notação B para provar o grau de correção de módulos. A Listagem 2 ilustra a definição de substituição, que consiste em realizar operações junto com as variáveis e verificar se os estados destas, de forma lógica, as regras estabelecidas pelos predicados.

Listagem 2. Definição de substituição.

Seja x uma variável, E uma expressão e F uma fórmula (predicado ou expressão), uma substituição é definida por:
  [x := E]F, que é a fórmula obtida ao substituirmos todas as ocorrências livres de x em F por E.
  OBS.: Uma variável é dita livre quando:
  1 - Está presente em uma fórmula.
  2 - Não está no escopo de um quantificador (∃ ou ∀), onde a variável quantificada é ela mesma.

Obrigações de Prova

Obrigações de Prova (OPs) são utilizadas para garantir a correção de um módulo com relação as invariantes quando ocorrem mudanças de estado na máquina que, por sua vez, deve iniciar em um estado válido, onde a inicialização deve estabelecer o invariante. As operações da máquina não deve levá-la em um estado inválido, assumindo que as suas pré-condições sejam respeitadas. Necessidade de gerar e cumprir de obrigações de prova. Estas obrigações de prova podem ser realizações em dois momentos:


  • Na inicialização: Onde os valores de inicialização das variáveis e demais objetos especificados, devem satisfazer as invariantes;
  • Na aplicação das operações: As operações devem preservar o invariante quando modificarem o estado da máquina.

Substituições Generalizadas

Consiste em uma extensão do conceito de substituições simples e faz parte da notação B e utilizada nas máquinas abstratas. Estas substituições podem ser:


  • Especificação: substituindo pré-condições e escolha não determinísticas;
  • Concretas: fazendo uso de sequências, laços condicionais, laços de loop e etc.

Refinamento

É a segunda etapa no processo de desenvolvimento em B. Consiste na transformação de uma máquina abstrata de um sistema em um modelo mais concreto para implementação. A etapa de Refinamento é útil para:


  • Remodelar dados;
  • Diminuir a distância entre especificação e implementação, por meio de verificação;
  • Definir uma versão mais concreta das substituições pela eliminação de pré-condições e eliminação ou diminuição de elementos não determinísticos;

O Refinamento é realizado em duas instâncias. Pelo Refinamento de dados, onde na invariante deve ser feita a relação entre a variável abstrata e a concreta. Pelo Refinamento de operações, pela não modificação das assinaturas das operações e não definir operações adicionais.

Na etapa de Refinamento também são realizadas as Obrigações de Prova para verificar a correção do refinamento com relação a máquina ou refinamento que se está acontecendo. Estas Obrigações de Prova podem ser realizadas de duas maneiras:


  • Inicialização: Todo possível estado de inicialização no refinamento que pode alcançar deve estar associado a um possível estado de inicialização que a máquina pode alcançar.
  • Operações: pela verificação de pré-condições mais fracas. Verificar se o modelo abstrato pode aplicar as operações da máquina, então o modelo concreto pode aplicar as operações do refinamento;

A Listagem 3 ilustra a definição de uma cláusula de refinamento, que pode ser aplicado a uma máquina ou a outro refinamento, onde devem ser definidas variáveis e as invariantes utilizadas nas obrigações de prova.

Listagem 3. Definição de uma cláusula para refinamento.

REFINEMENT <nome do refinamento>
  REFINES CMA <nome da qual o refinamento estará sendo aplicado. Se a uma máquina ou a outro refinamento>
  VARIABLES <Definição das variáveis>
  INVARIANT <Definição dos predicados>

Implementação

Consiste no último nível de refinamento. É a etapa a partir do qual é possível gerar código de linguagem de programação. Contudo possui apenas alguns tipos e substituições “implementáveis” em linguagem de programação como sequências, tipos inteiros, condicionais e etc.

A Listagem 4 ilustra definição de cláusulas de implementação. Como pode ser observado, em uma implementação deve ser especificada os parâmetros da máquina e o refinamento associado, importando os estados da máquina e inicializando as suas variáveis.

Listagem 4. Definição de uma cláusula de implementação.

IMPLEMENTATION <nome da implementação> (Parâmetros) <parâmetros da máquina> 
   
  REFINES <nome do refinamento>
  IMPORTS <Estados que devem ser encapsulados em outras máquinas>
  INVARIANT <restrições e tipos das variáveis>
  INITIALISATION <inicialização das variáveis>

Estudo de Caso

A seguir será descrito um breve estudo de caso de como se utilizar o método B para desenvolvimento de sistemas. Será tratado o problema do gerente de turmas.

O gerente de turmas precisa controlar os estudantes matriculados em uma determinada turma e registrar que os estudantes fazem os exercícios propostos em sala de aula. Dentre as observações e restrições estão que: um estudante pode deixar a classe a qualquer momento, mas só receberá um certificado se tiver feito todos os exercícios. Há um número máximo de estudantes que podem ser matriculados.

De acordo com o problema acima abordado, pode-se definir as seguintes instâncias:

  • Domínio do Problema: um conjunto de estudantes (ESTUDANTE);
  • Dois subconjuntos:
    o matriculado: todos os estudantes matriculados;
    o certificado: todos os estudantes matriculados que fizeram os exercícios;
  • tam_turma: tamanho máximo da turma (número de estudantes que podem ser matriculados).

Etapa de Especificação pela criação da Máquina de Estados Abstrata

A Listagem 5 a seguir ilustra como foi definido a Máquina de Estados Abstrata. Como pode ser observado, o nome da máquina é CMA, que corresponde as iniciais de Class Manager’s Assistant (Assistente de Gerenciamento de Classes). Essa máquina recebe os seguintes parâmetros:


  • tam_turma: controla o número máximo de matrículas na turma;
  • ESTUDANTE: conjunto universo de todos os estudantes.

Quanto as tipagens e restrição (Cláusula CONSTRAINTS) aos valores dos parâmetros da máquina, uma turma deve possuir alunos e o conjunto dos estudantes de ser finito. Como ilustrado, uma turma deve ter um número de alunos maior que 0 e os elementos contidos no conjunto estudante pertence ao conjunto dos números naturais e infinitos. Na cláusula VARIABLES são declaradas duas variáveis: matriculado e certificado, que serão utilizadas nas operações. Na cláusula INVARIANT são definidas as restrições sobre as variáveis declaradas e, como pode ser visto, os elementos da variável matriculado estão contidos no conjunto ESTUDANTE, assim como os elementos da variável certificado, e que os elementos contidos nela estão contidos dentro da variável matriculado e que a quantidade de elementos do conjunto formado pelo elementos da variável matriculado deve ser menor que a quantidade de elementos da turma. Já na cláusula INITIALISATION são definidos como as variáveis serão inicializadas. Neste caso, as variáveis matriculado e certificado foram inicializadas como conjuntos vazios.

Listagem 5. Ilustração da Máquina de Estados Abstrata.

MACHINE CMA (tam_turma, ESTUDANTE)
  CONSTRAINTS
              tam_turma > 0 ^  card(ESTUDANTE) ∈ N
  VARIABLES
              matriculado, certificado
  INVARIANT
              matriculado ⊆ ESTUDANTE ^
              certificado ⊆ ESTUDANTE ^
              certificado ⊆ matriculado ^
              card(matriculado) ≤ tam_turma
  INITIALISATION
              matriculado, certificado := ∅, ∅

Substituição, Obrigações de Prova

Substituições e obrigações de prova são utilizados para verificar a inicialização da máquina e vê se tudo está correto quando as proposições lógicas estabelecidas. As Listagens 6 e 7 ilustram como devem ser realizadas as operações de prova e as substituições, respectivamente.

Listagem 6. Ilustração das invariantes que serão verificadas.

Obrigação de prova ([S]I):
  [matriculado, certificado := ∅, ∅]
              (matriculado ⊆ ESTUDANTE ^
              certificado ⊆ ESTUDANTE ^
              certificado ⊆ matriculado ^
              card(matriculado) ≤ tam_turma)

Listagem 7. Ilustração das substituições que devem ser realizadas para verificação.

∅ ⊆ ESTUDANTE ^
  ∅ ⊆ ESTUDANTE ^
  ∅ ⊆ ∅ ^
  card(∅) ≤ tam_turma

Como operações que podem ser realizadas na máquina temos: matricular um estudante, certificar um estudante e consultar se um estudante está matriculado. A Listagem 8 ilustra a operação de matricular estudantes, que recebe como parâmetro uma variável. Como pode ser visto na listagem, as pré-condições são estabelecidas para que possa ser inserido o elemento no conjunto de matriculados na turma. Além disso é verificado se o elemento st existe no conjunto ESTUDANTE e, se o mesmo não está contido no conjunto dos estudantes matriculados e se a quantidade de elementos no conjunto matriculado é menor que o limite de alunos na turma, o elemento st é inserido no conjunto matriculado.

Listagem 8. Ilustração da operação matricular.

matricular(st) =
  PRE
       st ∈ ESTUDANTE ^
       st ∉ matriculado ^
       card(matriculado) < tam_turma
  THEN
        matriculado := matriculado ∪ {st}
  END

A Listagem 9 ilustra a operação certificar estudante, que recebe um elemento e verifica se o mesmo faz parte do conjunto dos estudantes matriculados. Caso não pertença ao conjunto dos estudantes certificados, o elemento st é adicionado ao conjunto dos estudantes certificados.

Listagem 9. Ilustração da operação certificar.

certificar(st) =
  PRE
           st ∈ matriculado ^
           st ∉ certificado
  THEN
           certificado := cetirficado ∪ {st}
  END

A Listagem 10 ilustra a operação de se verificar se um estudante está matriculado e recebe como parâmetro uma variável e que possui um valor de retorno para uma variável local chamada ans. Possui como pré-condição que o elemento pertença ao conjunto ESTUDANTE, sendo assim, verifica se o elemento st pertence ao conjunto matriculado: caso afirmativo retorna o valor TRUE, senão retorna FALSE.

Listagem 10. Ilustração da operação que verificar se o estudante está matriculado.

ans <-  estaMatriculado(st) =
  PRE
        st ∈ ESTUDANTE
  THEN
        IF
                st ∈ matriculado
        THEN
                ans := TRUE
         ELSE
                ans := FALSE
         END
  END

Etapa de Refinamento

Na etapa de refinamento é feito o detalhamento da máquina. Na Listagem 11 é ilustrada um refinamento para especificação de alunos que fizeram os exercícios. Na cláusula VARIABLES são declaradas duas variáveis:


  1. mat_r, utilizada para armazenar alunos matriculados
  2. ambos, utilizada para armazenar os alunos matriculados que fizeram exercícios.

Na cláusula INVARIANT são definidos que elementos nas variáveis mat_r e ambos, e devem estar contidos no conjunto ESTUDANTE. Além disso, os elementos na variável mat_r devem estar presentes na variável ambos e vice-versa. Assim, a relação de refinamento é que o conjunto matriculado deve ser a união entre o conjunto mat_r e ambos, e que o conjunto certificado recebe elementos da variável ambos.

Listagem 11. Refinamento da máquina.

REFINEMENT CMA_ref
  REFINES CMA
  VARIABLES
           mat_r, ambos
  INVARIANT
           mat_r ⊆ ESTUDANTE ^
           ambos ⊆ ESTUDANTE ^
           mat_r ∩ ambos = ∅ ^
           matriculado = mat_r ∪ ambos ^
           certificado = ambos

Assim, é necessário fazer um refinamento da operação certificar para que os certificados sejam entregues aos estudantes que fizeram todos os exercícios e que suas matriculas sejam desativadas. A Listagem 12 descreve que o elemento deverá ser retirado do conjunto matriculado e adicionado ao conjunto de matriculados que fizeram todos os exercícios.

Listagem 12. Refinamento da operação certificar.

certicar(st) =
  BEGIN
      mat_r := mat_r - st ||
      ambos := ambos ∪ st
  END

Etapa de Implementação

Na etapa de implementação são definidas as instâncias que serão executadas de acordo com refinamento especificados. A Listagem 13 define a especificação de uma implementação do refinamento anterior. Na cláusula IMPORTS são encapsulados os estados das máquinas. Neste caso, a máquina BT_SET que manipula o conjunto de estudantes do qual foram criadas duas instâncias: uma para a variável ambos e a outra para a variável mat_r. Toda mudança ou consulta de estado deve ser feita por meio das operações das máquinas “importadas”. Na cláusula INVARIANT é definido que as variáveis ambos e mat_r vão fazer uso das instâncias de máquinas que foram importadas acima, neste caso são instâncias da mesma máquina. Na cláusula INITIALISATION as variáveis são inicializadas vazias.

Listagem 13. Descrição da implementação.

IMPLEMENTATION CMA_ref_imp (tam_turma, ESTUDANTE)
  REFINES CMA_refined
  IMPORTS
            ambos.BT_SET (tam_turma, ESTUDANTE),
            mat_r.BT_SET (tam_turma, ESTUDANTE)
  INVARIANT
            ambos = ambos.bt_set ^
            mat_r = mat_r.bt_set
  INITIALISATION
            ambos.clear;
            mat_r.clear

A Listagem 14 descreve a implementação da operação certificar, que remove o elemento do conjunto matriculados e adiciona no conjunto matriculados com todos os exercícios feitos.

Listagem 14. Implementação da operação certificar.

certificar(st) =
  BEGIN
         mat_r.remove(st);
         ambos.add(st)
  END

Ferramentas de Apoio ao Desenvolvimento em B

Existem diversas ferramentas disponíveis no mercado para apoio ao desenvolvimento na notação formal B e também para animação. As ferramentas AtelierB, B4Free, B-Toolkite Rodinsão utilizadas como ambientes de desenvolvimento. A ferramenta ProB é utilizada para a animação e para checagem de modelos. Já a ferramenta Brama é utilizada para modelagem na notação formal B.

Outros tipos de projetos ferramentais que trabalham aliadas a notação B são:


  • ComenC: um tradutor de especificações B para a linguagem de programação C que já incorporada a ferramenta AtelierB ou obtida separadamente e disponível somente para Linux.
  • Composys: ferramenta e método para modelagem de sistemas críticos de segurança. Faz uso do formalismo Event-B e está disponível para as plataformas Linux e Windows.

Após a investigação realizada e descrita neste post podemos concluir que o Método B possui aplicação bem sucedida na indústria e, pelas fontes consultadas, principalmente na modelagem de sistemas críticos. Além disso, tem ótimo suporte ferramental, tendo em vista que existe uma ampla quantidade de ferramentas de ótima qualidade para auxiliar no desenvolvimento. Para mais informações sobre a notação B visitem o site oficial da notação e no site da companhia ClearSy. Espero que tenham gostado deste artigo e até a próxima.