====== Fundamentals of Reactive Systems ======
----
===== News =====
<WRAP center round important 95%>
  * <wrap em>21/1/2019: from 9:00 to 13:00 there will be ALL project presentations.</wrap>
  * <wrap em>14/1/2019: second in itinere test</wrap>
  * 9/1/2019: Wednesday 09 January there will be the last theoretical lecture.
  * 17/12/2018: due to bad weather, ALL lectures on Monday 17 December are cancelled.
  * 5/12/2018: wed 5/12 the lecture is replaced by the seminar by Prof. Nobuko Yoshida, starting at 10:00.
  * 28/11/2018: wed 28/11 the lecture is cancelled.
  * 26/11/2018: mon 26/11 the lecture is cancelled due to the academic year inauguration.
  * 14/11/2018: First in itinere test.
  * 31/10/2018: The lectures of 31/10 is postponed.
  * 08-10/10/2018: The lectures of 8/10 and 10/10 are postponed; the next lecture is 15/10.
  * 03/10/2018: First lecture of the course.
  * <wrap em>Telegram channel: FRS1819@unicam</wrap>
</WRAP>

----
===== General Info =====
<WRAP box round 95% center>
**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**:
  * Monday 9 - 11 (AB3 room)
  * Wednesday 9 - 11 (AB2 room)

**Students Office hours**:
  * on appointment (via email), second floor of Polo Lodovici, via Madonna delle Carceri 9, Camerino
</WRAP>
----
===== Course Objectives =====

<WRAP box round 95% center>
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.
</WRAP>

----
===== Course Contents =====

<WRAP round 95% center box>
  * 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 and muCRL2
</WRAP>
----
===== Study material =====
<WRAP box round center 95%>
**Course Slides**
  * {{ :didattica:magistrale:frs:ay_1819:frs_intro1819.pdf |Introduction and general information}}
  * {{ :didattica:magistrale:frs:ay_1819:preliminaries_1819.pdf |Preliminaries}}
  * {{ :didattica:magistrale:frs:ay_1819:formal_semantics_of_regular_expressions_1819.pdf |Formal semantics of regular expressions}}
  * {{ :didattica:magistrale:frs:ay_1819:ccs_1819.pdf |CCS}}


**Lectures**
  * 3/10/2018: general info; reactive systems; process algebraic approach; formal methods for reactive systems ([[https://unicam.webex.com/unicam/ldr.php?RCID=a67bc5754fa377d212adc8b4cc93cdd8 |registration]])
  * 15/10/2018: LTS; sets; relations ([[https://unicam.webex.com/unicam/ldr.php?RCID=a16993cd3fb0bf8242b67388f27ae3c1|registration]])
  * 17/10/2018: equivalences; functions; induction principle; inductively defined sets; inference systems ([[https://unicam.webex.com/unicam/ldr.php?RCID=39017e7da7e0f9a10f69666d53c0637c |registration]])
  * 22/10/2018: grammars; LTS; syntax of regular expressions ([[https://unicam.webex.com/unicam/ldr.php?RCID=aa8061e8e22baf1572eea159f2a51264|registration]])
  * 24/10/2018: operational semantics of regular expressions ([[https://unicam.webex.com/unicam/ldr.php?RCID=9986df15ca2cf41ae856f1415ec96543|registration]])
  * 29/10/2018: examples about operational semantics of regular expressions; denotational semantics of regular expressions; axiomatic semantics of regular expressions ([[https://unicam.webex.com/recordingservice/sites/unicam/recording/playback/cbad041c59e84af6ac2404481efa7598|registration]])
  * 5/11/2018: introduction to Maude: sort, operations, equations ([[https://unicam.webex.com/unicam/ldr.php?RCID=95ce0f9cb2070490dadaa822dad27dbe|registration]]) 
  * 7/11/2018: Introduction to Maude: rewrite laws; {{ :didattica:magistrale:frs:ay_1819:river.maude.zip |Maude examples}} ([[https://unicam.webex.com/unicam/ldr.php?RCID=85b8b0c42848c4aa5300bd3a0a3a0a76 |registration]])
  * 12/11/2018: Operational semantics of regular expression in Maude ({{ :didattica:magistrale:frs:ay_1819:op_sem_regular_expressions.maude.zip|Maude code}}) ([[https://unicam.webex.com/unicam/ldr.php?RCID=8cdc37a0026f5c9530d14e1962999e40|registration]])
  * 14/11/2018: First in itinere test.
  * 19/11/2018: Discussion of the in itinere test results; discussion of projects.
  * 21/11/2018: CCS synatx and semantics ([[https://unicam.webex.com/unicam/ldr.php?RCID=e920e98dd4b3024ffbf767cb9f8e98a7|registration]])
  * 3/12/2018: CCS examples ([[https://unicam.webex.com/unicam/ldr.php?RCID=59fc08b441f3fcf8dd5409ea8f72a93c|registration]])
  * 5/12/2018: Seminar on Polymorphic Sessions and Functions.
  * 10/12/2018: Process Algebras operators (basic processes, sequential composition, choice, parallel composition, merge) ([[https://unicam.webex.com/unicam/ldr.php?RCID=d4234a6b5f61311d3fde918a4fc0f4ac |registration]]) 
  * 12/12/2018: Process Algebras operators (hiding, recursive definitions, replication) ([[https://unicam.webex.com/unicam/ldr.php?RCID=5fea6b180ef7993580759b6e3693e051|registration]])
  * 19/12/2018: Behavioural equivalences (strong bisimilarity, weak trace equivalence, weak bisimilarity) ([[https://unicam.webex.com/unicam/ldr.php?RCID=4723b27347859cb2d68b82e0f38a8a7e|registration]])
  * 9/1/2019: Exercises on CCS and behavioural equivalences ([[https://unicam.webex.com/unicam/ldr.php?RCID=642834a22dec26bb9bfaa988e5fad169 |registration]])
  * 14/1/2019: Second in itinere test
  * 21/1/2019: Project presentations (from 9:00 to 12:00).
  
   
**Reference books**\\
The main material of the course consists of: 
  * Rocco De Nicola. {{ :didattica:magistrale:frs:ay_1819: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/

The mCRL2 tool can be downloaded for free for academic use, together with documentation and tutorials, from the website: http://www.mcrl2.org/release/user_manual/index.html

</WRAP>
----
===== Exams =====
<WRAP box round center 95%>
**Exam Dates A.Y. 2018/2019**
  * 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 **
  * ...
</WRAP>