Especificação e Modelação
Classificações do exame da época especial:
a64287 = R; pg22842 = R.
Classificações finais:
(Apenas dos alunos avaliados):a32652 = 10; a53791 = 10; a64287 = R; a64365 = R; a67652 = F; a67709 = 10; a70058 = F; a70430 = 14; a70441 = 10; a70644 = F; a71580 = 13; a71625 = F; a72204 = 11; a72205 = R; a72227 = 11; a72424 = 14; pg22842 = F; pg31577 = 10; pg32996 = R.
Método de avaliação
- Teste individual escrito (70%, ≥ 8)
- Trabalho de grupo (30%, ≥ 10)
- Presença obrigatória nas aulas
Enunciados de provas escritas de avaliação (T)
| Data | Descrição | Ficheiro |
|---|---|---|
| 26-Jan-2017 | Exame de recurso | |
| 12-Jan-2017 | Teste | PDF (com a correcção de algumas perguntas) |
Enunciado do Trabalho (TP)
Introdução - Nesta disciplina foram estudados métodos de especificação, modelação e raciocínio para a produção de software de alta fiabilidade. Todos os sistemas de segurança-crítica exigem software fiável, por exemplo nos equipamentos médicos, nos transportes aéreos, etc. A norma de certificação DO-178B é uma diretriz sobre segurança do software crítico destinado à aviação.
O artigo Modelling an Aircraft Landing System in Event-B, que 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, é o ponto de partida para este trabalho.
O que é para fazer - 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 o mesmo modelo em Alloy, de forma o mais simples possível. Note-se que não se pretende uma tradução à letra do modelo dado, mas antes um modelo independente e simplificado. Mais do que a quantidade, valorizar-se-á a qualidade e a capacidade de abstracção.
Prazos e "deliverables" - os grupos deveram entregar, até à data limite de 31-Jan-2017, um pequeno relatório (em inglês) onde conste o código Alloy que desenvolveram. Deverão também preparar uma apresentação do seu trabalho (slides) prevista para (no máximo) 10 minutos. As orais destas apresentações decorrerão de 1 a 10 de Fevereiro.
Os alunos deverão estar atentos a esta página quanto a prováveis esclarecimentos sobre este trabalho que os inicia na aplicação de métodos formais a problemas reais. Bom trabalho!
Material pedagógico
- Modeling, Specification, and Verification: slides introdutórios.
- Exercícios sobre SMV: as questões marcadas com CTL requerem conhecimento sobre lógica temporal CTL que ainda não foi leccionada este ano.
- Exemplos SMV: barqueiro, cadeira pesada, algoritmo de exclusão mútua de Peterson (sem módulos e com módulos).
- A perspective on Model Checking. Estes slides sobre model checking abarcam muito mais matéria do que a que será leccionada este ano, mas podem ser úteis para quem desejar saber mais sobre este assunto (ver bibliografia no final). Em particular, este ano usamos SMV e não Petri Nets como linguagem de modelação.
- J.N. Oliveira. Specification and modelling: where everything becomes a relation
(versão de 20-Nov-16, 130 slides).
Bibliografia
- D. Jackson. Software abstractions: logic, language, and analysis. Revised edition, MIT Press, 2012.
- C.B. Jones. Systematic Software Development Using VDM. Series in Computer Science. Prentice-Hall International, 1986 (first edition). (345 pages)
Ferramentas
Exemplos / bibliotecas Alloy
- Módulo Alloy: RelCalc.als - Cálculo relacional básico em Alloy.
Desafios Alloy
Alunos
| Nome | P/C | Nr | Curso | Grupo | Fot |
|---|---|---|---|---|---|
| Axel da Silva Ferreira | C | a53064 | MiEI | G4 |  |
| Daniel Gonçalves Rodrigues | C | a67634 | MiEI | G9 |  |
| Daniel da Fonte Torres | EC | a70058 | LCC | G8 |  |
| David António Cardoso Moreira | P | a64287 | MiEI | G2 |  |
| David Miguel Duarte Rodrigues Alves | C | a53791 | MiEI | (cong) |  |
| Diana Filipa Oliveira | C | a67652 | MiEI | G7 |  |
| Diogo Filipe da Silva Vilaça | P | a72227 | MiEI | G3 |  |
| Fernanda Raquel Cerdeira Alves | C | a64365 | MiEI | G2 |  |
| Fátima Cristiana da Costa Conceição | P | pg22842 | MMC | (cong) |  |
| Gil Gonçalves | C | a67738 | MiEI | G7 |  |
| Hugo Filipe da Silva Ribeiro | P | pg32996 | MEI | G5 |  |
| Isac Pereira Oliveira Meira | P | pg31577 | MEI | G8 |  |
| José Nuno Castro de Macedo | P | a72424 | MiEI | G3 |  |
| José Paulo Queiroga Amorim Fernandes | P | a72204 | MiEI | G6 |  |
| João Bernardo Machado Quintas Dias da Costa | P | a70430 | MiEI | G1 |  |
| João Luís Braga Simões Romero | C | pg31384 | MEI | G5 |  |
| Luís Martinho de Aragão Rego da Silva | C | a72205 | MiEI | G9 |  |
| Mário Jorge Viana Ferreira | P | a70441 | MiEI | G6 |  |
| Nelson Arieira Parente | C | a71625 | MiEI | ||
| Nuno Alberto Pires Fernandes | C | a61066 | MiEI | G4 |  |
| Pedro Duarte Cardoso Lopes | C | a32652 | MiEI | (cong) |  |
| Rafael Alexandre Antunes Barbosa | P | a71580 | MiEI | G1 |  |
| Ruben Miguel Cunha Santos | C | a70644 | MiEI | ||
| Saulo Rodrigues e Silva | ? | id5541 | PDINF | ||
| Sandra Isabel Lopes Ferreira | P | a67709 | MiEI | (cong) |  |
Atendimento electrónico (FAQs)
(Esta secção será actualizada regularmente com as dúvidas mais frequentes que forem colocadas à equipa docente.)
- Q1 - Tenho dificuldade em decorar a diferença entre núcleo e imagem de uma relação. Há alguma mnemónica que possa ajudar?
R: Haverá concerteza muitas, por exemplo: decore o nome feminino "NEIDE" e leia-o como o acrónimo de "Núcleo, Esquerda, Imagem, Direita, Etc", isto abreviatura de "num núcleo Rº.R o converso está à esqerda, numa imagem R.Rº está à direita, etc". Haverá melhores, mas este já pode ajudar.
- Q2 - Se eu tiver <∀ a,b : a X b : a=b> posso trocar para <∀ a,b : a=b : aXb> e depois aplicar 'one point', correcto?
R: Não (!) Isso é se o quantificador for o existencial (∃). No caso do universal, a troca possível é de <∀ a,b : a X b : a=b> para <∀ a,b :: a X b => a=b>, cf. a regra Trading (∀) dos slides, para R = true.