====== 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**:
* [[http://docenti.unicam.it/pdett.aspx?ids=N&tv=d&UteId=990&ru=PA|Francesco Tiezzi]]
**ESSE3 Link**
* [[https://didattica.unicam.it/Guide/PaginaADErogata.do?cod_lingua=eng&ad_er_id=2018*N0*N0*S1*15043*9983&ANNO_ACCADEMICO=2018&mostra_percorsi=S|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
----
===== 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**
* {{ :didattica:magistrale:frs:ay_1920:frs_intro1920.pdf |Introduction and general information}}
* {{ :didattica:magistrale:frs:ay_1920:preliminaries1920.pdf |Preliminaries}}
* {{ :didattica:magistrale:frs:ay_1920:formal_semantics_of_regular_expressions_1920.pdf |Formal semantics of regular expressions}}
* {{ :didattica:magistrale:frs:ay_1920:ccs_1920.pdf |CCS}}
**Lectures**
* 09/10/2019: general info; reactive systems; process algebraic approach; formal methods for reactive systems ([[https://unicam.webex.com/unicam/ldr.php?RCID=a00da58b13380f7c0155060a4f9ad3a1|recorded lecture]])
* 10/10/2019: sets; relations; equivalences; functions; induction principle. ([[https://unicam.webex.com/unicam/ldr.php?RCID=c79c647b9e9af8511bd94fa97d8a1155|recorded lecture]])
* 16/10/2019: inductively defined sets; inference systems; grammars ([[https://unicam.webex.com/unicam/ldr.php?RCID=4fb2d0877f2b4e909fb93ed9dc464a7e|recorded lecture]])
* 24/10/2019: LTS; syntax of regular expressions ([[https://unicam.webex.com/unicam/ldr.php?RCID=daeadda833d640e18419753d29d782e7|recorded lecture]])
* 30/10/2019: operational semantics of regular expressions ([[https://unicam.webex.com/unicam/ldr.php?RCID=52f445504ffa404aa928f95fc2a62d4d|recorded lecture]])
* 31/10/2019: examples about operational semantics of regular expressions ([[https://unicam.webex.com/unicam/ldr.php?RCID=74b7d1c601e84ae3bc9f8c3e77072628 |recorded lecture]])
* 06/11/2019: denotational semantics of regular expressions ([[https://unicam.webex.com/unicam/ldr.php?RCID=c634023d533a4471a49be28ae766566d|recorded lecture]])
* 07/11/2019: exercise on denotational semantics; axiomatic semantics ([[https://unicam.webex.com/unicam/ldr.php?RCID=bf0e3fb1b2a34a9bbd0f52019d00a462|recorded lecture1]],[[https://unicam.webex.com/unicam/ldr.php?RCID=b4220a16c89f4d9db353ada6b67d8e0f|recorded lecture2]])
* 14/11/2019: first in itinere test
* 20/11/2019: Introduction to Maude: sorts, operations ([[https://unicam.webex.com/recordingservice/sites/unicam/recording/playback/c2f238ca993f40148a123a86e8b4acb7|recorded lecture]])
* 21/11/2019: Introduction to Maude: equations ([[https://unicam.webex.com/recordingservice/sites/unicam/recording/playback/1f6bc281365e44c79874af5dddcd8e06|recorded lecture]])
* 27/11/2019: Introduction to Maude: rewrite laws ([[https://unicam.webex.com/recordingservice/sites/unicam/recording/playback/344a698a6e114077b6145d15c49e2a81|recorded lecture]]) {{ :didattica:magistrale:frs:ay_1920:mycigaretteexample.maude.zip |example}}
* 28/11/2019: Maude examples ([[https://unicam.webex.com/recordingservice/sites/unicam/recording/playback/b6e2e08452b94556a305064b2bcd928c|recorded lecture]]) {{ :didattica:magistrale:frs:ay_1920:river.maude.zip |example}}
* 04/12/2019: Operational semantics of regular expression in Maude ([[https://unicam.webex.com/recordingservice/sites/unicam/recording/playback/b73bb4f6722c42be9d18dc7413dde280|recorded lecture]]) {{ :didattica:magistrale:frs:ay_1920:op_sem_regular_expressions.maude.zip |example}}
* 05/12/2019: CCS synatx and semantics ([[https://unicam.webex.com/recordingservice/sites/unicam/recording/playback/5b52d5c8aacc4170a5c46df0b469f0a8|recorded lecture]])
* 11/12/2019: Psecuo and TAPAs ([[https://unicam.webex.com/recordingservice/sites/unicam/recording/playback/58c17660c8304ab4bf701bec079d59ec|recorded lecture]])
* 12/12/2019: Process Algebras operators
* 19/12/2019: Behavioural equivalences: bisimilarity and trace equivalence ([[https://unicam.webex.com/recordingservice/sites/unicam/recording/playback/5f87ee3eed8e4978aba2aa6a27ae8ee1|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. {{ :didattica:magistrale:frs:ay_1920:intro-to-pa.pdf |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 **
* ...