| Código |
14466
|
| Ano |
1
|
| Semestre |
S2
|
| Créditos ECTS |
6
|
| Carga Horária |
PL(30H)/T(30H)
|
| Área Científica |
Informática
|
|
Objectivos de Aprendizagem |
Os objetivos de aprendizagem gerais consistem em
• Compreender o ciclo de vida de sistemas de software seguros e fiáveis, desde a especificação até à verificação, utilizando técnicas baseadas em formalismos matemáticos (métodos formais).
• Conhecer os métodos e técnicas formais modernos, quando devem ser aplicados e quais são os mais adequados em cada fase dos sistemas de software seguros e fiáveis.
• Aplicar os métodos e técnicas formais na especificação e verificação de sistemas de software seguros e fiáveis.
|
|
Conteúdos programáticos |
• Introdução de linguagens de especificação e programação para construção de software seguro e fiável
• Lógicas para especificação formal: Lógica proposicional, lógica de primeira ordem e lógica temporal
• Técnicas de prova automática: SAT solving para lógica proposicional, SMT solving para lógica e teorias de primeira ordem, Bounded model-checking via SAT para lógica temporal
• Especificação de Programas: Linguagens de domínio para especificação comportamental, propriedades de segurança de execução e propriedades funcionais, especificação com base em contratos
• Verificação estática de programas: condições de verificação para programas com contratos
• Verificação dinâmica de programas: monitorização em tempo de execução com contratos
• Introdução aos métodos formais para sistemas ciber-físicos
|
|
Metodologias de Ensino e Critérios de Avaliação |
A avaliação avaliará a aprendizagem teóricas e prática dos conceitos introduzidos com recurso à resoluções de exercícios que consistem em desafios de desenho de programas correctos e seguros por construção e da demonstração de que esses estão inequivocadamente sem bugs que comprometam a sua segurança.
Fraudes
A equipa docente gostaria de realçar que qualquer tipo de fraude em qualquer dos itens desta disciplina implica a reprovação automática do aluno faltoso, podendo ainda vir a ser alvo de processo disciplinar. Listamos a seguir as diferentes componentes da avaliação.
Nota da avaliação contínua mede a aquisição dos conceitos expostos. Como tal é baseada na realização de três exercícios entregue à equipa docente. Alguns exercícios poderão ter uma parte opcional que, se realizada, poderá valorizar a nota do exercício.
A Nota da Avaliação Contínua (NCP, 20 valores) é a média das notas dos exercícios.
|
|
Bibliografia principal |
Michael Huth & Mark Ryan. Logic in Computer Science: Modelling and Reasoning About Systems. Cambridge University Press; 2nd edition (2004).
Aaron R. Bradley & Zohar Manna. The Calculus of Computation: Decision Procedures with Applications to Verification. Springer (2007).
J.B. Almeida & M.J. Frade & J.S. Pinto & S.M. de Sousa. Rigorous Software Development: An Introduction to Program Verification. Springer (2011).
|
| Língua |
Português
|