Métodos Formais em Engenharia de Software

Código:

EIC0039

Sigla:

MFES

Áreas Científicas
Classificação	Área Científica
OFICIAL	Engenharia de Software

Ocorrência: 2007/2008 - 2S

Ativa?	Sim
Página Web:	http://paginas.fe.up.pt/~apaiva/teach/0708/MFES.htm
Unidade Responsável:	Secção de Informática
Curso/CE Responsável:	Mestrado Integrado em Engenharia Informática e Computação

Ciclos de Estudo/Cursos

Sigla	Nº de Estudantes	Plano de Estudos	Anos Curriculares	Créditos UCN	Créditos ECTS	Horas de Contacto	Horas Totais
LEIC	0	Plano de estudos de transição para 2006/07	4	5	5	-
MIEEC	0	Plano de estudos oficial a partir de 2007/08	4	-	5	-
MIEIC	102	Plano de estudos oficial a partir de 2006/07	4	-	5	-

Língua de trabalho

Português

Objetivos

Saber aplicar métodos formais de especificação (baseado em modelos; baseado em propriedades; baseado em comportamento) e verificação ("Model-checking", provas formais e teste) no desenvolvimento de sistemas de software.
Conhecer os métodos formais existentes e saber quando devem ser aplicados e quais são mais adequados em cada caso.

Programa

1. Introdução (semana 1)
O que são métodos formais.
Importância e aplicabilidade dos métodos formais no desenvolvimento de software.
Modelos de ciclo de vida e processos de desenvolvimento de software incorporando métodos formais.
Especificação, refinamento, implementação, verificação e validação.
Classificação de métodos formais.
Modelos explícitos vs implícitos, executáveis vs não executáveis.
Técnicas de verificação formal.

2. Especificação baseada em modelos (semanas 2-4)
As linguagens VDM-SL e VDM++.
Representação de dados com base em estruturas matemáticas (conjuntos, sequências e funções finitas).
Especificação com estado e sem estado.
Definição de tipos, valores e funções.
Definição de classes, variáveis de instância e operações.
Expressões e instruções.
Design-by-contract: definição de invariantes, pré-condições e pós-condições.
Descrição de algoritmos, especificações executáveis.
Análise de consistência da especificação: obrigações de prova e teste.
Ligação do VDM++ ao UML.
Geração de código a partir de uma especificação formal.
A ferramenta VDMTools.

3. Lógica e "Model Checking" (semanas 5 e 6)
Lógica proposicional, de predicados, temporal linear (LTL), temporal ramificada (CTL).
Representação de estados.
"Model Checking":
- Propriedades: "Safety"; "Fairness"; "Liveness"; Universalidade; Inevitabilidade; Possibilidade; Ausência; Resposta; Precedência.
- Problema de Explosão de estados (técnicas existentes para minorar este problema): Estado Simbólico; "Bounds"; "On-the-fly"; "Partial Order Reduction (POR)"; Abstracção.
A ferramenta Spin e a liguagem de especificação Promela.

4. "Alloy Constraint Analyzer", para modelação e análise semântica (semanas 7-8)
Modelação declarativa.
Diferenças relativas a "model checking".
Comandos Alloy.
Funções; Predicados; Factos; Asserções e Verificações ("Checks").
Modelação estática vs dinâmica.
Simular a execução de uma operação.
Verificar propriedades "safety".
A ferramenta Alloy analyzer.

5. Especificação algébrica (semana 9)
Tipos abstractos de dados.
A linguagem OBJ.
Estrutura da especificação.
Especificação de operações (de construção, transformação e inspecção).
Especificação de axiomas.
Análise da especificação: completude, redundância, consistência, prova de teoremas com base em axiomas, testes.
A ferramenta CafeObj.

6. Provas Formais (semana 10-12)
Aplicação de lógica de Hoare à prova de correcção de algoritmos.
Linguagem de especificação Gallina: tipos e expressões; proposições e provas; tipos de dados indutivos; tácticas de prova e automação; predicados indutivos.
A ferramenta Coq 8.1pl3.

Bibliografia Obrigatória

Fitzgerald, John; Validated designs for object-oriented systems. ISBN: 1-85233-881-4
Yves Bertot e Pierre Castéran; Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions, Springer, 2004. ISBN: 3-540-20854-2
B. Bérard; M. Bidoit; A. Finkel; F. Laroussinie; A. Petit; L. Petrucci; Ph. Schnoebelen; P. McKenzie; Systems and Software Verification - Model Checking Techniques and Tools, Springer, 2001. ISBN: 3-540-41523-8

Bibliografia Complementar

Fitzgerald, John; Modelling systems. ISBN: 0-521-62605-6
Alagar, V. S.; Specification of software systems. ISBN: 0-387-98430-5
Peled, Doron A.; Software reliability methods. ISBN: 0-387-95106-7
Clarke, Jr., Edmund M.; Model checking. ISBN: 0-262-03270-8

Métodos de ensino e atividades de aprendizagem

As aulas teóricas serão usadas para exposição e estudo dos conteúdos programáticos.
As aulas práticas serão usadas para realização de exercícios, para contactar com a diversas ferramentas e para a realização de trabalhos práticos.

Software

VDMTools
Spin
Coq
CafeOBJ
Alloy Analyzer

Palavras Chave

Ciências Tecnológicas > Engenharia > Engenharia de computadores
Ciências Tecnológicas > Tecnologia > Tecnologia de computadores > Tecnologia de software

Tipo de avaliação

Avaliação distribuída com exame final

Componentes de Avaliação

Descrição	Tipo	Tempo (Horas)	Peso (%)	Data Conclusão
Aulas da disciplina (estimativa)	Participação presencial	56,00
Exames	Exame	10,00		2008-07-29
Trabalhos práticos	Trabalho escrito	50,00		2008-05-26
	Total:	-	0,00

Componentes de Ocupação

Descrição	Tipo	Tempo (Horas)	Data Conclusão
Estudo individual	Estudo autónomo	20	2008-07-29
	Total:	20,00

Obtenção de frequência

Nota mínima de 40% na classificação de frequência.

Fórmula de cálculo da classificação final

Avaliação distribuída com exame final, com as seguintes componentes:
a) exame final com consulta, duração 2h, peso 40%, nota mínima de 40%;
b) classificação de frequência, 60%:
- trabalho prático, peso 30%, nota mínima de 40%;
- trabalho prático, peso 30%, nota mínima de 40%.

Nota: em todo o caso, a classificação final não pode exceder em mais de 4 valores a classificação do exame arredondada para o inteiro mais próximo.

Avaliação especial (TE, DA, ...)

Os trabalhos são obrigatórios para todos os alunos, mesmo para os alunos dispensados de frequência às aulas.

Melhoria de classificação

A classificação do exame pode ser melhorada em exame de recurso.
As classificações obtidas nos trabalhos práticos podem ser melhoradas na edição seguinte da disciplina.