Especificação e Modelação

Classificações do exame da época especial:

a64287 = R; pg22842 = R.

Classificações finais:

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
12-Jan-2017	Teste	PDF (com a correcção de algumas perguntas)
26-Jan-2017	Exame de recurso	PDF

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

• Alloy
• NuSMV

Exemplos / bibliotecas Alloy

• Módulo Alloy: RelCalc.als - Cálculo relacional básico em Alloy.

• Eu sou o meu próprio avô (avo.als e avo.thm).

Desafios Alloy

• Barqueiro
• Unidades Curriculares de Especialização
• Agenda telefónica
• Leilões

Alunos

Nome	P/C	Nr	Curso	Grupo	Fot
Nelson Arieira Parente	C	a71625	MiEI
Ruben Miguel Cunha Santos	C	a70644	MiEI
Saulo Rodrigues e Silva	?	id5541	PDINF
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)
João Bernardo Machado Quintas Dias da Costa	P	a70430	MiEI	G1
Rafael Alexandre Antunes Barbosa	P	a71580	MiEI	G1
David António Cardoso Moreira	P	a64287	MiEI	G2
Fernanda Raquel Cerdeira Alves	C	a64365	MiEI	G2
Diogo Filipe da Silva Vilaça	P	a72227	MiEI	G3
José Nuno Castro de Macedo	P	a72424	MiEI	G3
Axel da Silva Ferreira	C	a53064	MiEI	G4
Nuno Alberto Pires Fernandes	C	a61066	MiEI	G4
Hugo Filipe da Silva Ribeiro	P	pg32996	MEI	G5
João Luís Braga Simões Romero	C	pg31384	MEI	G5
José Paulo Queiroga Amorim Fernandes	P	a72204	MiEI	G6
Mário Jorge Viana Ferreira	P	a70441	MiEI	G6
Diana Filipa Oliveira	C	a67652	MiEI	G7
Gil Gonçalves	C	a67738	MiEI	G7
Daniel da Fonte Torres	EC	a70058	LCC	G8
Isac Pereira Oliveira Meira	P	pg31577	MEI	G8
Daniel Gonçalves Rodrigues	C	a67634	MiEI	G9
Luís Martinho de Aragão Rego da Silva	C	a72205	MiEI	G9

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?