Departamento de Informática (UM)

Modelação e Análise Avançadas de Sistemas

15750 [ME87ME8704007099]

Mestrado em Engenharia Aeroespacial [MEA]

S1

Manuel Alcino Pereira Cunha

Objetivos

Esta UC tem por objetivo lecionar técnicas de modelação e análise de sistemas de software. Dada a natureza crítica do domínio aeroespacial, o foco será em técnicas formais que suportem o desenvolvimento de software confiável, em particular técnicas de verificação de modelos para análise automática de requisitos estruturais e comportamentais do sistema.

Programa

1. Linguagens formais para modelação estrutural de sistemas de software.
2. Modelação comportamental de sistemas de software com máquinas de estados.
3. Lógicas para especificação formal de requisitos estruturais e comportamentais.
4. Análise de requisitos com técnicas automáticas de verificação de modelos.
5. Técnicas avançadas para modelação de sistemas interativos, sistemas de tempo real e sistemas ciberfísicos.

Bibliografia

Jackson, D., 2012. Software Abstractions: logic, language, and analysis. MIT press.

Baier, C. and Katoen, J.P., 2008. Principles of model checking. MIT press.

Weyers, B., Bowen, J., Dix, A. and Palanque, P. eds., 2017. The handbook of formal methods in human-computer interaction. Springer.

Abrahám, E., 2012. Modeling and analysis of hybrid systems. RWTH Aachen University, Lecture Notes.

Resultados da aprendizagem

- Idealizar modelos estruturais de software a diferentes níveis de abstração;
- Modelar o comportamento de um sistema de software com uma máquina de estados;
- Usar um modelo comportamental com informação de tempo real;
- Formalizar a interação de um sistema de software com o ambiente onde opera (incluindo os utilizadores e outros sistemas analógicos);
- Especificar requisitos estruturais de software com lógicas de primeira ordem;
- Especificar requisitos comportamentais de software com lógicas temporais;
- Utilizar ferramentas de verificação de modelos para análise automática de requisitos de software.

Método de avaliação

A avaliação consistirá num projeto desenvolvido em grupo ao longo do semestre (70%-90%). O projeto consistirá na modelação e análise de vários aspetos de um caso de estudo relacionado com domínio aeroespacial.
A avaliação será dividida em vários checkpoints ao longo do semestre e complementada com uma componente de avaliação contínua do comportamento do estudante nas aulas laboratoriais (10%-30%).

Funcionamento

Turno: T 1; Docente: José Francisco Creissac Freitas Campos; Dep.: DI; Horas: 10.
Turno: T 1; Docente: Manuel Alcino Pereira Cunha; Dep.: DI; Horas: 10.
Turno: T 1; Docente: Renato Jorge Araújo Neves; Dep.: DI; Horas: 10.
Turno: PL 1; Docente: José Francisco Creissac Freitas Campos; Dep.: DI; Horas: 10.
Turno: PL 1; Docente: Manuel Alcino Pereira Cunha; Dep.: DI; Horas: 10.
Turno: PL 1; Docente: Renato Jorge Araújo Neves; Dep.: DI; Horas: 10.