Métodos Formais em Engenharia de Software

Mestrado Integrado em Engenharia Informática - MFES 2019/2020

Tópicos

Avisos

17 Set - Vídeo de apresentação da edição de tinynew.gif 2020/21.

30 Mar - VF: alteração do método de avaliação. tinynew.gif

21 Fev - VF: aula de substituição será, 4ª feira, 26-Fev, às 14:00, na sala 0.04 do DI.

10 Fev - CSI: afixadas as notas finais na página de CSI.

4 Fev - As aulas de AC e VF iniciam-se esta quinta-feira, 6-Fev.

28 Jan - CSI: o exame de recurso terá lugar na sala E2-1.10 às 9h00.

26 Jan - CSI: estão lançadas as classificações após a realização do teste - ver página CSI. Atendimento para mostrar os testes: dia 27-Jan, às 16h.

13 Jan - CSI: a aula de dúvidas amanhã de tarde será às 17h, na sala 0.09, e não às 16h, como por lapso disse a alguns alunos. Pf ver Sumarios.

13 Jan - CSI: matéria para a parte 2 do teste - ver FAQ 9 na página de CSI.

13 Jan - CSI: o teste terá lugar no dia 16-Jan às 14h, na sala E7-0.07.

13 Jan - CSI: haverá uma aula de dúvidas amanhã de tarde, na sala 0.09, pf ver Sumarios.

5 Jan - EM: o prazo para a entrega do TP2 foi adiado uma semana.

2 Jan - CSI: estão lançadas as classificações do mini-teste na página CSI.

3 Dez - CSI: os alunos devem prestar atenção ao material pedagógico que vai aparecendo na página da disciplina.

24 Nov - CSI: os alunos devem prestar atenção às FAQs que vão saindo na página da disciplina.

12 Nov - CSI: mini-teste terá lugar no dia 28-Nov às 14h, na sala E7-0.07. Haverá aula depois até às 17h.

10 Nov - CSI: Caso de estudo da aula de 7-Nov ('campeonato de futebol') adicionado ao material da disciplina.

29 Out - CSI: Formulário actualizado colocado na página respectiva.

2 Out - Atenção à mudança de sala de ATS: passa para CP2.-2.08.

26 Set - Atenção à mudança de sala de CSI: passa da 1.10 para a 0.07 (Edifício 7).

17 Set - Início das aulas: 17-Set (ATS).

-- JoseNunoOliveira - 17 Sep 2019

Especificação e Modelação

Programa

  • Lógicas para especificação e modelação
    • Lógica de primeira ordem
    • Lógica relacional
    • Lógica temporal
  • Técnicas de análise e verificação
    • Simulação
    • Model-finding para lógica relacional
    • Model-checking para lógica temporal
  • Linguagens e ferramentas principais
    • Alloy e o respectivo Analyzer
    • Electrum e o respectivo Analyzer
  • Outras linguagens e ferramentas
    • SMV e NuSMV
    • TLA+ e a respectiva Toolbox

Docente / Horário

Docente Foto Horário Sala
Manuel Alcino Cunha Alcino 5a-feira, 9h-10h (T) E7 1.10
Nuno Moreira Macedo Nuno 5a-feira, 10h-12h (PL) E7 1.10

NB: poderá haver trocas de horário entre EM e CSI de acordo com necessidades de serviço dos docentes das duas disciplinas.

Método de avaliação

  • 1 teste individual escrito (70%, ≥ 8)
    • Data do teste: 9 de Janeiro de 2020
    • Data do exame: 23 de Janeiro de 2020
  • 2 trabalhos a realizar em grupos de 2 alunos (30%, ≥ 10)

Material pedagógico

Acetatos

Exercícios

Leituras recomendadas

Enunciados dos trabalhos

Os carros modernos oferecem várias funcionalidades de segurança e conforto baseadas em componentes de software. Em particular, são já comuns atualmente sistemas de luzes exteriores adaptativos e de controlo de velocidade. Estes sistemas recolhem informação tanto de sensores (e.g., de luminosidade ou de velocidade) e da interface com o condutor (e.g., botões ou opções no computador de bordo), que é depois usada para controlar os atuadores (e.g., luzes externas ou os travões). É também comum que estes sistemas sejam adaptáveis para diferentes mercados (e.g., carros vendidos na UE ou nos EUA têm que seguir diferentes regras). O seguinte apontador descreve possíveis requisitos para sistemas deste tipo, e foi lançado como desafio numa conferência sobre métodos formais como os que estudamos nesta UC. Disponibiliza também um conjunto de sequências de validação que exemplificam possíveis execuções do sistema.

Os grupos de trabalho devem estudar o documento de referência referido acima com atenção, por forma a perceberem bem qual é o problema que é abordado. Naturalmente, devido à natureza das ferramentas, aspetos contínuos como o tempo real e a velocidade terão que ser abstraídos. Não é também expectável que cada grupo modele todas as componentes do sistema, ficando à consideração de cada um que aspetos focar. O modelo deve no entanto ser suficientemente rico em estrutura e comportamento, e permitir a verificação de alguns dos requisitos. Algumas sugestões são:

  • Focar-se apenas num sistema (e.g., o de luzes exteriores)
  • Focar-se apenas numa das funcionalidade do sistema (e.g., luzes de direção)
  • Focar-se apenas numa configuração concreta (e.g., mercado EU)

Trabalho 1 sobre Alloy/Electrum

O objetivo deste trabalho é desenvolver um modelo Electrum de (uma parte) deste sistema, assim como um theme que facilite a compreensão das instâncias. Os grupos deverão entregar por email o trabalho até à data limite de 4-Dec-2019 (um modelo Electrum, devidamente comentado, e o respetivo theme).

Trabalho 2 sobre SMV/TLA+

O objetivo deste trabalho é desenvolver um modelo em SMV ou TLA+ de (uma parte) deste sistema. Os grupos deverão entregar por email o trabalho até à data limite de 15-Jan-2020 (um modelo SMV ou TLA+, devidamente comentado).

Bibliografia

Ferramentas

r37 - 05 Nov 2020 - 08:27:21 - AlcinoCunha
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM