Modelação e Validação de Sistemas Concorrentes | NOVA Guia de Cursos
Modelação e Validação de Sistemas Concorrentes
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
Conhecimento básico de:
2) Lógicas de primeira ordem
3) Teoria de Conjuntos
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.
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.
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.
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.
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)