Departamento de Informática (UM)

Métodos Formais em Engenharia de Software

14598 [ME78ME7800003255]

Mestrado em Engenharia Informática [MEINF]

S1

Manuel Alcino Pereira Cunha

Objetivos

O objetivo desta UC é dar uma introdução geral à utilização de métodos formais na engenharia de software, focando-se nas fases de concepção (modelação) e de implementação (derivação de programas). Pretende-se que os alunos consolidem a teoria com a prática de usar ferramentas para análise e verificação automática, quer dos requisitos dos modelos, quer dos contratos dos programas.

Programa

1. Introdução aos métodos formais:
1.1. Utilização de métodos formais no processo de desenvolvimento de software;
1.2. Breve história dos métodos formais.
2. Técnicas e ferramentas para análise de modelos estruturais:
2.1. Modelação usando conjuntos e relações;
2.2. Especificaçãocom lógica relacional;
2.3. Análise automática usando ferramentas de model finding.
3. Técnicas e ferramentas para análise de modelos comportamentais:
3.1. Modelação de comportamento com máquinas de estados finitas;
3.2. Modelação de sistemas ciber-físicos usando autómatos híbridos;
3.3. Especificação de comportamento com lógica temporal;
3.4. Análise automática usando ferramentas de model checking explícito, simbólico e bounded.
4. Técnicas e ferramentas para análise e verificação de programas especificados por contratos:
4.1. Análise estática por interpretação abstrata;
4.2. Verificação dinâmica, dedutiva e bounded.
5. Introdução ao refinamento de dados e operações.

Bibliografia

D. Jackson. Software abstractions: logic, language, and analysis. Revised edition, MIT Press, 2012.

C. Baier and J.-P. Katoen. Principles of Model Checking. MIT Press, 2008.

José Bacelar Almeida, Maria João Frade, Jorge Sousa Pinto, and Simão Melo de Sousa. 2011. Rigorous Software Development: An Introduction to Program Verification (1st ed.). Springer Publishing Company, Incorporated.

Logical foundations of cyber-physical systems. André Platzer. Published by Springer, 2018; ISBN: 978-3-319-63587-3.

Resultados da aprendizagem

No final, os alunos serão capazes de:
- Compreender o papel dos métodos formais na engenharia de software.
- Modelar o comportamento e as estruturas de dados de um sistema de software (possivelmente ciber-físico).
- Especificar os requisitos de um sistema de software usando lógica temporal e lógica relacional.
- Utilizar ferramentas de model finding e model checking na análise automática de modelos de software.
- Especificar programas por contratos.
- Utilizar ferramentas para diversas tarefas na análise e verificação de programas.

Método de avaliação

A avaliação inclui os seguintes elementos de avaliação:
- teste escrito (60%);
- trabalho de grupo ou teste prático laboratorial (40%).

Funcionamento

Turno: T 1; Docente: Manuel Alcino Pereira Cunha; Dep.: DI; Horas: 15.
Turno: T 1; Docente: Jorge Miguel Matos Sousa Pinto; Dep.: DI; Horas: 15.
Turno: TP 1; Docente: Jorge Miguel Matos Sousa Pinto; Dep.: DI; Horas: 15.
Turno: TP 2; Docente: Jorge Miguel Matos Sousa Pinto; Dep.: DI; Horas: 15.
Turno: TP 3; Docente: Manuel Alcino Pereira Cunha; Dep.: DI; Horas: 15.
Turno: TP 4; Docente: Manuel Alcino Pereira Cunha; Dep.: DI; Horas: 15.
Turno: TP 5; Docente: Manuel Alcino Pereira Cunha; Dep.: DI; Horas: 15.