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 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 modelaçã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 |
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 |
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
|