====== Formal Modeling of Software Intensive Systems ======
----
===== News =====
<WRAP center round important 95%>
  * <wrap em>The result of the second in itinere test are published (see end of this page).</wrap>
  * The second in itinere test will take place on 30 June 2018 at 9:15 in Room AB2 (Polo Lodovici).
  * Calendar of the next lectures:
    * 15/05 (11:00-13:00): Exercises
    * 22/05 (11:00-12:00): Projects' discussion
    * 29/05 (11:00-13:00): Second in itinere test
    * 06/06 (9:00-12:00): Projects' presentations  
  * The lecture of May 3 is moved to the time slot 11:00-13:00 (Classroom AB2).
  * Calendar next lectures: April 18 9:00-11:00, April 26 16:00-18:00, May 2 9:00-11:00. 
  * The lecture of April 10 is postponed to April 12, 16:00-18:00, Classroom AB2.
  * The in itinere test will take place on 11 April 2018 at 9:15 in Room AB2 (Polo Lodovici).</wrap> 
  * Classroom code: 07ds9gi
  * March 6th: first lecture
</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]] 

**Lessons schedule**:
  * Tuesday 11 - 13 (LA1 room)
  * Wednesday 9 - 11 (LA1 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:fmsis:ay_1718:fmsis_intro_1718.pdf |Introduction and general information}}
  * {{ :didattica:magistrale:fmsis:ay_1718:preliminaries_1718.pdf |Preliminaries}}
  * {{ :didattica:magistrale:fmsis:ay_1718:formal_semantics_of_regular_expressions_1718.pdf |Formal semantics of regular expressions}}
  * {{ :didattica:magistrale:fmsis:ay_1718:ccs_1718.pdf |CCS}}
  * {{ :didattica:magistrale:fmsis:ay_1718:intro-to-pa.pdf |A gentle introduction to Process Algebras}}


**Lectures**
  * 6 March: general info; sw intensive systems; process algebraic approach; formal methods for reactive systems ([[https://unicam.webex.com/unicam/ldr.php?RCID=fa963af541a24fa92c5faa596061e15a|registration]])
  * 7 March: LTS; sets; relations ([[https://unicam.webex.com/unicam/ldr.php?RCID=9e8d9e5791eb2779a92838a123ed466c|registration]])
  * 13 March: equivalences; functions; induction principle; inductively defined sets ([[https://unicam.webex.com/unicam/ldr.php?RCID=bb496e57fcad8945958fd3dad8d05d90|registration]])
  * 14 March: inference systems; grammars; LTS ([[https://unicam.webex.com/unicam/ldr.php?RCID=99238dfa6d653dc189a6846248847025|registration]])
  * 20 March: syntax and operational semantics of regular expressions ([[https://unicam.webex.com/unicam/ldr.php?RCID=19ff20d6967d0126612d95e4bec1e00d|registration]])
  * 21 March: examples about operational semantics of regular expressions ([[https://unicam.webex.com/unicam/ldr.php?RCID=71c665f6f99425752f3c4212dad18ee8|registration]])
  * 27 March: denotational semantics of regular expressions; axiomatic semantics of regular expressions ([[https://unicam.webex.com/unicam/ldr.php?RCID=e4b8e70db043e0d831028718b07f0c0b|registration]])
  * 28 March: CCS ([[https://unicam.webex.com/unicam/ldr.php?RCID=3c7f57ae0a1810612cfc05a4bdc452e9|registration]])
  * 4 April: CCS examples ([[https://unicam.webex.com/unicam/ldr.php?RCID=c5c56fb690bd88d346454360c4899321|registration]])
  * 11 April: First in itinere test.
  * 12 April: CCS examples; TAPAs ([[https://unicam.webex.com/unicam/ldr.php?RCID=4f298b65e18a98b282ccee00cef475dc|registration]])
  * 18 April: Process Algebras operators (basic processes, sequential composition, choice) ([[https://unicam.webex.com/unicam/ldr.php?RCID=286067affee49375169fd5f94f8513b4|registration]])
  * 26 April: Process Algebras operators (parallel composition, merge, hiding, recursive definitions, replication) ([[https://unicam.webex.com/unicam/ldr.php?RCID=68b2d6cacb4f20e79a781ac8a2c189c9|registration]])
  * 02 May: Presentation of the course's project. Behavioural equivalences (strong trace equivalence) ([[https://unicam.webex.com/unicam/ldr.php?RCID=ec192d9b2ea4026952cc4d8fd463afc4|registration]])
  * 03 May: Behavioural equivalences (strong bisimilarity, weak trace equivalence, weak bisimilarity) ([[https://unicam.webex.com/unicam/ldr.php?RCID=b902e38f65c9add99ea4f69efef39dfa|registration]])
  * 08 May: Equivalence checking with TAPAs ([[https://unicam.webex.com/unicam/ldr.php?RCID=9cda8a3ee9bfaa87b6d01a85feac90ed|registration]])
  * 09 May: HML and ACTL logics ([[https://unicam.webex.com/unicam/ldr.php?RCID=b119676c05eb1c1019502485478336a5|registration]])
  * 15 May: Exercises ([[https://unicam.webex.com/unicam/ldr.php?RCID=7af7824830fcb7dc405f8e4e23590a4b|registration]])
  * 22 May: Projects' discussion

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

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**
  * 13/06/2018, 14:00, Polo Lodovici
  * 03/07/2018, 14:00, Polo Lodovici  
  * 18/07/2018, 14:00, Polo Lodovici
  * 12/09/2018, 14:00, Polo Lodovici
  * 26/09/2018, 14:00, Polo Lodovici
  * 27/02/2019, 14:00, Polo Lodovici
  * 25/06/2019, 14:00, Polo Lodovici
  * 09/07/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 **
  * {{ :didattica:magistrale:fmsis:ay_1718:risultati_secondo_parziale_30_maggio_2018.pdf |Results of second partial exam}}
</WRAP>