====== Formal Modeling of Software Intensive Systems ======
----
===== News =====
<WRAP center round important 95%>
  * <wrap em>The date of the project presentations is March 20th</wrap> 
  * December 22th: this lecture is postponed 
  * October 18th: this lecture is postponed
  * October 13th: this lecture is postponed
  * October 6th: this lecture is postponed
  * October 4th: 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 (R. Milner room)
  * Thursday 15 - 17 (R. Milner room)

**Students Office hours**:
  * on appointment (via email), room CS 08, second floor of Polo Tecnologico Palazzo Battibocca, via del Bastione 1, 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_1617:fmsis_intro.pdf |Introduction and general information}}
  * {{ :didattica:magistrale:fmsis:ay_1617:2_-_preliminaries.pdf |Preliminaries}}
  * {{ :didattica:magistrale:fmsis:ay_1617:3_-_formal_semantics_of_regular_expressions.pdf | Formal semantics of regular expressions}}
  * {{ :didattica:magistrale:fmsis:ay_1617:intro-to-pa.pdf | Introduction to Process Algebras}}
  * {{ :didattica:magistrale:fmsis:ay_1617:4_-_ccs.pdf | CCS}}
  * {{ :didattica:magistrale:fmsis:ay_1617:5_-_tapas.pdf | Model and equivalence checking via TAPAs}}

**Lectures**
  * [[https://cmr-em.webex.com/cmr-em-it/lsr.php?RCID=58574c805e6bb9abccd5526b2f6c3873|15 December]]
  * [[https://cmr-em.webex.com/cmr-em-it/lsr.php?RCID=426cf070257127a545e8f805bd4114e1|16 December]]
  * [[https://drive.google.com/open?id=0B2v4obBsNmUOdEFaaUlIWVZpTkE|23 December]] (password: PuSwKri3)
  * [[https://drive.google.com/open?id=0B2v4obBsNmUOR1A3ZkRQSUYzbnc|12 January]](password: 9PxhmF8t)
  * [[https://drive.google.com/open?id=0B2v4obBsNmUOLU1ZTHRnOHFHbGs|13 January]](password: 3tGpp9aV)
  * [[https://drive.google.com/open?id=0B2v4obBsNmUOTjR4S0YxNDRaMDQ|26 January]] (password: 2mNW5Aec)
  * [[https://drive.google.com/open?id=0B2v4obBsNmUOTDV2elRpN0g3YTA|27 January]] (password: mTSTvZM5)
  * [[https://drive.google.com/open?id=0B2v4obBsNmUOWVNsNk9lRnNJZ2s|2 February]](password: FdGTsJA3)
  * [[https://drive.google.com/open?id=0B2v4obBsNmUOVUJGSGp0M3BQeWs|9 February]]
  * [[https://drive.google.com/open?id=0B2v4obBsNmUONHlrU2FadWhXTU0|10 February]]
  * [[https://drive.google.com/open?id=0B2v4obBsNmUORXcxZHJBX2d6Wnc|17 February]]

**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. 2016/2017**
  * Appello I: 28/02/2017 ore 14:00 - Polo Lodovici - AB1
  * Appello II: 16/03/2017 ore 14:00 - Polo Lodovici - AB1
  * Appello III: 05/06/2017 ore 10:00 - Polo Lodovici 
  * Appello IV: 07/07/2017 ore 10:00 - Polo Lodovici
  * Appello V: 21/07/2017 ore 10:00 - Polo Lodovici
  * Appello VI: 06/09/2017 ore 10:00 - Polo Lodovici
  * Appello VII: 20/09/2017 ore 10:00 - Polo Lodovici
  * Appello VIII: 02/10/2017 ore 10:00 - Polo Lodovici

**Results of the written in itinere test of 3/2/2017**
  * 098875: 30
  * 098434: 30
  * 099978: 30
  * 098702: 30
  * 098443: 29
  * 098543: 29
  * 098442: 27
  * 098541: 27
  * 098438: 25
  * 097946: 25
  * 098431: 21
  * 098437: 19

**Results of the written in itinere test of 3/2/2017**
  * 098875 26
  * 098434 26
  * 099978 30
  * 098702 27
  * 098443 26
  * 098543 26
  * 098442 23
  * 098541 26
  * 098438 23
  * 097946 28
  * 098431 25
  * 098437 27
  * 093700 25

**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 **
  * N/A
</WRAP>