|
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 |
A avaliação avaliará a aprendizagem teóricas e prática dos conceitos introduzidos nas aulas.
Como tal, esta será constituída por uma prova escrita e pela resoluções de um trabalho prático.
O trabalho prático poderá ser resolvido em grupo de duas pessoas ou individualmente. Cada grupo terá um tema de trabalho definido individualmetne pelo regente da UC. O trabalho deverá ser defendido e valerá metade da nota de avaliação contínua.
A prova escrita a realizar-se no dia 2 de Junho de 2022 no horário da aula teórica valerá a outra metade da nota da avaliação contínua.
Assim, recapitulando, a nota da avaliação contínua é a média da nota do trabalho e da nota da prova escrita.
O aluno é admitido a exame desde que tenha defendido o trabalho e comparecido na prova escrita da avaliação contínua.
O exame consistirá numa prova escrita que substituirá a nota da prova escrita da avaliação contínua.
A nota final será calculada como a média da nota prática e da prova escrita.
|
|
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.
|