# Fundamentals of Reactive Systems

## News

- 19/1/2021: Projects' presentations.
- 12/1/2021: Second in itinere test: partial test and full test.
- 08/11/2020: The lectures of 10/11 and 11/11 are postponed. Next lecture will take place on 17/11.
- 04/11/2020: First partial exam.
- 29/09/2020: First lecture of the course.
- Telegram channel: FRS2021@unicam

## General Info

**Teacher**:

**ESSE3 Link**

**Lessons schedule**:

- Tuesday 11 - 13 (LB1 room)
- Wednesday 9 - 11 (LB1 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

## Study material

**Course Slides**

**Lectures**

Copyright (PDF)

- 29/09/2020: general info; reactive systems; process algebraic approach; formal methods for reactive systems (recorded lecture)
- 30/09/2020: intro to LTS; sets; relations (recorded lecture)
- 06/10/2020: relations; equivalences; functions; induction principle; inductively defined sets; inference systems (recorded lecture)
- 07/10/2020: grammars; LTS (recorded lecture)
- 13/10/2020: syntax of regular expressions; operational semantics of regular expressions (recorded lecture)
- 14/10/2020: examples about operational semantics of regular expressions (recorded lecture)
- 20/10/2020: denotational semantics of regular expressions (recorded lecture)
- 21/10/2020: exercise on denotational semantics; axiomatic semantics (recorded lecture)
- 27/10/2020: CCS synatx and semantics (recorded lecture)
- 03/11/2020: CCS examples (recorded lecture)
- 04/11/2020: first in itinere test
- 17/11/2020: discussion of the solution of the first in itinere test; CCS examples; Pesuco tool (recorded lecture)
- 18/11/2020: Introduction to Maude: sorts, operations; equations (recorded lecture)
- 24/11/2020: Introduction to Maude: rewrite laws (recorded lecture)
- 25/11/2020: Maude examples (recorded lecture)
- 01/12/2020: Operational semantics of regular expression in Maude (recorded lecture)
- 02/12/2020: Exercises on CCS (recorded lecture)
- 09/12/2020: Process Algebras operators (recorded lecture)
- 15/12/2020: Behavioural equivalences (trace equivalence and bisimilarity) (recorded lecture)
- 12/1/2021: Second in itinere test.
- 19/1/2021: 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/

## Exams

**Exam Dates A.Y. 2020/2021**

- I: 09/02/2021, 15:00 - Polo Lodovici
- II: 23/02/2021, 15:00 - Polo Lodovici
- III: 14/06/2021, 15:00 - Polo Lodovici
- IV: 28/06/2021, 15:00 - Polo Lodovici
- V: 12/07/2021, 15:00 - Polo Lodovici
- VI: 13/09/2021, 15:00 - Polo Lodovici
- VII: 27/09/2021, 15:00 - Polo Lodovici
- VIII: 07/02/2022, 15: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**.