Disciplina Curricular
Concepção e Verificação de Sistemas Concorrentes CVSC
Diploma de Estudos Avançados em Segurança de Informação - DEASegInf2007
Peso
7.5 (para cálculo da média)
Objectivos
Projectar e verificar sistemas concorrentes, distribuídos e reactivos utilizando lógica temporal. Utilizar ferramentas computacionais de especificação e verificação.
Programa
Lógica de árvores de computação (CTL): assinatura; linguagem; semântica de árvores de computação; consequência semântica; sistema dedutivo; propriedades de sistemas concorrentes e reactivos. Alternativas e extensões: lógica temporal linear, CTL*. Linguagem abstracta de programação (SMVIL): sintaxe, semântica de sistemas de transições, justiça fraca e forte, ciclo de vida, árvore de computação; satisfação de fórmula por programa; exemplos. Verificação por via semântica: validade de fórmula temporal em sistema finito de transições, algoritmo de Clarke e Emerson, análise da complexidade. Utilização da ferramenta SMV. Aplicações: exclusão mútua; produtores/consumidores; comunicação em canais falíveis; protocolos de comunicação de dados; acordo bizantino; protocolos de troca de chave e de autenticação; comunicação e sincronização de processos em Unix. Outras abordagens: álgebras de processos, estruturas de eventos, redes de Petri. Bissimulação. Adjunções entre categorias de modelos de processos.
Metodologia de avaliação
Projecto (50%) e exame final (50%).