You can see a list of the materials provided and exercises done in each lecture here.
This curricular unit aims to familiarize students with the development of safety critical systems, and on the application of formal specification and verification techniques to increase the quality and reliability of software systems.
At the end of the course students should be able to:
- Identify the key concepts and techniques associated with the development and certification of safety critical software-based systems.
- Identify the main concepts and techniques for the formal specification and verification of software-based systems, and recognize their importance and applicability.
- Apply formal verification methods based on model-checking to the design of reactive software systems of small to medium complexity with tool support.
- Apply formal verification methods based on theorem proving and refinement to sequential software systems of small to medium complexity with tool support.
- Introduction to safety critical systems: definition, international standards, life cycle, risk analysis, safety integrity levels, functional safety assurance techniques, fault tolerance.
- Introduction to formal software specification and verification methods: definition, importance, life cycle, techniques.
- Formal verification of reactive system designs by model checking: reactive systems modeling, properties specification in first-order and temporal logic, model checking, tools.
- Formal verification of sequential systems by theorem proving and refinement: Hoare logic, weakest precondition calculus, design by contract, refinement, tools.
- Huth, M., & Ryan, M. Logic in computer science: Modelling and reasoning about systems
- Jackson, D. Software abstractions: Logic, language, and analysis