Modelação e Validação de Sistemas Concorrentes
Objetivos
1) Compreender, descrever e especificar sistemas concorrentes
2) Expressar propriedades de segurança e vivacidade de sistemas concorrentes
3) Verificar se as propriedades são válidas para as especificações
Caracterização geral
Código
11560
Créditos
6.0
Professor responsável
António Maria Lobo César Alarcão Ravara, Carla Maria Gonçalves Ferreira
Horas
Semanais - 4
Totais - 84
Idioma de ensino
Português
Pré-requisitos
Conhecimento básico de:
1) Programação
2) Lógicas de primeira ordem
3) Teoria de Conjuntos
Bibliografia
Principal:
L. Lamport. The TLA+ Hyperbook http://research.microsoft.com/en-us/um/people/lamport/tla/hyperbook.html
L. Lamport. Specifying Systems. Addison-Wesley, 2002. http://research.microsoft.com/en-us/um/people/lamport/tla/book-02-08-08.pdf
C. Stirling. Modal and Temporal Properties of Processes. Springer, 2001. http://www.springer.com/us/book/9780387987170
Complementar:
L. Aceto et al. Reactive Systems: Modelling, Specification, and Verification. Cambridge University Press, 2007. http://rsbook.cs.aau.dk/
M. Huth and M. Ryan. Logic in Computes Science: modelling and reasoning about systems. Cambridge University Press, 2004. http://www.cs.bham.ac.uk/research/projects/lics/
Método de ensino
As aulas da disciplina consistem em duas horas e uma aula de laboratorial de duas horas.
As aulas teóricas incluem exposição teórica, ilustrada por estudos de caso e apoiada pelo uso de ferramentas de verificação. Nas sessões de laboratório, os alunos resolvem exercícios: modelação de sistemas; especificação e verificação das propriedades do modelo.
A avaliação inclui dois testes e dois trabalhos práticos individuais. Nas duas tarefas, o aluno terá que especificar um sistema concorrente, especificar e verificar um conjunto de propriedades e escrever um relatório.
Condições para obter aprovação: NE> = 9.5 e NT> = 9.5, em que NE é a média das notas dos testes e NT é a nota do trabalho prático.
Método de avaliação
A avaliação é contínua é composta por:
- Componente teórica: 2 testes. A média das notas dos testes terá um peso de 70% na classificação final.
- Componente prática: 2 projetos. A média das notas dos projetos terá um peso de 30% na classificação final.
- Participação nas aulas teóricas e práticas poderão dar um bónus de 10% na classificação final.
Nota: O exame final, quando realizado tanto para aprovação como para melhoria de nota, substitui a componente teórica no cálculo da classificação final.
Para obter frequência à UC é necessário:
- Classificação mínima de 7.0 valores em cada um dos projetos; e
- Média da classificação dos projetos superior ou igual a 9.5 valores.
Nota: Alunos com frequência do ano anterior podem requerer que a classificação de frequência obtida no ano anterior seja considerada este ano.
Para obter aprovação à disciplina é necessário:
- Ter frequência à diciplina, obtida neste ano ou no ano passado;
- Média da componente teórica seja superior ou igual a 9.5 valores; e
- Classificação final seja superior ou igual a 9.5 valores.
Conteúdo
1) Modelação de sistemas concorrentes com TLA+
2) Especificar sistemas com o TLA+
3) Exemplificar com estudos de caso representativos, tais como eating philosophers, bakery algorithm, alternating bit protocol e algoritmos distribuídos (por exemplo, entrega de mensagens causais), tipos de dados abstratos simultâneos etc.
4) Especificar as propriedades desejadas de um sistema (exclusão mútua, deadlock, progresso etc.)
5) Verificar a correcçao de uma especificação TLA +
6) Modelagem de computação simultânea baseada em transição
7) Especificar o comportamento de um sistema com lógicas dinâmicas como CTL *, mu-calculus e Spatial Logics
8) Verificando especificações de lógicas dinâmicas com verificação de modelo (através das ferramentas TAPAs e SLMC)