Please enable JavaScript.
Coggle requires JavaScript to display documents.
Formal methods - Coggle Diagram
Formal methods
B method
Codigo que faz jus a espeficação
4 ideias chaves definem o desenvolvimento com B
Modelagem de Especificações
Single-threaded
Provas exaustivas
Gestão de complexidade
Mecanismos de Estruturação
Modularidade
Refinamento
Modelagem com event B
Foco em nivel de sistema
modelo baseado em eventos
refinamento progressivo
Impacto no ciclo V
Verificação vertical por provas
Eliminação de testes unitarios
Redução de testes de integração
specification
Modelo de um sistema com o comportamento esperado
Problemas
Como garantir o comportamento esperado?
Como conseguir uma implementação com o comportamento coerente a especificação?
Taxonomia
manual
horizontal verification
vertical verification
Provas
animation
Executar/simular a especificação para observar comportamento
tranformation
proving properties
rigor
elimina ambiguidade
Estilos
Estados/Modelos
Baseado em dados
Maquina Abstrata
Especificação formal
Constante e variaveis
Execução sim
Estrutura de Projetos B e Dependências
Hierarquia de Organização
Projeto B
Modulo B
Componente B
Mecanismos de Ligação entre módulos
Link de importação
Link de Visualização
integração e código externo
Uso de bibliotecas
Integração com codigos tradicionais
Máquina Basica
Os tres aspectos de um componente
Aspecto estatico
Espaço de Estados
Invariante
Aspecto dinamico
inicializaç~eo
Operações
Aspecto de prova
Obrigação de Prova
Refinamento
Adição de Detalhes
refinamento de dados
refinamento algorítmico