| 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 |
Para avaliar as competências adquiridas, as atividades de ensino-aprendizagem avaliam a compreensão dos conceitos teóricos apresentados e a capacidade de os pôr em prática. Esta avaliação será efetuada através de um teste escrito e de uma avaliação contínua baseada em exercícios práticos.
NF = Nota final
NCP = Nota da componente prática (avaliação dos exercícios)
NCT = Nota da componente teórica (prova escrita - exame ou frequência)
NF = Se (NCT >= 6 e NCP >= 6) então (NCT + NCP)/2, caso contrário Reprovado/Não Admitido
|
|
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
|