Directed Studies: Formal Specification and Verification of Cyber-Physical Systems

Schedule

  • Directed Studies (Dr. Georgiana Caltais)
    Tuesday 10:00 - 11:30  Room: PZ 901
  • Tutorial (Dr. Georgiana Caltais)
    Wednesday 11:45 - 13:15  Room: PZ 1001
  • The preliminary talk will take place at 10:00 on 25 April 2017
     in room PZ 901.

Description

Contents

One of the research areas of great importance in Computer Science is the rigorous modelling and study of cyber-physical systems. These are systems consisting of several interacting computational elements controlling physical entities. Examples of such systems range from platforms for smartphones to programs controlling mechanical devices such as cars, subways or spaceships. In light of their widespread deployment and complexity, the application of accurate methods for the specification, design and reasoning on the behaviour of cyber-physical systems has been a great challenge.

Process algebras have been successfully exploited as prototype specification languages for cyber-physical systems. They come equipped with a notion of syntax, enabling intuitive descriptions of computer systems as “process terms”. The operational semantics of such process terms is conveniently described within frameworks such as SOS, for instance. Reasoning on the compliance between the specification and the actual implementation of a system is typically performed in an equational fashion, or by model-checking the state-based system generated from the aforementioned process terms and their SOS semantic rules.

However, process algebras lack a proper integration of data. In this course, we shall study mCRL2 - as an extended process algebra which contains both data and processes. mCRL2 is supported by an automated tool. The latter shall be exploited in the context of the current course, in order to provide us with a more practical perspective on how the abstract formal framework of process algebras is applied in real-world scenarios.

Additional materials and information are available on ilias.

Participants

Bachelor/Master students

Subject Area

Informatik der Systeme / Angewandte Informatik 

Prerequisites

Ideally, a bachelor level standing in mathematics, theoretical computer science, or software engineering.

Contents / Syllabus

The objective of this course is to equip paticipants with the basic knowledge of terminology and concepts in algebraic process theories and their associated formal verification mechanisms. This can pave the way to carrying out further research in the area of formal methods for concurrency and software engineering.

Final examination (written or oral). A grade bonus can be earned during the tutorials.

180 hours, including 120 hours of presence studies and 60 hours of own studies.

Course taught entirely in English. 

Literature

"Modeling and Analysis of Communicating Systems" - By Jan Friso Groote and Mohammad Reza Mousavi (MIT Press, 2014) 

Further literature references may be suggested during the lectures.

Credits

SWS: 4
ECTS-points:6