Real-time and Probabilistic Systems Verification

Teacher:

• Luca Tesei

Lectures schedule:

• Mon 11.00 am - 1.00 pm @ Room LA1, ground floor, Polo Lodovici, via Madonna delle Carceri 9, Camerino.
• Thu 2.00 pm - 4.00 pm @ Room AB3, 1st floor, Polo Lodovici, via Madonna delle Carceri 9, Camerino.

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

Prerequisites

• Having passed the course “Reactive Systems Verification” alias “Model Checking I”

D1 – KNOWLEDGE AND UNDERSTANDING

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

1. Understand the concept of bisimilarity and the algorithms for calculating a bisimulation
2. Understand the concept of action-based branching time logic
3. Understand the issues related to time critical systems and the need of expanding non-deterministic formalisms with time
4. Understand the concepts of clock variables, timed automata, timed paths, divergence and zenoness
5. Illustrate the syntax and the semantics of Timed Computation Tree Logic (TCTL)
6. Understand the concept of clock regions and zones and illustrate how they can be used to realize the model checking of TCTL
7. Understand the concept of probabilistic and stochastic systems and their verification
8. Illustrate the definition of Discrete Time Markov Chains (DTMC), Markov Decision Processes (MDP) and Continuous Time Markov Chains (CTMC)
9. Illustrate the syntax and the semantics of Probabilistic Computation Tree Logic (PCTL) and Continuous Stochastic Logic (CSL)

D2 – APPLYING KNOWLEDGE AND UNDERSTANDING

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

1. Determine if two states of a transition system are bisimilar
2. Use the Hennessy-Milner Logic with recursion for specifying untimed properties
3. Use the formalism of Timed Automata to model real-time systems
4. Use the tool UPPAAL to verify real-time systems
5. Use the formalisms of DTMC, MDP and CTMC to model probabilistic or stochastic systems
6. Use the tool PRISM to verify probabilistic or stochastic systems

D3 – MAKING JUDGEMENTS

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

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

D4 - COMMUNICATION SKILLS

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

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

D5 – LEARNING SKILLS

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

1. Search the scientific literature for specific advances in formalisms and tools aimed at modelling and verifying timed, stochastic and probabilistic systems
2. Autonomously understand and learn to use new features added to tools for modelling and verifying timed, stochastic and probabilistic systems

• Bisimilarity and bisimulation, calculating the quotient set through partition refinement.
• Theory of fixed points.
• Hennessy-Milner Logic with Recursion.
• Real-time systems and timed formalisms.
• Timed Automata. Timed Computation Tree Logic (TCTL).
• Clock Regions and Zones.
• The UPPAAL Tool.
• Probabilistic and Stochastic Systems.
• Discrete Time Markov Chains (DTMC), Markov Decision Processes (MDP) and Continuous Time Markov Chains (CTMC).
• Probabilistic Computation Tree Logic (PCTL) and Continuous Stochastic Logic (CSL).
• The tool PRISM.

Additional Material besides the Reference Books

• Strong Bisimilarity, Exercises on Strong Bisimilarity - Reactive Systems Book pages: 31-53
• Weak Bisimilarity, Exercises on Weak Bisimilarity, Hennessy-Milner Logic (HML) - Reactive Systems Book pages: 53 - 72 and 89 - 101
• Tarski's Fixpoint Theorem, Bisimulation as a fixed point, Exercises and solution on Strong and Weak Bisimulation, HML and fixpoints Reactive Systems Book pages: 75 - 88
• HML with recursively defined variables - Reactive Systems Book pages: 105 - 120 - Exercises on HML, fixpoints and HML with recursion are in the Exercise book posted for the last lecture
• State-based bisimilarity and Bisimulation quotient - Principles of MC Book pages: 449 - 468, Algorithms for computing the bisimulation quotient - Principles of MC Book pages: 476 - 493, CTL, CTL* and Bisimulation Equivalence - Principles of MC Book pages: 468 - 476
• Timed Systems versus Untimed Systems: quantitative versus qualitative notion of time in models of software and hardware systems. Timed Labelled Transition Systems. Timed CCS: Syntax and Semantics. The principle of maximal process in Timed CCS (expressibility of time-outs). Examples. - Reactive Systems Book pages: 159 - 174.
• Definition of timed traces and timed languages (Reactive Systems Book pages: 193 - 195). Exercises on derivations of TCSS delay and action transitions. Exercises on existence of timed traces of TCCS processes. Exercises on TCCS Modelling and Derivations
• Timed Automata: Syntax and Semantics Slides
• Syntax and semantics of Networks of Timed Automata (see previous Slides), The UPPAAL Tool, Tutorial on UPPAAL
• UPPAAL Exercises: JobShop, Fischer's Mutual Exclusion protocol, UPPAAL Code , Slides on Fisher's Protocol, Discussion on starvation of Fischer's Protocol - Exercises on Timed Automata, Timed Bisimulation, Region Graphs
• Exercises on Timed Automata using UPPAAL: Fischer's mutual exclusion protocol, Gossipin Girls untimed and timed. Use of UPPAAL for determining the minimum number of calls to share all the secrets and the minimum amount of time to share all the secrets. Experiments on exponential state explosion. Exercises on UPPAAL
• Timed equivalences. Slides 1, Slides 2.
• Regions and region graph, Slides 1, Slides 2.
• Zones, forward reachability analysis with zones, time divergence, time locks, zeno paths. Minutes, Slides Zones Slides Time Divergence, Timelocks, Zenoness. Link to the online recording of the lecture
• TCTL, Model Checking for TCTL Slides TCTL Model Checking
• Introduction to probabilistic systems and their verification. Definition of Discrete Time Markov Chain. Introduction to the tool PRISM. Examples of DTMC in PRISM. Notes
• Definition of Cylinder Sets and of the probability measure on the set of paths of a DTMC. Formal syntax and semantics of PCTL. Introduction to Markov Decision Processes. Notes
• Exponential Distributions. Continuous Time Markov Chains. Examples in PRISM. Slides, PRISM Tutorial and example
• Continuous Stochastic Logic. Reachability Probabilities in MDPs. Slides CSL, Slides MDPs, Example of MDP in PRISM
• Exercises on Modelling and Verification of MDPs and CTMCs in PRISM. Randomised Dining Philosophers, Module relabelling for 3 and 5 philosophers, Historical Paper on Randomised Dining Philosophers, and Circadian Clock
• Probabilistic Timed Automata in PRISM. Simplified IPv4 ZeroConf Protocol, Simplified protocol as PTA. Biochemical Reactions as CTMC.

Reference Books

• Luca Aceto, Anna Ingolfsdottir, Kim Guldstrand Larsen and Jiri Srba, “Reactive Systems. Modelling, Specification and Verification”, Cambridge University Press, 2007. ISBN: 9780521875462 – Website
• Christel Baier, Joost-Pieter Katoen, “Principles of Model Checking”, The MIT Press, ISBN: 9780262026499

Reading Books

• Vidyadhar G. Kulkarni, “Modeling and Analysis of Stochastic Systems, Third Edition”, Chapman & Hall/CRC, 2016, ISBN-13: 978-1498756617
• Michael Huth, Mark Ryan, “Logic in Computer Science: Modelling and Reasoning about Systems”, Cambridge University Press. ISBN: 9780521543101.
• Glynn Winskel, “Formal Semantics of Programming Languages”, The MIT Press, ISBN: 9780262731034.

Project(s) to be sent the day before the written test:

1. Project 2017-18

Exam Dates A.Y. 2017/2018

1. Appello I - Written Test on Tuesday 30/01/2018 at 3.00pm, Room TBA
2. Appello II - Written Test on Tuesday 13/02/2018 at 3.00pm, Room TBA
3. Appello III - Written Test on Tuesday 19/06/2018 at 3.00pm, Room TBA
4. Appello IV - Written Test on Tuesday 10/07/2018 at 3.00pm, Room TBA
5. Appello V - Written Test on Tuesday 11/09/2018 at 3.00pm, Room TBA
6. Appello VI - Written Test on Tuesday 25/09/2018 at 3.00pm, Room TBA
7. Appello VII - Written Test on Tuesday 05/02/2019 at 3.00pm, Room TBA
8. Appello VIII - Written Test on Wednesday 20/02/2019 at 11.00am, Room TBA

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.

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

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