In English: Lecture notes and slides produced by the teacher, available on the teacher's web page
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.
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, distant lessons (for COVID emergency), personal lab exercises
Further information
Exam Calendar:
I appello 07/01/2021 10:00
II appello 21/01/2021 11:00
III appello 11/02/2021 11:00
IV appello 22/06/2021 11:00
V appello 08/07/2021 11:00
VI appello 22/07/2021 11:00
Dates and hours are for reference only. Please contact the teacher in advance.
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
Course program
The course provides 9 CFU.
There is the possibility of attending and giving the exam for 6 CFU, following only the first module
Module 1
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
Stable memory
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
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
Labeled Transition Systems vs. Kripke Structures
Process algebras - CCS - Operational semantics - Observational equivalence
ACTL Logic
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
Module 2
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.
Requirements Traceability