Fundamentals of Reactive Systems

Teacher:

• Francesco Tiezzi

ESSE3 Link

• Fundamentals of Reactive Systems - AY 2018/2019

Lessons schedule:

• Wednesday 9 - 11 (TL room)
• Thursday 11 - 13 (TL room)

Students Office hours:

• on appointment (via email), second floor of Polo Lodovici, via Madonna delle Carceri 9, Camerino

D1 – KNOWLEDGE AND UNDERSTANDING
At the end of the course, the student should be able to:

1. Have the knowledge of the issues concerning concurrent/distributed programming and the modelling of hardware/software systems as software-intensive systems.
2. Have the knowledge of the semantics of the operators of the process algebras CCS, CSP and ACP.
3. Have the knowledge of the syntax and the semantics of the modal logic Hennessy-Milner Logic (HML), with and without recursion, and of the ACTL logic.
4. Have the knowledge of the main observational behavioural equivalences, weak and strong.
5. Have the knowledge of the tools for the automatic verification of software-intensive systems modelled by means of process algebras.

D2 – APPLYING KNOWLEDGE AND UNDERSTANDING
At the end of the course, the student should be able to:

1. Modelling a software-intensive system using the formal languages presented in the course, using a compositional approach.
2. Derive the labelled transition system associated to a process.
3. Decide if one or more state of a labelled transition system are stong or weak bisimilar, providing a suitable bisimulation relation whereas possible.
4. Decide if one or more states of a labelled transition system satisfy formulas of HML and ACTL logics.
5. Define temporal properties of a software-intensive system using the HML and ACTL logics.
6. Use a specific software tool for the analysis of software-intensive systems modelled using the CCS language or other formalism.

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.
2. Write a brief survey and state of the art about a given research topic by searching the scientific literature.

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 software-intensive systems.
2. Autonomously understand and learn to use new features added to tools for modelling and verifying software-intensive systems.

• Introductory concepts: concurrent, reactive and software-intensive systems
• Preliminary mathematical concepts
• Semantics of the operators of the process algebras CCS, CSP and ACP
• The Maude toolset
• Main behavioural equivalences, weak and strong
• Hennessy-Milner Logic and ACTL
• Software tools for the automatic verification of software-intensive systems modelled by means of process algebras: TAPAs

Course Slides

• Introduction and general information
• Preliminaries
• Formal semantics of regular expressions
• CCS

Lectures

• 09/10/2019: general info; reactive systems; process algebraic approach; formal methods for reactive systems (recorded lecture)
• 10/10/2019: sets; relations; equivalences; functions; induction principle. (recorded lecture)
• 16/10/2019: inductively defined sets; inference systems; grammars (recorded lecture)
• 24/10/2019: LTS; syntax of regular expressions (recorded lecture)
• 30/10/2019: operational semantics of regular expressions (recorded lecture)
• 31/10/2019: examples about operational semantics of regular expressions (recorded lecture)
• 06/11/2019: denotational semantics of regular expressions (recorded lecture)
• 07/11/2019: exercise on denotational semantics; axiomatic semantics (recorded lecture1,recorded lecture2)
• 14/11/2019: first in itinere test
• 20/11/2019: Introduction to Maude: sorts, operations (recorded lecture)
• 21/11/2019: Introduction to Maude: equations (recorded lecture)
• 27/11/2019: Introduction to Maude: rewrite laws (recorded lecture) example
• 28/11/2019: Maude examples (recorded lecture) example
• 04/12/2019: Operational semantics of regular expression in Maude (recorded lecture) example
• 05/12/2019: CCS synatx and semantics (recorded lecture)
• 11/12/2019: Psecuo and TAPAs (recorded lecture)
• 12/12/2019: Process Algebras operators
• 19/12/2019: Behavioural equivalences: bisimilarity and trace equivalence (recorded lecture)
• 15/01/2020: Second in itinere test
• 16/01/2020: Projects' presentations

Reference books
The main material of the course consists of:

• Rocco De Nicola. A gentle introduction to Process Algebras. Notes obtained by the restructuring of two entries (Process Algebras - Behavioural Equivalences) of Encyclopedia of Parallel Computing, David A. Padua (Ed.). Springer 2011; pp. 120-127 and pp. 1624-1636.
• Luca Aceto, Anna Ingolfsdottir, Kim Guldstrand Larsen and Jiri Srba, “Reactive Systems. Modelling, Specification and Verification”, Cambridge University Press, 2007. ISBN: 9780521875462. Website of the book with additional material available: http://rsbook.cs.aau.dk

Morover, lecture notes, papers and slides may be provided in this website.

The Maude tool can be downloaded for free for academic use, together with documentation and tutorials, from the website: http://maude.cs.illinois.edu/

The TAPAs tool can be downloaded for free for academic use, together with documentation and tutorials, from the website: http://rap.dsi.unifi.it/tapas/

Exam Dates A.Y. 2018/2019 (TO BE UPDATED)

• 28/01/2019, 14:00 - Polo Lodovici
• 11/02/2019, 14:00 - Polo Lodovici
• 25/02/2019, 14:00 - Polo Lodovici
• 20/05/2019, 14:00 - Polo Lodovici
• 03/06/2019, 14:00 - Polo Lodovici
• 01/07/2019, 14:00 - Polo Lodovici
• 13/09/2019, 14:00 - Polo Lodovici
• 27/09/2019, 14:00 - Polo Lodovici

Exam rules:

• Written test. On the exam date a written test takes place, it has a mixed structure: solution of exercises, and open/close answer questionnaire. During the course in itinere tests take place; in case they are evaluated positively, they replace the written test of the exam date.
• Realisation of a project with a software tool presented during the course, or writing of a report. There is an oral discussion.

Exam Results

• …