Métodos Formais em Engenharia de Software

Mestrado Integrado em Engenharia Informática [17/18]

Tópicos

Avisos

4 Fev - tinynew.gif As notas finais de UC2 - CSI já se encontram na respectiva página. Os exames podem ser consultados dia 6 de Fevereiro às 15:00 no gabinete do docente.

30 Jan - tinynew.gif As notas finais de UC1 - EM já se encontram na respectiva página. Os exames podem ser consultados dia 2 de Fevereiro às 14:00 no gabinete do docente.

25 Jan - A aula de dúvidas de UC2 - CSI já está narcada no calendário (30-Jan de tarde, na sala do costume).

24 Jan - A hora do exame de UC1 - EM foi alterada para as 9h00 do dia 25 de Janeiro (sala CP2 111).

24 Jan - A hora do exame de UC2 - CSI foi alterada para as 11h00 do dia 1 de Fevereiro (sala CP2-105).

18 Jan - A entrega do trabalho de Alloy foi adiada para o dia 21 de Janeiro.

18 Jan - As notas do teste de UC1 - EM já se encontram na respectiva página. Os testes podem ser consultados dia 19 de Janeiro às 14:00 no gabinete do docente.

10 Jan - As notas do teste de UC2 - CSI já se encontram na respectiva página.

8 Jan - Colocados na página de CSI os enunciados das provas de avaliação com propostas de resolução .

4 Jan - A aula suplementar de hoje terá lugar na sala DI 1.09

23 Dez - As notas do miniteste de UC2 - CSI já se encontram na respectiva página.

11 Dez - As aulas de reposição do dia 13, 4ª feira, serão na Sala de Reuniões do DIUM do 3º andar (não foi possível obter nenhuma sala comum, está tudo cheio nesse dia).

11 Dez - Preparação em casa ('Flipped Classroom') das aulas de CSI desta semana (2 dias): ler até ao slide 172 (para 4ª-feira) e daí fazer os exercícios que estão nesta folha.

04 Dez - CSI: sessão de dúvidas - amanhã à tarde, após as 16h30, o docente estará disponível para tirar dúvidas para o mimi-teste.

03 Dez - CSI: pf vejam as FAQs que vão aparecendo ao fundo da página de CSI.

27 Nov - CSI: Por colisão de agenda com um júri da FEUP em que o docente participa, o miniteste terá que ser adiado 1 semana. Esta semana apenas permanece a aula T das 17h-18h.

13 Nov - As aulas de reposição da próxima 4ª-feira dia 15 terão lugar no Anfiteatro DI-1.01 (vulg. A2).

12 Out - Preparação em casa das aulas de CSI desta semana (2 dias): ler até ao slide 114 e preparar os exercícios 28-31 e 43-44. NB: há uma nova versão dos slides, com algumas alterações (204 slides no total).

29 Out - Preparação em casa da aula de CSI desta semana: ler até ao slide 92 e preparar os exercícios 19, 21, 22 e

16 Out - Preparação em casa da aula de CSI desta semana: ler até ao slide 62 e preparar os exercícios 7, 8, 12, 14 e 15.

7 Out - Preparação em casa da aula de CSI da próxima semana: ler até ao slide 44 e estudar os exercícios 1 e 4.

30 Set - Os slides de UC2 - CSI já estão disponíveis.

22 Set - Idealmente, na próxima aula de UC1 - EM devem já trazer a ferramenta NuSMV instalada.

19 Set - As aulas da disciplina UC2 - CSI só se iniciam a 28-Set (docente esta semana em missão no estrangeiro).

17 Set - Início das aulas: 19-Set.

09 Set - Aguarda-se informação da Direcção de Curso sobre data do início das aulas das disciplinas deste perfil.

06 Set - Slides da apresentação do perfil.

Especificação e Modelação

Docente e horário

Docente Foto Horário Sala
Manuel Alcino Cunha mac 5a-feira, 9h-12h Sala 1.16 (antiga 1.08)

Método de avaliação

  • Teste individual escrito (70%, ≥ 8). Enunciado do teste e do exame.
  • Trabalho de grupo (30%, ≥ 10)

Notas

Enunciado do trabalho sobre NuSMV

O artigo Modelling an Aircraft Landing System in Event-B descreve a modelação formal de um sistema de controlo do trem de aterragem de um avião baseado nos requisitos impostos pela Federal Aviation Administration dos EUA. Neste artigo o trem de aterragem é modelado a níveis diferentes de abstracção, dando origem a vários modelos nomeados M1, M2, M3, etc, com cada vez mais detalhe.

Os grupos de trabalho devem estudar o artigo acima referido com atenção por forma a perceberem bem qual é o problema que é abordado. Ao mesmo tempo, deverão informar-se sobre a linguagem de modelação Event-B, mas apenas na medida do que é necessário para perceberem o artigo. O que se pretende neste trabalho é exprimir os diferentes modelos M1, M2, M3, etc, usando o NuSMV em vez de Event-B. O nível de detalhe a atingir fica à consideração de cada grupo.

Os grupos deveram entregar por email o trabalho até à data limite de 15-Dez-2017 (um ficheiro zip com todos os modelos desenvolvidos, devidamente comentados).

Enunciado do trabalho sobre Alloy

O Monopólio é um dos jogos de tabuleiro mais populares em todo o mundo. O objectivo deste trabalho é fazerem um modelo Alloy deste jogo, cujas regras podem ser encontradas aqui. Naturalmente, por questões de eficiência na análise será necessário abstrair certos aspectos do jogo (por exemplo, a configuração exacta do tabuleiro ou os valores monetários envolvidos nas transacções), podendo cada grupo escolher diferentes aspectos a abstrair. Fica também à consideração de cada grupo a escolha do idioma de Alloy a usar na modelação da dinâmica do jogo, assim como a escolha das propriedades a verificar. Finalmente, os grupos devem também desenvolver um theme que facilite a compreensão das instâncias.

Os grupos deveram entregar por email o trabalho até à data limite de 21-Jan-2018 (um modelo Alloy, devidamente comentado, e o respectivo theme).

Material pedagógico

Bibliografia

Ferramentas

r17 - 30 Jan 2018 - 09:38:36 - AlcinoCunha
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM