Teachers:

• Luca Tesei
• Franco Raimondi visiting Professor from Middlesex University London

Lectures schedule:

• Wednesday, 5pm - 7pm (Room D. M. Ritchie)
• Thursday, 3pm - 5pm (Room D. M. Ritchie)

Please see “Course Organization” below for the actual scheduling of the lectures

Office hours:

• Luca Tesei's office hours are every Wednesday from 11 am to 1 pm in room CS 07, second floor of Polo Tecnologico Palazzo Battibocca, via del Bastione 1, Camerino. For any variation, first look here
• From 13th June 2016 Luca Tesei's office hours schedule can be found here.
• Prof. Franco Raimondi will be available during his visiting period at Palazzo Battibocca (precise office hours will be communicated)

KNOWLEDGE

At the end of the course, the student should be able to:

• Understand the concept of verification of a concurrent system and the main issues related to the model checking problem of reactive systems
• Define the formalism of transitions systems for modelling concurrent systems also using more higher level concepts such as state variables and communication channels
• Illustrate the concepts of parallel composition, interleaving, synchronous communication, synchronized product between transition systems
• Have knowledge of the type of properties that can be expressed on a trace of a transition system: safety, liveness or mixed properties
• Illustrate the concept of fairness of actions in the three variants: unconditional, strong and weak
• Have knowledge of the main concepts of automata theory applied to system verification, in particular the algorithms for verifying regular safety properties and omega-regular properties
• Define the Linear Time Logic (LTL) and illustrate the automata-based algorithms for the model checking of an LTL formula
• Define the Computation Tree Logic (CTL) and the extended version CTL^* and illustrate the main algorithms for the model checking of a CTL formula

APPLYING KNOWLEDGE AND UNDERSTANDING

At the end of the course, the student should be able to:

• Model a concurrent reactive system using a component-based approach
• Define finite state machines with a suitable synchronization interface using both a graphical language and a textual language (e.g. Promela)
• Apply standard algorithms for the fundamental operations (intersection, union, complementation, synchronized product) to finite state automata
• Formally express properties of reactive systems using automata on infinite words, LTL formulas and CTL/CTL^* formulas
• Apply the concept of fairness, in its variants, to real cases
• Apply to finite models the main algorithms for the automata-based verification of properties expressed in LTL and CTL/CTL^*
• Use in an effective way available software tools for model checking (e.g. SPIN or JPF)

MAKING JUDGEMENTS

At the end of the course, the student should be able to:

• Identify the best model suitable for describing a system using a given formalism

COMMUNICATION SKILLS

At the end of the course, the student should be able to:

• Write a clear report on the modelling and analysis of a system under study using a formal style

LEARNING SKILLS

At the end of the course, the student should be able to:

• Search the scientific literature for specific advances in formalisms and tools aimed at modelling and verifying untimed and real-time systems
• Autonomously understand and learn to use new features added to tools for modelling and verifying reactive systems

• System verification: main concepts. Definition and characteristics of model checking.
• Transition Systems. Program Graphs and Channel Systems. Parallelism and communication. The language Promela.
• Linear-time properties: safety, liveness, fairness.
• Regular safety properties and their verification. Automata on infinite words. Omega-regular properties and their verification.
• Linear Temporal Logic (LTL). Automata-based LTL model checking.
• The tool JPF: Java Path Finder.
• Computation Tree Logic (CTL). CTL model checking.

In order to adapt the scheduling to the intensive part of the course given by visiting Prof. Raimondi, the actual scheduling of lectures is as follows. Note that the following dates do not correspond to every scheduled lecture in timetable.

• Wed 02/03/2016 5pm-7pm Prof. Tesei
• Thu 10/03/2016 3pm-5pm Prof. Tesei
• Wed 16/03/2016 5pm-7pm Prof. Tesei
• Thu 17/03/2016 3pm-5pm Prof. Tesei
• Wed 23/03/2016 5pm-7pm Prof. Tesei
• Wed 30/03/2016 5pm-7pm Prof. Tesei
• Thu 31/03/2016 3pm-5pm Prof. Tesei
• Wed 06/04/2016 5pm-7pm Prof. Tesei
• Thu 07/04/2016 3pm-5pm Prof. Tesei
• Wed 13/04/2016 5pm-7pm Thu 14/04/2016 3pm-5pm Prof. Tesei
• Thu 21/04/2016 3pm-5pm Prof. Tesei
• Wed 27/04/2016 5pm-7pm Thu 28/04/2016 3pm-5pm Prof. Tesei
• Wed 04/05/2016 5pm-7pm Thu 05/05/2016 3pm-5pm Prof. Tesei

From Thu 12/05/2016 to Wed 25/05/2016 Prof. Franco Raimondi will give the following lectures:

• Thu 12/05/2016 3pm-7pm Room D. M. Ritchie
• Fri 13/05/2016 11am-1pm Room D. M. Ritchie
• Mon 16/05/2016 5pm-7pm Room D. M. Ritchie
• Tue 17/05/2016 5pm-7pm Room R. Milner
• Thu 19/05/2016 3pm-7pm Room D. M. Ritchie
• Mon 23/05/2016 3pm-6pm Room D. M. Ritchie
• Tue 24/05/2016 5pm-7pm Room R. Milner
• Wed 25/05/2016 5pm-7pm Room D. M. Ritchie

Course Slides

Specification of Models

