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: 2009/2010 - 2S

Ativa?	Sim
Página Web:	http://paginas.fe.up.pt/~apaiva/teach/0910/MFES.htm
Unidade Responsável:	Departamento de Engenharia 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
MIEEC	1	Plano de estudos oficial a partir de 2007/08	4	-	6	56	162
MIEIC	125	Plano de estudos a partir de 2009/10	4	-	6	56	162

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
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. "Alloy Constraint Analyzer", para modelação e análise semântica
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.

3. Lógica e "Model Checking"
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.

4. Especificação baseada em modelos
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.

5. Provas Formais
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.
Prova de correcção de programas.
As ferramenta Coq, Caduceus, JAPE e Krakatoa.

Bibliografia Obrigatória

Daniel Jackson; Software Abstractions, MIT Press, 2006. ISBN: 0-262-10114-9
Fitzgerald, John; Validated designs for object-oriented systems. ISBN: 1-85233-881-4
Richard Bornat; Proof and Disproof in Formal Logic, Oxford University Press, 2005. ISBN: 0-19-8530269
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

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

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
Coq
Krakatoa
JAPE
Alloy Analyzer
Caduceus

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
Participação presencial (estimativa)	Participação presencial	64,00
Exames	Exame	12,00		2010-07-31
Trabalhos práticos	Defesa pública de dissertação, de relatório de projeto ou estágio, ou de tese	50,00		2010-06-26
	Total:	-	0,00

Componentes de Ocupação

Descrição	Tipo	Tempo (Horas)	Data Conclusão
Estudo individual	Estudo autónomo	36	2010-07-24
	Total:	36,00

Obtenção de frequência

Nota mínima de 45% na classificação de frequência.
Nota mínima de 45% no exame.

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 2h30, peso 50%, nota mínima de 45%;
b) classificação de frequência, 50%:
- trabalho prático, peso 25%, nota mínima de 45%;
- trabalho prático, peso 25%, nota mínima de 45%.

Nota: em todo o caso, a classificação final não pode exceder em mais de 2.5 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.