Fundamentals of Reactive Systems

News

  • 21/1/2019: from 9:00 to 13:00 there will be ALL project presentations.
  • 14/1/2019: second in itinere test
  • 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.
  • Telegram channel: FRS1819@unicam

General Info

Teacher:

ESSE3 Link

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

Course Objectives

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.

Course Contents

  • 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

Study material

Course Slides

Lectures

  • 3/10/2018: general info; reactive systems; process algebraic approach; formal methods for reactive systems (registration)
  • 15/10/2018: LTS; sets; relations (registration)
  • 17/10/2018: equivalences; functions; induction principle; inductively defined sets; inference systems (registration)
  • 22/10/2018: grammars; LTS; syntax of regular expressions (registration)
  • 24/10/2018: operational semantics of regular expressions (registration)
  • 29/10/2018: examples about operational semantics of regular expressions; denotational semantics of regular expressions; axiomatic semantics of regular expressions (registration)
  • 5/11/2018: introduction to Maude: sort, operations, equations (registration)
  • 7/11/2018: Introduction to Maude: rewrite laws; Maude examples (registration)
  • 12/11/2018: Operational semantics of regular expression in Maude (Maude code) (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 (registration)
  • 3/12/2018: CCS examples (registration)
  • 5/12/2018: Seminar on Polymorphic Sessions and Functions.
  • 10/12/2018: Process Algebras operators (basic processes, sequential composition, choice, parallel composition, merge) (registration)
  • 12/12/2018: Process Algebras operators (hiding, recursive definitions, replication) (registration)
  • 19/12/2018: Behavioural equivalences (strong bisimilarity, weak trace equivalence, weak bisimilarity) (registration)
  • 9/1/2019: Exercises on CCS and behavioural equivalences (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. 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

Exams

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

  • …