====== Fundamentals of Reactive Systems ======
----
===== News =====
<WRAP center round important 95%>
  * 19/1/2021: Projects' presentations.
  * <wrap em>12/1/2021: Second in itinere test: {{ :didattica:magistrale:frs:ay_2021:frs_written_test_12_jan_2021.pdf |partial test}} and {{ :didattica:magistrale:frs:ay_2021:frs_written_test_12_jan_2021_full.pdf |full test}}.</wrap>
  * 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
</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=ita&ad_er_id=2020*N0*N0*S1*16793*9983&ANNO_ACCADEMICO=2020&mostra_percorsi=S|Fundamentals of Reactive Systems - AY 2020/2021]]

**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
</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
</WRAP>
----
===== Study material =====
<WRAP box round center 95%>
**Course Slides**
  * {{ :didattica:magistrale:frs:ay_2021:frs_intro2021.pdf |Introduction and general information}}
  * {{ :didattica:magistrale:frs:ay_2021:1_frs2021_preliminaries.pdf |Preliminaries}}
  * {{ :didattica:magistrale:frs:ay_2021:2_frs2021_-_formal_semantics_of_regular_expressions.pdf |Semantics of Regular Expressions}}
  * {{ :didattica:magistrale:frs:ay_2021:3_frs2021_-_ccs.pdf |CCS}}




**Lectures**

Copyright ({{ :didattica:magistrale:frs:ay_2021:dichiarazione_di_copyright.pdf |PDF}})
  * 29/09/2020: general info; reactive systems; process algebraic approach; formal methods for reactive systems ([[https://unicam.webex.com/recordingservice/sites/unicam/recording/playback/eaa5af287d474ea28ab922a3a1bcedf8|recorded lecture]])
  * 30/09/2020: intro to LTS; sets; relations ([[https://unicam.webex.com/recordingservice/sites/unicam/recording/playback/dd5aafac5bbd4db1a5d733a0e15189c9|recorded lecture]])
  * 06/10/2020: relations; equivalences; functions; induction principle; inductively defined sets; inference systems ([[https://unicam.webex.com/recordingservice/sites/unicam/recording/playback/8731fcce7b0b40149e6d18cc5ae2ee34|recorded lecture]])
  * 07/10/2020: grammars; LTS ([[https://unicam.webex.com/recordingservice/sites/unicam/recording/playback/e2af2c5d8c1d43209a771ca040a6383a|recorded lecture]])
  * 13/10/2020: syntax of regular expressions; operational semantics of regular expressions ([[https://unicam.webex.com/recordingservice/sites/unicam/recording/playback/e2e2e57d7351405294b4fc9b944d69fe|recorded lecture]])
  * 14/10/2020: examples about operational semantics of regular expressions ([[https://unicam.webex.com/recordingservice/sites/unicam/recording/playback/da2ad511c7704aa8821414f2d82326b4|recorded lecture]])
  * 20/10/2020: denotational semantics of regular expressions ([[https://unicam.webex.com/recordingservice/sites/unicam/recording/playback/1d30a49203964682b08a243aa3a57eea|recorded lecture]])
  * 21/10/2020: exercise on denotational semantics; axiomatic semantics ([[https://unicam.webex.com/recordingservice/sites/unicam/recording/playback/ef8acdc1eed442c88687f3a7dd3f50b1|recorded lecture]])
  * 27/10/2020: CCS synatx and semantics ([[https://unicam.webex.com/recordingservice/sites/unicam/recording/playback/ecfdf30fab7c4e25a65805cc0680f805|recorded lecture]])
  * 03/11/2020: CCS examples ([[https://unicam.webex.com/recordingservice/sites/unicam/recording/playback/2972b5c39e7c450daab2ba83572b789d|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 ([[https://unicam.webex.com/recordingservice/sites/unicam/recording/playback/3baa19c2766f450daff73d7903533b6f|recorded lecture]])
  * 18/11/2020: Introduction to Maude: sorts, operations; equations ([[https://unicam.webex.com/recordingservice/sites/unicam/recording/playback/ad04ef26f4ab4f3ab7738a43aaa9be60|recorded lecture]])
  * 24/11/2020: Introduction to Maude: rewrite laws ([[https://unicam.webex.com/unicam/ldr.php?RCID=54dc01ed7a9749f1a7dd99940569619f|recorded lecture]])
  * 25/11/2020: Maude examples ([[https://unicam.webex.com/unicam/ldr.php?RCID=65d555f2429541269196a378b97e329c|recorded lecture]])  
  * 01/12/2020: Operational semantics of regular expression in Maude ([[https://unicam.webex.com/unicam/ldr.php?RCID=6dd1f240544b4687ad87cd3a7073acb2|recorded lecture]])
  * 02/12/2020: Exercises on CCS ([[https://unicam.webex.com/unicam/ldr.php?RCID=c976a588a71340fc93b0dc25c55256c3|recorded lecture]])
  * 09/12/2020: Process Algebras operators ([[https://unicam.webex.com/unicam/ldr.php?RCID=eac56526bbac4c27be643feafcbbae4d|recorded lecture]])
  * 15/12/2020: Behavioural equivalences (trace equivalence and bisimilarity) ([[https://unicam.webex.com/unicam/ldr.php?RCID=58012ef62631487288b562ff51bf197b|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. {{ :didattica:magistrale:frs:ay_2021: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/


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

</WRAP>