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, 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 duas Trabalhos de natureza Teórico-prático – um sobre Model Checkers (Tr1) e um sobre provas de programa com Frama-C Tr2 (ou outro framework). Deve ser elaborado um relatório sobre cada um dos temas disponibilizados pelo docente para exploração e uma apresentação da mesmo, com peso de 50% da nota final para cada Trabalho. Nota final : Época Frequência: Nota Tr1 + Nota Tr2 Época Exame: (Nota Tr1 + Nota Tr2)/2 + Nota Exame Escrito.
|
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
|