System modeling and analysis

A.Y. 2020/2021
Overall hours
Learning objectives
The objective of the course is to introduce methods and techniques for formal specification and verification of complex systems. The course then presents languages for formal specification (operational and denotational) of system requirements and formal verification of temporal logic properties.
Expected learning outcomes
At the end of the course, the student will be able to design a formal specification model for complex systems. The student will also have the ability of modeling through model refinement and have skills on methods and techniques for formal verification of temporal properties.
Course syllabus and organization

Single session

Lesson period
Second semester
Since this is a second semester course, unless further indications from DR, for the AA. 2020/21 lessons will be delivered in presence.

In case of online teaching, lessons will be delivered in synchronous mode through the Microsoft Teams platform. Recorded lessons will also be made available online at the Ariel course website for possible asynchronous use. The individual or group chat services of the course Teams will be used for asynchronous communication between the teacher and students.

The entire teaching material of the course is available on the following Ariel site.
Course syllabus
- Introduction: What are Formal Methods and what they are useful for. Using Formal Methods for systems design and analysis.
- Modeling and analysis at high level of abstraction. The Abstract State Machines (ASM). Model refinement techniques. Model abstraction techniques. The ASMETA tool-set for ASM models. Case studies of system specification.
- Modeling and analysis at low level of abstraction. Kripke Automata and CTL temporal logic: syntax, semantics, specification patterns. Model checking algorithms. Symbolic Model Checking with OBDD. Temporal property verification: properties of reachability, safety, liveness, fairness, deadlock free. Model abstraction: fusion of states, variable abstraction, variable reduction, observer automata. Model refinement: mapping high level abstraction models to low level abstraction temporal models. Tool: NuSMV model checker and AsmetaSMV.
Prerequisites for admission
Passing the exam in Logics is strongly recommended
Teaching methods
Lab activities
Teaching Resources
1) Egon Boerger, Robert Staerk. Abstract State Machines. A Method for High-Level System Design and Analysis. Springer Verlag, 2003.
2) Michael Huth , Mark Ryan. Logic in Computer Science: modelling and reasoning about systems (2nd edition). Cambridge University Press, 2004.
3) B. Berard et al., System and Software Verification Model-Checking Techniques and Tools, Springer Verlag, 2001.

Web site:
Assessment methods and Criteria
The exam consists of a written test and a practical test in the laboratory, both mandatory and both lasting two hours.
The written test focuses on checking the acquisition of skills on the theoretical aspects of the course; the practical test concerns the acquisition of the ability to use software environments for the specification, validation and verification of system properties.
Each test is evaluated in thirtieths and the overall mark is the average of the marks reported in the two tests.

Possible online exams will be taken on the platform, following the indications given at the University website. Both tests (written and practical) will have the same structure of the tests taken in presence, but slightly reduced time.
INF/01 - INFORMATICS - University credits: 6
Lessons: 48 hours
on appointment
Dept. of Computer Science