Formal Modeling of Software Intensive Systems

Teacher:

• 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

D1 – KNOWLEDGE AND UNDERSTANDING
At the end of the course, the student should be able to:

1. Have the knowledge of the issues concerning concurrent/distributed programming and the modelling of hardware/software systems as software-intensive systems.
2. Have the knowledge of the semantics of the operators of the process algebras CCS, CSP and ACP.
3. 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.
4. Have the knowledge of the main observational behavioural equivalences, weak and strong.
5. 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:

1. Modelling a software-intensive system using the formal languages presented in the course, using a compositional approach.
2. Derive the labelled transition system associated to a process.
3. Decide if one or more state of a labelled transition system are stong or weak bisimilar, providing a suitable bisimulation relation whereas possible.
4. Decide if one or more states of a labelled transition system satisfy formulas of HML and ACTL logics.
5. Define temporal properties of a software-intensive system using the HML and ACTL logics.
6. 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:

1. 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:

1. Write a clear report on the modelling and analysis of a system under study using a formal style.
2. 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:

1. Search the scientific literature for specific advances in formalisms and tools aimed at modelling and verifying software-intensive systems.
2. Autonomously understand and learn to use new features added to tools for modelling and verifying software-intensive systems.

• 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

Course Slides

• Introduction and general information
• Preliminaries
• Formal semantics of regular expressions
• CCS
• A gentle introduction to Process Algebras

Lectures

• 6 March: general info; sw intensive systems; process algebraic approach; formal methods for reactive systems (registration)
• 7 March: LTS; sets; relations (registration)
• 13 March: equivalences; functions; induction principle; inductively defined sets (registration)
• 14 March: inference systems; grammars; LTS (registration)
• 20 March: syntax and operational semantics of regular expressions (registration)
• 21 March: examples about operational semantics of regular expressions (registration)
• 27 March: denotational semantics of regular expressions; axiomatic semantics of regular expressions (registration)
• 28 March: CCS (registration)
• 4 April: CCS examples (registration)
• 11 April: First in itinere test.
• 12 April: CCS examples; TAPAs (registration)
• 18 April: Process Algebras operators (basic processes, sequential composition, choice) (registration)
• 26 April: Process Algebras operators (parallel composition, merge, hiding, recursive definitions, replication) (registration)
• 02 May: Presentation of the course's project. Behavioural equivalences (strong trace equivalence) (registration)
• 03 May: Behavioural equivalences (strong bisimilarity, weak trace equivalence, weak bisimilarity) (registration)
• 08 May: Equivalence checking with TAPAs (registration)
• 09 May: HML and ACTL logics (registration)
• 15 May: Exercises (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

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

• Results of second partial exam