# Fundamentals of Reactive Systems

## News

- 23/10/2019: Lecture postponed, next lecture Thursday 24 October.
- 09/10/2019: First lecture of the course.
- Telegram channel: FRS1920@unicam

## General Info

**Teacher**:

**ESSE3 Link**

**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

## Course Objectives

D1 – KNOWLEDGE AND UNDERSTANDING

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

- Have the knowledge of the issues concerning concurrent/distributed programming and the modelling of hardware/software systems as software-intensive systems.
- Have the knowledge of the semantics of the operators of the process algebras CCS, CSP and ACP.
- 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.
- Have the knowledge of the main observational behavioural equivalences, weak and strong.
- 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:

- Modelling a software-intensive system using the formal languages presented in the course, using a compositional approach.
- Derive the labelled transition system associated to a process.
- Decide if one or more state of a labelled transition system are stong or weak bisimilar, providing a suitable bisimulation relation whereas possible.
- Decide if one or more states of a labelled transition system satisfy formulas of HML and ACTL logics.
- Define temporal properties of a software-intensive system using the HML and ACTL logics.
- 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:

- 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:

- Write a clear report on the modelling and analysis of a system under study using a formal style.
- 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:

- Search the scientific literature for specific advances in formalisms and tools aimed at modelling and verifying software-intensive systems.
- Autonomously understand and learn to use new features added to tools for modelling and verifying software-intensive systems.

## Course Contents

- 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

## Study material

**Course Slides**

**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/

## Exams

**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 **

- …