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: 2016/2017 - 1S

Ativa?	Sim
Página Web:	http://moodle.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
MIEIC	144	Plano de estudos a partir de 2009/10	4	-	6	56	162

Língua de trabalho

Inglês

Objetivos

1-CONHECIMENTOS ÚTEIS Conhecimentos de engenharia de software (nomeadamente, processos de desenvolvimento e modelação de software) e conhecimentos de teoria de computação.

2-OBJETIVOS ESPECÍFICOS Desenvolver as capacidades de abstração de forma a descrever o que o sistema deve fazer e não a maneira de o fazer. Estar familiarizados com os métodos formais e forma como eles podem contribuir para aumentar a qualidade dos sistemas de software.

3-CONHECIMENTO PRÉVIO É útil frequência anterior em Engenharia de software, Teoria de computação e Conceção e análise de algoritmos.

4-DISTRIBUIÇÂO PERCENTUAL Componente científica = 75% Componente tecnológica = 25%

5-RESULTADO DA APRENDIZAGEM 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.

Resultados de aprendizagem e competências

1. No final da unidade curricular, os estudantes deverão ser capazes de especificar um sistema de software de forma declarativa, saber distinguir os vários métodos formais existentes e quando os aplicar e perceber a utilidade destas técnicas para a melhoria da qualidade dos sistemas de software.

Modo de trabalho

Presencial

Programa

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

2. Provas Formais
2.1 Aplicação de lógica de Hoare à prova de correcção de algoritmos.
2.2 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.
2.3 Prova de correcção de programas.
2.4 A ferramenta Jape.

3. "Alloy Constraint Analyzer", para modelação e análise semântica
3.1 Modelação declarativa.
3.2 Diferenças relativas a "model checking".
3.3 Comandos Alloy.
3.4 Funções; Predicados; Factos; Asserções e Verificações ("Checks").
3.5 Modelação estática vs dinâmica.
3.6 Simular a execução de uma operação.
3.7 Verificar propriedades "safety".
3.8 A ferramenta Alloy analyzer.

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

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
Derrick G. Kourie, Bruce W. Watson; The correctness-by-construction approach to programming. ISBN: 978-3-642-27918-8

Bibliografia Complementar

Alagar, V. S.; Specification of software systems. ISBN: 0-387-98430-5
Richard Bornat; Proof and Disproof in Formal Logic, Oxford University Press, 2005. ISBN: 0-19-8530269

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 diversas ferramentas e para a realização de trabalhos práticos.

Software

VDMTools
Alloy Analyzer
Overture

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 sem exame final

Componentes de Avaliação

Designação	Peso (%)
Teste	60,00
Trabalho laboratorial	40,00
Total:	100,00

Componentes de Ocupação

Designação	Tempo (Horas)
Estudo autónomo	60,00
Frequência das aulas	52,00
Trabalho laboratorial	50,00
Total:	162,00

Obtenção de frequência

Nota mínima de 40% na classificação do trabalho prático. A presença nas aulas teórico-práticas é registada e obrigatória conforme legislação em vigor.
Nota mínima de 40% em cada minitestes.

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

Avaliação distribuída sem exame final, com as seguintes componentes:
(A) trabalho prático de VDM++, peso 40%, nota mínima de 40%.
(B) Miniteste 1, duração 1h30, peso 30%, nota mínima de 40%.
(C) Miniteste 2, duração 1h30, peso 30%, nota mínima de 40%.

Classificação Final = (A)*40% + (B)*30% + (C)*30%

 

Provas e trabalhos especiais

Trabalho prático de VDM++: entrega até às 23h do dia 6 de janeiro; defesa do trabalho prático durante a semana de 9-13 de janeiro.

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

- As classificações obtidas no trabalho prático podem ser melhoradas na edição seguinte da disciplina
- A classificação dos mintestes pode ser melhorada em exame de recurso.

Observações

Os alunos com frequência à disciplina do ano anterior terão que fazer os mintestes A classificação obtida no trabalho de VDM++ do ano anterior será usada como classificação do trabalho de VDM++ desta edição.