Aula 1/2 16/02
Objectivos da disciplina e tópicos do programa. Métodos de avaliação. Bibliografia recomendada.
Breve introdução aos métodos formais para o desenvolvimento de sistemas informáticos.
Introdução ao Model checking. Sistemas de transição. Execuções. Modelação de circuitos sequências e programas.
Bibliografia: Cap. 1 e 2 RSD, Slides, Cap 1 , 2.1 PMC
Exercícios: Folha 1 1-2
—————————————————————————————————————————————————————
Aula 3/4 23/02
Paralelismo e Comunicação. Concorrência e Intercalagem. Comunicação por variáveis partilhadas. Handshaking. Protocolos de Exclusão Mútua.
Bibliografia: Cap 2.2.1-2.2.3 PMC
Exercícios: Folha 1 3-6
—————————————————————————————————————————————————————
Aula 5/6 02/03
Paralelismo e Comunicação (cont.). Passagem de mensagens síncronas e assíncronas. Sistestemas de canais e sistemas de transição associados. Produto síncrono. Problema da explosão do número de estados. Introdução à linguagem Promela e ao model Checker SPIN.
Bibliografia: Cap 2.2.4-2.2.7 PMC; PMCSPIN
Exercícios: Folha 1 7 e estudar Promela
—————————————————————————————————————————————————————
Aula 7/8 9/03
Propriedades Temporais Lineares (LT). Deadlock. Caminhos e Traços. Invariantes e propriedades de segurança. Propriedades de vivacidade. Classificação de propriedades LT. Justeza.
Bibliografia: Cap 3 PMC
Exercícios: Folha 2