| 18-2-2016 | Enquadramento da cadeira - o que é arquitectura de software. |
| 25-2-2016 | Estilos arquitecturais e visão de sistemas reactivos. Sistemas de transição e "reachability. CCS (com semântica operacional) e introdução a processos no mCRL2. Equivalência de sistemas de transição por traços. Simulações e bisimulações (fortes). |
| 3-3-2016 | Propriedades de sistemas de transição e de processos (vistos como sistemas de transição). Bissimulações "branching" e fracas. Pequena contextualização à lógica. |
| 10-3-2016 | Lógicas modais: sintaxe, semântica, exemplos (inlcuindo a lógica de Hennessy-Milner e lógicas temporais). |
| 17-3-2016 | Relação com a lógica de 1a ordem. Relação entre sistemas caracterizados por fórmulas modais e bissimulações. Verificação usando mCRL2. |
| 24-3-2016 | Férias da Páscoa. |
| 31-3-2016 | Lógicas temporais em mais detalhe. Lógicas híbridas e sua semântica. Introdução a sistemas de tempo real. Definição de automato de tempo real e da sua representação no Uppaal. Composição de automatos de tempo real. |
| 7-4-2016 | Semântica de automatos de tempo real (TA). Traços "time-convergent", "timelock", e "zeno". Extensões aos TA no Uppaal. |
| 14-4-2016 | Equivalência de TAs, incluindo noções de bissimulação. Verificação usando lógica temporal no Uppaal. |
| 21-4-2016 | Exclusão mútua no Uppaal. Introdução a sistemas de coordenação. Reo: motivação, syntaxe, e ferramentas. |
| 28-4-2016 | Semânticas do Reo: Connector Colouring 2, Port Automata, their (formal) relation, and reo as mCRL2 processes. |
| 5-5-2016 | Mais semânticas baseadas em automatos do Reo. Contexto e connector colouring 3. |
| 12-5-2016 | Enterro da gata. |
| 19-5-2016 | Demonstrações do 2º trabalho. Exemplos de conectores em Reo. |
| 9-6-2016 | Teste de avaliação. |
| 16-6-2016 | Demonstrações do 3º trabalho. |
| 30-6-2016 | Exame de recurso. |