In English: Lecture notes and slides produced by the teacher, available on Moodle
Learning Objectives
The current ubiquity of software, particularly inside objects that can have an impact on economy or on safety of people, prompts the need that software is bug-free.
This course wants to show a series of techniques that help avoiding the introduction of design errors in software production: mainly, formal development and verification techniques, but also fault forecasting and fault tolerance techniques.
The introduction of such techniques in a production context will be studied, and the relationships with guidelines of specific industrial production domains will be discussed.
The course aims in particular to provide:
Knowledge of the discipline of software reliability
Knowledge of the main formal methods
Knowledge of model-based design principles
Knowledge of the theory and techniques of formal verification of software systems
Prerequisites
It is a necessary prerequisite for the course
knowledge of programming techniques, particularly in C language.
In addition, for the learning of specific notions, it will be useful to have prior knowledge in:
operating systems,
real-time programming, software engineering, dependability of hardware systems,
discrete mathematics ,
theoretical computer science
Teaching Methods
Classroom lessons, personal lab exercises
Further information
Exam Calendar:
TBD
Dates and hours are for reference only. Please contact the teacher in advance.
Type of Assessment
The final examination consists of an oral test
The oral test is aimed at assessing the personal knowledge acquired:
Knowledge of the discipline of software reliability
Knowledge of formal modelling theory
Knowledge of the principles and tools of formal verification of software systems
Course program
Recalls on the concepts of dependability of computer-controlled systems
Measures for software dependability
Software reliability: estimation models
Tolerance to software failures: Forward / Backward error recovery
Formal methods for software development and verification
Axiomatic methods, Z, B
Modal Logic
Temporal Logic
LTL - safety / liveness properties, fairness properties
Recurrence, minimum and maximum fixed point properties
Branching logics - CTL - interpretation on Kripke Structures - CTL *
Model Checking Algorithm for CTL
State space explosion
Binary Decision Diagrams (BDD) as a compact state space representation technique
Model checking algorithm based on fixed point
Algoritmo di model checking basato su punto fisso
Buchi automata - Model checking algorithm for LTL
Local model checking
Bounded Model Checking, using SAT solvers
Model Driven Development
UML state diagrams
Model checking on UML state diagrams and on Statecharts
Modelling a system with Statecharts: the Stateflow and UML dialects.
Model checking tools: SMV, SPIN, UMC
Abstract Interpretation. Static analysis using Abstract Interpretation. Industrial usage.
Introduction to Software model checking; translation approach.
Software Model checking. Abstraction criteria: over-approximation, under-approximation.
Introduction to Probabilistic Model Checking and Statistical Model Checking.