• General Introduction Slides - 2nd March 2016
• Introduction to Model Checking - 2nd March 2016
• Transition Systems - 10th March 2016
• Modelling Hardware Circuits - 10th March 2016
• Program Graphs - 10th March 2016 + 16th March 2016
• Guarded Commands Language - 16th March 2016
• Parallelism. Interleaving for Transition Systems - 16th March 2016
• Parallelism. Interleaving for Program Graphs - 17th March 2016
• Parallelism and Communication. Synchronous Message Passing - 17th March 2016
• Parallelism and Communication. Channel Systems - 23rd March 2016
• Parallelism and Communication. Synchronous Product - 23rd March 2016

Exercises on Models and Modelling

• Exercises with (some) solutions - 17th March 2016 and 23rd March 2016 (Partial)
• Promela Language and SPIN Model Checker - Check this out!
• SpinRCP Front-end to SPIN - Check this out!

Linear Time Properties

• Linear Time Properties. Introduction. - 30th March 2016
• Linear Time Properties. Definition and Satisfaction. Trace Equivalence - 30th March 2016
• Linear Time Properties. Invariants and Invariant Checking. - 31st March 2016
• Linear Time Properties. Safety Properties. Bad Prefixes and Prefix Closure. - 31st March 2016
• Linear Time Properties. Liveness Properties. - 31st March 2016
• Linear Time Properties. Decomposition Theorem. - 31st March 2016
• Linear Time Properties. Fairness. - 6th April 2016
• Linear Time Properties. Regular Safety Properties. - 7th April 2016 (Partial), 14th April 2016
• Linear Time Properties. Omega-Regular Properties. - 14th April 2016 (Partial), 21st April 2016
• Model Checking with Buchi Automata - 28th April 2016

Exercises on Linear Time Properties

• Exercises with (some) solutions on Linear Time Properties, Safety/Liveness, Fairness - 31st March 2016, 6th April 2016, 7th April 2016
• Exercises with (some) solutions on Regular Properties - 28th April 2016 (Partial), 5th May 2016
• Exercises with (some) solutions on LTL (Partial overlap with the second part of the course)

Linear Temporal Logic

• Revision of propositional and predicate logic with examples of SAT solvers - 13 May 2016
• LTL syntax and semantics - 13 May 2016
• LTL to Buchi - 16 May 2016

Exercises on Linear Temporal Logic

• LTL exercises

Computational Tree Logic

• CTL syntax and semantics - 17 May 2016
• CTL model checking and OBDDs - 19 May 2016

Tools and practical applications

• NuSMV - 23 May 2016
• Spin - 23 May 2016
• JPF - 24 May 2016
• SMT, Z3, Concolic testing, DO178 - 25 May 2016

Reference books

• Christel Baier, Joost-Pieter Katoen, “Principles of Model Checking”, The MIT Press, 2008, ISBN: 9780262026499. Website of the book with additional material available here
• Michael Huth, Mark Ryan, “Logic in Computer Science”, Second Edition, Cambridge University Press, 2004. ISBN: 9780521543101.
• Lecture notes and slides may be given by the teachers for studying and for exercises. These can be downloaded from the section above

Other Books

• Luca Aceto, Anna Ingólfsdóttir, Kim Guldstrand Larsen, Jiri Srba, “Reactive Systems”, Cambridge University Press, ISBN: 9780521875462, Book Website

Assignments:

• Text of Assignment 1. Deadline to return the homework by email is Friday 29th April 2016 at 23.59 - Solutions
• Text of Assignment 2. Deadline to return the homework by email is Friday 10th June 2016 at 23.59 - Solutions not available yet.
• Text of Assignment 3. Deadline to return the homework by email is Friday 24th June 2016 at 23.59 - Solutions

Exam Dates A.Y. 2015/2016

1. Thursday 16/06/2016 3.00pm, Room TBA
2. Thursday 30/06/2016 3.00pm, Room TBA
3. Thursday 14/07/2016 3.00pm, Room TBA
4. Thursday 08/09/2016 3.00pm, Room TBA
5. Thursday 22/09/2016 3.00pm, Room TBA
6. Thursday 06/10/2016 3.00pm, Room TBA
7. Thursday 09/02/2017 3.00pm, Room TBA
8. Thursday 23/02/2017 3.00pm, Room TBA

Exam rules: The exam consists of a written test containing open-answer and/or closed-answer questions. Mini projects and/or assignments will be communicated during the lectures. Students sending the projects/assignments on time will be given a mark and the possibility to skip parts of the written test. During the exercises sessions throughout the course samples of the written test questions will be presented with solution.

Registration for the written tests must be done using the Student Career System ESSE3 here. Please note that the registration deadline is usually 3 days before the written test date (the Monday before). BSc students or MSc students who did not select the Software Modelling and Verification (SMV) Curriculum will not be able to register for the written test until they communicate to the Secretary Office (Tiziana Jajani c/o Polo degli Studenti, Via Pieragostini 18, Camerino Opening Hours) their choice to attend to this course, code [ST1046] MODEL CHECKING I.

Exam Results

• The results will be communicated through the Student Career System ESSE3.
• Contextually to the communication of the results students will be invited to a meeting to look at the corrected test.

Prof. Franco Raimondi is one of the mentors for projects about Java Path Finder (JPF) during Google Summer of Code. The contents of this course include JPF and its usage for verification.

Students who want to participate should contact Prof. Raimondi as soon as possible to start working on the proposal. More information on the timeline of the event is here.