Sumários
L01 - Laboratório sobre Promela
5 outubro 2015, 09:00 • David João Barros Henriques
Apresentação da linguagem de especificação Promela e ao software SPIN. Executabilidade, Tipos de dados, Processos, Instanciação e Parametrização, Asserções, Deadlocks, Condições de Corrida e Sequências Atómicas, Canais Assíncronos, Canais Síncornos, Controlo de Fluxo.
T04 - Propriedades de tempo linear 2
1 outubro 2015, 15:00 • David João Barros Henriques
Invariantes. Verificação de invariantes. Propriedades de segurança. Caracterização alternativa de propriedades de segurança. Relação entre propriedades de segurança e traços finitos. Propriedades de animação. Decomposição de uma propriedade de tempo linear numa propriedade de animação e numa propriedade de segurança.
P02 - Exercícios sobre Sistemas de Transição
28 setembro 2015, 09:00 • David João Barros Henriques
Exercícios sobre especificação de sistemas em Sistemas de Transição. Exercícios sobre Composição Paralela de Sistemas de Transição: Composição Simples, Variáveis Partilhadas, Composição por Sincornização de acções, Composição por canais Partilhados. O problema Dining Philosophers como motivação à Composição Paralela de Sistemas de Transição.
T03 - Propriedades de tempo linear
24 setembro 2015, 15:00 • David João Barros Henriques
Composição por canais Partilhados. Propriedades de tempo linear. Satisfação de propriedades por sistema de transições. Implementações e Abstracções. Equivalência de sistemas de transição.
T02 - Composição de sistemas de transição
21 setembro 2015, 09:00 • David João Barros Henriques
Sistemas de transição. Estado sucessor. Execução. Estado acessível. Caminho. Traço. Grafo de programa. Sistema de transição induzido por grafo de programa. Compoisção paralela de sistemas de transição. Variáveis partilhadas. Composição paralela de grafos de programa. Composição paralela por sincronização de acções (handshake).