Reactive Systems Verification

Teacher:

• Luca Tesei

Lectures schedule:

• Wednesday, 2pm - 4pm @ Room AB3, 1st floor, Polo Lodovici, via Madonna delle Carceri 9, Camerino.
• Thursday, 9am - 11am @ Room AB3, 1st floor, Polo Lodovici, via Madonna delle Carceri 9, Camerino.

Webex Room for Lecture Streaming

• Luca Tesei's room

Office hours:

• Luca Tesei's office hours are specified here, look at the notices for any variation. The place is Luca Tesei's office, 1st floor, Polo Lodovici, via Madonna delle Carceri 9, Camerino.

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 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 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
• Use in an effective way available software tools for model checking (e.g. SPIN, NuSMV)

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 SPIN tool.
• Computation Tree Logic (CTL). CTL model checking.
• The NuSMV tool.

1. Wed 04/10/2017 Watch Lecture, Download Lecture
2. Thu 05/10/2017 Watch Lecture, Download Lecture, Notes
3. Wed 11/10/2017 Watch Lecture, Download Lecture, Notes
4. Wed 18/10/2017 Watch Lecture, Download Lecture
5. Thu 19/10/2017 Watch Lecture, Download Lecture, Notes
6. Thu 26/10/2017 Watch Lecture, Download Lecture, Spin Promela examples of the slides or of the exercises
7. Thu 02/11/2017 Watch Lecture, Download Lecture
8. Wed 15/11/2017 Watch Lecture, Download Lecture, Notes
9. Thu 16/11/2017 Watch Lecture, Download Lecture, Notes
10. Wed 22/11/2017 Watch Lecture, Download Lecture, Notes
11. Thu 23/11/2017 Watch Lecture, Download Lecture, Notes
12. Wed 29/11/2017 Watch Lecture, Download Lecture, Notes
13. Thu 30/11/2017 Watch Lecture, Download Lecture, Notes
14. Wed 06/12/2017 Watch Lecture, Download Lecture
15. Thu 07/12/2017 Watch Lecture, Download Lecture, Notes
16. Wed 13/12/2017 Watch Lecture, Download Lecture, Promela examples
17. Thu 14/12/2017 Watch Lecture, Download Lecture, Notes
18. Wed 20/12/2017 Watch Lecture, Download Lecture
19. Thu 21/12/2017 Watch Lecture, Download Lecture
20. Wed 10/01/2018 Watch Lecture, Download Lecture, Notes
21. Thu 11/01/2018 Watch Lecture First Part, Download Lecture First Part, Watch Lecture Second Part, Download Lecture Second Part, Notes

Course Additional Resources (w.r.t. the textbook)

Specification of Models

• Introduction to Model Checking
• Transition Systems
• Modelling Hardware Circuits
• Program Graphs
• Guarded Commands Language
• Parallelism. Interleaving for Transition Systems
• Parallelism. Interleaving for Program Graphs
• Parallelism and Communication. Synchronous Message Passing
• Parallelism and Communication. Channel Systems
• Parallelism and Communication. Synchronous Product
• NanoPromela Syntax and Semantics

Exercises on Models and Modelling

• Exercises with (some) solutions

SPIN Model Checker

• Promela Language and SPIN Model Checker
• SpinRCP Front-end to SPIN
• SPIN Slides 1
• SPIN Slides 2
• SPIN Slides 3
• SPIN Slides 4
• SPIN Slides 5
• SPIN Slides 6

Linear Time Properties

• Introduction.
• Definition and Satisfaction. Trace Equivalence
• Invariants and Invariant Checking.
• Safety Properties. Bad Prefixes and Prefix Closure.
• Liveness Properties.
• Decomposition Theorem.
• Fairness.
• Regular Safety Properties.
• Omega-Regular Properties.
• Model Checking with Buchi Automata

Exercises on Linear Time Properties

• Exercises with (some) solutions on Linear Time Properties, Safety/Liveness, Fairness
• Exercises with (some) solutions on Regular Properties
• Exercises with (some) solutions on LTL

