Description

Theory
2

Laboratory
3

Instructors

Luís Miguel Pinho

Contents

CP1. The critical application verification and validation process
CP2. Contract-based approaches for static and dynamic verification of critical applications.
CP3. Formal specification and verification of critical systems models: principles and tools
 

Learning Outcomes

The successful student should be able to:

CO1. Understand the V&V process of critical applications in order to ensure the correction of functional and non-functional properties of systems and their components.

CO2. Understand the advantages and disadvantages of using different software V&V methods, understand their strengths and weaknesses, and their complementary role in ensuring application correctness.

CO3. Apply annotations to simple imperative programs with formal contracts, including pre- and post-conditions, and cycle variants and invariants, in order to perform tests, flow analysis and verification of programs with contracts;

CO4. Apply, adequately, static analysis methodologies, state machines and model checking tools to verify critical applications.