| Código |
15646
|
| 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 gerais são:
• Perceber e dominar o ciclo de vida do desenvolvimento de sistemas informáticos seguros e fiáveis baseado em Métodos Formais.
• Conhecer os métodos formais existentes, saber quando devem ser aplicados e quais são os mais adequados em cada caso.
• Aplicar os Métodos Formais de especificação e verificação no desenvolvimento de sistemas informáticos seguros e fiáveis.
• Saber selecionar, aplicar mas também desenvolver métodos de análise estática de programas.
|
|
Conteúdos programáticos |
1. Métodos formais em engenharia de software
2. Análise de fluxo de dados
3. Path Sensitivity, análise interprocedural e análise de fluxo de controlo
4. Lógica temporal (temporizada), verificação de modelos temporizados,
5. Verificação de modelos com UPPAAL
6. Semântica operacional para a verificação
7. Semântica denotacional, de traços
8. Semântica axiomática, Lógica de Hoare e Weakest precondition calculus
9. Verificação dedutiva de programas
10. Verificação formal e provas de programas comn Frama-C
|
|
Metodologias de Ensino e Critérios de Avaliação |
As aulas presenciais são divididas em duas categorias:
1. Aulas Teóricas onde são expostos os conceitos teóricos, os modelos matemáticos próprios à construção/validação/analise de software, os algoritmos subjacentes mas também as tecnologias capacitativas à produção de software fiável e seguro.
2. Aulas Práticas com aplicação das técnicas de especificação e de verificação de programas.
Por fim a avaliar as competências adquiridas, as atividades de Ensino-Aprendizagem avaliará a compreensão dos conceitos teóricos expostos e a capacidade em por estes em prática. Assim, será realizada por uma prova escrita e por 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 = if (NCT >= 6 e NCP >= 6) then (NCT + NCP)/2 else Reprovado/Não Admitido
|
|
Bibliografia principal |
J.B. Almeida, M.J. Frade, J.S. Pinto, and S. Melo de Sousa. Rigorous Software Development, An Introduction to Program Verification, volume 103 of Undergraduate Topics in Computer Science. Springer-Verlag, 2011.
Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci, and Philippe Schnoebelen. Systems and Software Verification. Model-Checking Techniques and Tools. Springer, 2001.
E.M. Clarke, O. Grumberg, and D Peled. Model Checking. MIT press 2000
J. Cooke. Constructing correct software. Formal approaches to computing and information technology. Springer Verlag, 2005.
ACSL by Example. Towards a Formally Verified Standard Library for Frama-C 22.0 November 2020, Jens Gerlach
Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, Boris Yakobowski Frama-C, A Software Analysis Perspective In Formal Aspects of Computing, vol. 27 issue 3, 2015
Introduction to C program proof with Frama-C Allan Blanchard July 1, 2020 ebook.
|
| Língua |
Português
|