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: 2019/2020 - 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 Matemática Discreta, Algoritmos e Estruturas de Dados, Conceção e Análise de Algoritmos, Teoria da Computação e Engenharia de Software.

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, propriedades e comportamento) e verificação (provas formais e model-checking) 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

No final da unidade curricular, os estudantes deverão ser capazes de especificar  e verificar formalmente um sistema de software, 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

Pré-requisitos (conhecimentos prévios) e co-requisitos (conhecimentos simultâneos)

Pré-requisitos desejáveis: Matemática Discreta; Algoritmos e Estruturas de Dados; Conceção e Análise de Algoritmos; Teoria da Computação; Engenharia de Software.

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 Métodos formais no ciclo de vida do software: especificação, refinamento, implementação, verificação e validação.
1.4 Classificação de métodos formais.
1.5 Técnicas de verificação formal.

2. Verificação formal de programas
2.1 Verificação de programas com lógica de Hoare.
2.2 Verificação de programas por cálculo da pré-condição mais fraca.
2.3 Introdução à linguagem Dafny (sistema de tipos, organização de programas, mecanismos de especificação e verificação, ferramentas).
2.4 Especificação e verificação de algoritmos e programas imperativos em Dafny.
2.5 Desenho por contrato e verificação de estruturas de dados  e programas orientados por objetos em Dafny. 
2.6 Técnicas avançadas de especificação e verificação em Dafny (abstração de dados, refinamento, lemas, etc.).

3. Verificação por model checking de sistemas reactivos
3.1 Modelação de sistemas reactivos: sistemas de transição e concorrência.
3.2 Propriedades temporais lineares.
3.3 Lógica temporais: linear (LTL) e ramificada (CTL e CTL*).
3.4 Model checkers.
3.5 Model checking simbólico: BDDs e OBDDs.
3.6 Algoritmos de decisão baseados em autómatos finitos.

Bibliografia Obrigatória

Huth, M., & Ryan, M. ; Logic in Computer Science, Cambridge University Press, 2004. ISBN: 978-0-511-26401-6
Baier Christel; Principles of model checking, MIT Press, 2008. ISBN: 978-0-262-02649-9

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
Daniel Jackson; Software Abstractions, MIT Press, 2006. ISBN: 0-262-10114-9
Derrick G. Kourie, Bruce W. Watson; The correctness-by-construction approach to programming. ISBN: 978-3-642-27918-8

Métodos de ensino e atividades de aprendizagem

As aulas teóricas serão usadas para exposição e discussão 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

Spin
Dafny extension for Visual Studio Code
iSpin
Dafny
jSpin

Palavras Chave

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

Tipo de avaliação

Avaliação distribuída sem exame final

Componentes de Avaliação

Designação	Peso (%)
Teste	100,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

A presença nas aulas teórico-práticas, bem como nas aulas teóricas com oradores convidados, é registada e obrigatória conforme legislação em vigor.
Nota mínima de 40% em cada miniteste.

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

Avaliação distribuída sem exame final, com as seguintes componentes:
(MT1) Miniteste 1, duração até 2h, peso 50%, nota mínima de 40%.
(MT2) Miniteste 2, duração até 2h, peso 50%, nota mínima de 40%.

 

Provas e trabalhos especiais

Estudantes com classificação superior a 75% no 1º mini-teste, podem desenvolver um projeto (P) individual em Dafny, de especificação, implementação e verificação de um algoritmo ou estrutura de dados de complexidade média, não verificado previamente em Dafny. A classificação final é então calculada como 50% * max(P, MT1) + 50% * MT2.

Existirá um exame de recurso com duas partes (correspondentes a MT1 e MT2) a que todos os estudantes podem aceder (desde que tenham cumprido as regras de assiduidade e tenham realizado os dois mini-testes, atingindo ou não a nota mínima), para obtenção de aprovação ou melhoria de classificação a uma ou ambas as partes.

Melhoria de classificação

A classificação dos mintestes pode ser melhorada em exame de recurso.

Observações

Palestra convidada a 10 de outubro (presença obrigatória): "Formal Method, Software Development and Safety Critical Systems" by Thierry Lecomte, ClearSy.