Linear Temporal Logic

• LTL syntax and semantics - Updated 13/12/17
• LTL equivalences and laws - Updated 13/12/17
• Expressing fairness in LTL - Updated 13/12/17
• General Picture of LTL model checking with omega automata and complexity - Updated 13/12/17

Computation Tree Logic

• CTL: Syntax, Semantics, Equivalence and Normal Forms
• CTL vs LTL
• CTL Model Checking
• CTL with Fairness

Exercises on NFA, NBA, LTL and CTL

• Exercises NFA, Bad prefixes and NBA
• Exercises LTL
• Exercises CTL

Textbook

• Christel Baier, Joost-Pieter Katoen, “Principles of Model Checking”, The MIT Press, 2008, ISBN: 9780262026499. Website of the book with additional material available here

Reference books

• Gerard Holzmann, “The Spin Model Checker: Primer and Reference Manual”, Addison Wesley, 2003. ISBN: 978-0321773715.
• 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

Project to be sent the day before the written test:

1. Text of the Project

Exam Dates A.Y. 2017/2018

1. Appello I - Written Test on Thursday 01/02/2018 at 3.00pm, Room AB3 Polo Lodovici - Written Test Text, Written Test Solution
2. Appello II - Written Test on Thursday 15/02/2018 at 3.00pm, Room AB3 Polo Lodovici - Written Test Text, Written Test Solution
3. Appello III - Written Test on Wednesday 20/06/2018 at 3.00pm, Room AB3 Polo Lodovici - No Students
4. Appello IV - Written Test on Wednesday 11/07/2018 at 10.00am, Room AB3 Polo Lodovici - Written Test Text, Written Test Solution
5. Appello V - Written Test on Wednesday 12/09/2018 at 10.00am, Room AB3 Polo Lodovici
6. Appello VI - Written Test on Wednesday 26/09/2018 at 3.00pm, Room AB3 Polo Lodovici
7. Appello VII - Written Test on Wednesday 06/02/2019 at 3.00pm, Room TBA
8. Appello VIII - Written Test on Wednesday 20/02/2019 at 3.00pm, Room TBA

Sample Written Tests

1. Sample 1
2. Sample 2, Sample 2 with Solutions
3. Sample 3

Exam rules

The exam consists of a written test, containing open-answer and/or closed-answer questions, together with one project, realised with a model checking tool (see section “Projects” above). The project must be sent the day before the written test to which the student is registered (see section “Instructions for Sending Projects” below). During the exercise sessions throughout the course samples of the written test questions will be presented with solutions. During the written test students can consult a hand-written A4 paper of their production for reference.

Registration for the written tests must be done using the Student Career System ESSE3 here. Please note that the registration deadline is usually 3 working days before the written test date. 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 Student Secretary Office at Campus, Via D'Accorso SNC, Camerino Opening Hours) their choice to attend to this course, code [ST1113] REACTIVE SYSTEMS VERIFICATION.

Please note that any student who did not send the project the day before the written test may be excluded from the written test. In case of re-trying of the written test the project must be re-sent.

Instructions for Sending Projects

Students must create a folder in Google Drive, using the Google account associated to their email name.surname@studenti.unicam.it

The folder must contain all the files relative to the project and a written report, in English, which describes all the phases of the developing of the project. The use of screenshots is encouraged to show, within the report, the runs and the results of the project.

The folder must be named

RSV1718-Project-N-APP-X-Surname-Name

where N is the number of the realised project (according to the section “Projects” above) and X is the number of the exam session (Appello) as specified for each date of the written test above.

The folder must be shared (using Google Drive facilities) with luca.tesei@unicam.it and francesco.tiezzi@unicam.it by 11.59pm of the day before the written test scheduled for the selected session X.

Exam Results

• The results will be communicated through this site or by email (depending on the number of students).
• Contextually to the communication of the results, students will be invited to accept or reject the evaluation. In case of acceptance, the grade will be registered in ESSE3.