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)
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
Bibliografia
- 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 |
|---|
| Daniel Gonçalves Rodrigues | C | a67634 | MiEI | G9 |  |
| Luís Martinho de Aragão Rego da Silva | C | a72205 | MiEI | G9 |  |
| Daniel da Fonte Torres | EC | a70058 | LCC | G8 |  |
| Isac Pereira Oliveira Meira | P | pg31577 | MEI | G8 |  |
| Diana Filipa Oliveira | C | a67652 | MiEI | G7 |  |
| Gil Gonçalves | C | a67738 | MiEI | G7 |  |
| José Paulo Queiroga Amorim Fernandes | P | a72204 | MiEI | G6 |  |
| Mário Jorge Viana Ferreira | P | a70441 | MiEI | G6 |  |
| Hugo Filipe da Silva Ribeiro | P | pg32996 | MEI | G5 |  |
| João Luís Braga Simões Romero | C | pg31384 | MEI | G5 |  |
| Axel da Silva Ferreira | C | a53064 | MiEI | G4 |  |
| Nuno Alberto Pires Fernandes | C | a61066 | MiEI | G4 |  |
| Diogo Filipe da Silva Vilaça | P | a72227 | MiEI | G3 |  |
| José Nuno Castro de Macedo | P | a72424 | MiEI | G3 |  |
| David António Cardoso Moreira | P | a64287 | MiEI | G2 |  |
| Fernanda Raquel Cerdeira Alves | C | a64365 | MiEI | G2 |  |
| João Bernardo Machado Quintas Dias da Costa | P | a70430 | MiEI | G1 |  |
| Rafael Alexandre Antunes Barbosa | P | a71580 | MiEI | G1 |  |
| David Miguel Duarte Rodrigues Alves | C | a53791 | MiEI | (cong) |  |
| Fátima Cristiana da Costa Conceição | P | pg22842 | MMC | (cong) |  |
| Pedro Duarte Cardoso Lopes | C | a32652 | MiEI | (cong) |  |
| Sandra Isabel Lopes Ferreira | P | a67709 | MiEI | (cong) |  |
| Nelson Arieira Parente | C | a71625 | MiEI |
| Ruben Miguel Cunha Santos | C | a70644 | MiEI |
| Saulo Rodrigues e Silva | ? | id5541 | PDINF |
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.
Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.