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: 2010/2011 - 1S

Ativa?	Sim
Página Web:	http://paginas.fe.up.pt/~apaiva/teach/1011/MFES.htm
Página e-learning:	http://moodle.fe.up.pt/
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	0	Plano de estudos oficial	4	-	6	56	162
			5
MIEIC	141	Plano de estudos a partir de 2009/10	4	-	6	56	162

Língua de trabalho

Português - Suitable for English-speaking students

Objetivos

No final da unidade curricular os estudantes devem ser capazes de:
- 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.
- identificar 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.
A ferramenta Jape.

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, bem como, realização de exercícios prá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

JAPE
Alloy Analyzer
VDMTools

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	56,00
Exames	Exame	6,00		2011-02-11
Trabalhos práticos	Trabalho escrito	40,00		2010-11-27
	Total:	-	0,00

Componentes de Ocupação

Descrição	Tipo	Tempo (Horas)	Data Conclusão
Estudo individual e acompanhamento das aulas	Estudo autónomo	40	2011-02-11
Estudo para realização dos trabalhos práticos	Estudo autónomo	20	2010-11-26
	Total:	60,00

Obtenção de frequência

Nota mínima de 45% na classificação de frequência.
A presença nas aulas teórico-práticas é registada e obrigatória conforme legislação em vigor.

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 3 valores a classificação do exame arredondada para o inteiro mais próximo.

Provas e trabalhos especiais

Trabalho prático de Alloy:
- entrega até às 23h do dia 15 de Outubro;
- defesa do trabalho prático durante as aulas práticas da semana de 18 a 22 de Outubro.

Trabalho prático de VDM++:
- entrega até às 23h do dia 26 de Novembro;
- defesa do trabalho prático durante as aulas práticas da semana de 29 Nov a 3 de Dez.

A defesa dos trabalhos práticos é obrigatória para TODOS os alunos.

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.

Os alunos dispensados de frequência às aulas devem contactar o docente para sessões especiais de acompanhamento dos trabalhos.

A defesa dos trabalhos práticos é obrigatória para TODOS os estudantes.

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.