In English: Lecture notes and slides produced by the teacher, available on the teacher's web page
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.
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:
real-time programming, software engineering, dependability of hardware systems,
discrete mathematics ,
theoretical computer science
Classroom lessons, personal lab exercises
Exam Calendar (the dates listed are for reference for registration and to contact the teacher)
Lun 23-12-2019 C.Didat.Morgagni(1°piano) 11:00 Aula 101
Gio 30-01-2020 C.Didat.Morgagni(1°piano) 11:00 Aula 101
Gio 20-02-2020 C.Didat.Morgagni(1°piano) 11:00 Aula 106
Mar 23-06-2020 C.Didat.Morgagni(1°piano) 11:00 Aula 102
Gio 09-07-2020 C.Didat.Morgagni(1°piano) 11:00 Aula 102
Gio 23-07-2020 C.Didat.Morgagni( p.terra) 11:00 Aula 004
Gio 10-09-2020 Santa Marta (p.terra) 11:00 Aula 120
Type of Assessment
The final exam consists of a project assigned by the teacher, usually to a group of two or three students, followed by an oral test.
The project aims to demonstrate the capabilities of:
- Knowing how to model a distributed system of medium complexity according to the principles of model-based design
- Knowing how to apply model-based design tools and formal verification on the model object of the paper
The oral exam is aimed at assessing the personal knowledge acquired:
Knowledge of the software reliability discipline
Knowledge of distributed algorithms for fault tolerance
Knowledge of formal modeling theory and formal verification of software systems
The course provides 9 CFU.
There is the possibility of attending and giving the exam for 6 CFU, following only the first module
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
Distributed algorithms - concepts of consistency, validity and agreement
Distributed checkpointing and domino effect
Two-phase commit protocol
Principle of uncertainty
Paradox of the Byzantine generals
Byzantine Agreement: the ZA algorithm.
The algorithm of interactive consistency
Blockchain as a distributed consensus algorithm
Distributed clock synchronization algorithms
Formal methods for software development and verification
Axiomatic methods, Z, B
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
Labeled Transition Systems vs. Kripke Structures
Process algebras - CCS - Operational semantics - Observational equivalence
Model Driven Development
UML state diagrams
Model checking on UML state diagrams and on Statecharts
Modelling a system with Statecharts: the Stateflow and Scade 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.
Requirement Engineering: Definition of requirements engineering. Examples of requirements documents. Requirements analysis.
Functional and non-functional requirements, goal-oriented requirements. Requirements analysis process.
Requisite writing techniques: Scenarios, use cases.
Problems of using natural language in the requirements writing.
The ambiguity in the requirements documents.