Reactive Systems Verification


  • Wed 4th October 2017: the course officially starts at 2.00 pm in Room AB3 of Polo Lodovici, via Madonna delle Carceri 9, Camerino
  • Thu 12th October 2017: the lecture of Thursday 12th October is cancelled for a committment of the teacher.
  • Thu 25th October 2017: the lecture of Wednesday 25th October is cancelled for a personal problem of the teacher.
  • Mon 30th October 2017: on Thursday 2nd November the lecture will be given regularly.
  • Mon 30th October 2017: the lectures of Wednesday 8th November and of Thursday 9th November are cancelled for a commitment of the teacher.

Teacher:

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

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.

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

Specification of Models

Exercises on Models and Modelling

SPIN Model Checker

Linear Time Properties

Exercises on Linear Time Properties

Linear Temporal Logic

Computational Tree Logic

Exercises on NFA, NBA, LTL and 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(s) to be sent the day before the written test:

  1. TBA

Exam Dates A.Y. 2017/2018

  1. Appello I - Written Test on Thursday 01/02/2018 at 3.00pm, Room TBA
  2. Appello II - Written Test on Thursday 15/02/2018 at 3.00pm, Room TBA
  3. Appello III - Written Test on Wednesday 20/06/2018 at 3.00pm, Room TBA
  4. Appello IV - Written Test on Wednesday 11/07/2018 at 3.00pm, Room TBA
  5. Appello V - Written Test on Wednesday 12/09/2018 at 3.00pm, Room TBA
  6. Appello VI - Written Test on Wednesday 26/09/2018 at 3.00pm, Room TBA
  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

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 will 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 will 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.