DC-UFRPE/Bacharelado em Ciência da Computação/14079 - MÉTODOS FORMAIS

Programa da Disciplina

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 - Engenharia de Software

Ementa

• 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

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

Básica

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

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.