Métodos Formais
Juan Andrés Mussini
Métodos Formais
Métodos formais são técnicas baseadas em regras
matemáticas para especificar, desenvolver e verificar
sistemas de software e hardware.
Classificações – Semântica
denotacional
●
●
●
●
●
O significado de um sistema é expressado em
forma de função matemática
As funções semânticas denotam os significados
das estruturas das linguagens de programação.
A abordagem faz uso de cálculo lambda para
modelar as funções.
Nem todo sistema pode ser vistos como uma
função.
Comando de composição S1;S2 é dado por
Classificações - Semântica
Operacional
●
●
Preocupa-se mais em como os programas são
executados do que meramente com os resultados.
O significado do sistema é expressado como uma
sequência de ações de um modelo computacional
(teoricamente) mais simples.
–
Semântica operacional estruturada – mais detalhada
●
–
a atribuição x: = a será avaliada no estado s como sendo a transição que conduz
ao estado em que a variável x foi substituida pelo valor A[a]s
Semântica natural – mais simples
Classificações – Semântica
Axiomática
●
Especificam propriedades do efeito da execução
das estruturas como asserções.
–
Asserções: sentenças de lógica de predicado são
geralmente chamadas de axiomas.
●
●
●
●
{P}Q{R} > P e R são asserções.
P - pré-condição: sentença verdadeira antes da execução do
comando Q
R - póscondição: sentença verdadeira após Q
Enfatiza a possibilidade de provar propriedades de
programas usando-se lógica formal,
particularmente verificação formal.
Finalidades
•Realizar provas matemáticas que garantem que este modelo
possui as propriedades requisitadas (verificação)
•Analisar se a solução proposta é aceitável do ponto de vista
de desempenho, indicando quais as melhores estratégias para
implementação a serem seguidas
•Validar um modelo através de simulações
•Realizar o desenvolvimento do software podendo-se provar
que a implementação está correta (geração de código
correto).
• Especificação
• Desenvolvimento
• Verificação
Método/Notação Z
●
Definição dos estados
Notação Z
●
Operações
Notação Z
●
Estado inicial
Notação Z
●
Conjunção
Notação Z
●
Conjunção
Notação Z
Implementação
Verificação
Verificação
●
●
Linguagem Natural
Autômatos
Método de gramáticas de grafos
●
●
Linguagem visual de representação
Descreve com naturalidade fenômenos de sistemas
concorrentes
–
Redes de Petri
Redes de Petri