DC-UFRPE/Bacharelado em Ciência da Computação/14079 - MÉTODOS FORMAIS
Programa da Disciplina
[editar | editar código-fonte]Nome: | Métodos Formais |
Código: | 14079 |
Departamento: | Departamento de Computação (DC) |
Área: | Engenharia de Sistemas de Software |
Carga-horária total: | 60 horas |
Créditos: | 4 |
Pré-requisitos: | - Introdução a Programação I |
Ementa
[editar | editar código-fonte]- Processo de desenvolvimento formal.
- Classificação dos métodos formais.
- Notação formal para especificação de sistemas.
- Notação formal para especificação de propriedades do sistema.
- Noções de leis e cálculo usados para refinamento.
- Ferramenta para animação de especificação formal.
- Ferramenta para verificação automática de propriedades de modelos.
- Ferramenta para verificação automática de refinamento entre modelos.
Conteúdo Programático
[editar | editar código-fonte]1. Introdução aos métodos formais
a. Desenvolvimento formal de software
b. Tipos de métodos formais
c. Diferentes tipos de ferramentas de apoio ao desenvolvimento (semi) formal
d. Aplicações
2. Detalhamento de ao menos um método formal que deve ser uma álgebra de processos, ou, um método formal baseado em modelos
a. Se escolhida uma álgebra de processos como CSP, LOTOS ou FSP
i. Processo, alfabeto e comunicação
ii. Operadores para composição de processos
iii. Modelo operacional
iv. Modelos denotacionais e refinamentos
v. Propriedades clássicas: livelock, deadlock e não determinismo
vi. Ferramentas para verificação automática de refinamentos
b. Se escolhido um método formal baseado em modelos como B, Z ou VDM
i. Tipos, variáveis, operações e invariantes
ii. Consistência vs. refinamento
iii. Refinamento de máquinas, operações e dados
iv. Lógica temporal
v. Ferramenta para verificação automática de invariantes e refinamentos
Bibliografia
[editar | editar código-fonte]Básica
[editar | editar código-fonte]1) HUTH, R. A; RYAN, M. D. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, Second Edition, 2004.
2) Roscoe, A. W. The Theory and Practice of Concurrency, Prentice Hall, 2005.
3) J. R. Abrial, The B-Book: assigning programs to meanings, Cambridge University Press New York, NY, USA 1996
Complementar
[editar | editar código-fonte]1) Woodcock, J.; Davies J. Using Z - Specification, Refinement, and Proof. Prentice-Hall, 1996
2) Roscoe, A. W. Understanding Concurrency, Springer, 2010.
3) Jones, C.B. Systematic Software Development using VDM, Prentice Hall 1990.
4) Magee, J.; Kramer, J. Concurrency: State Models & Java Programs. Second Edition. Wiley 2006.
5) Morgan, C. Programming from Specifications. Second edition. Caroll Morgan 1998.