Algorithmic Analysis of Cyber-Physical Systems

Description

Scientific Question. Cyber-physical systems [1] (CPS) consist of interacting computational and physical components. Autonomous systems such as autonomous cars, trains and factories are prominent examples of CPS. As CPS are becoming continuously larger in size, more complex in functionality, and more safety-critical in their applications, it is vital to guarantee their safety and correctness. In order to achieve this goal, we need to investigate formal methods, enabling novel computer-aided verification technologies. This project aims at developing innovative verification techniques to assure safe behaviour of cyber-physical systems.

Hybrid systems [2] are mathematical models that combine discrete and continuous dynamics, which makes them particularly suitable to model CPS. This formalism can capture the behaviour of a large range of real-world systems. For example, systems from automotive and aerospace domains, as well as biological systems can be modelled using the hybrid systems formalism. A number of powerful and scalable tools to verify correctness of hybrid systems have emerged. Although modern tools can analyse systems with up to 100 state variables within a feasible time frame, algorithms scaling still proves to be a major scientific challenge. Therefore, in this project, we will investigate novel algorithmic approaches to accelerate hybrid systems analysis.

Basic Approach & General Tasks. Depending on the student’s preferences and ongoing projects in the lab at the project time, the student will extend some of the following software tools developed in the group of Dr Bogomolov:

  • SpaceEx [3] is an up-to-date hybrid systems analysis tool developed in the Verimag laboratory, France. The group of Dr Bogomolov is involved in the development of SpaceEx and collaborates with Verimag intensively [4]. For example, we have proposed novel methods to find bugs in designs of cyber physical systems based on AI planning techniques and implemented them as part of SpaceEx [5]. SpaceEx is written in C++.
  • HYST [6] is a source-to-source translation tool, currently taking input in the SpaceEx model format, and translating to the formats of some other tools for hybrid systems analysis such as HyCreate[7], Flow*[8] or dReach[9]. In addition, the tool supports generic model transformation passes that serve to both ease the translation and potentially improve analysis results for the supported tools. HYST is written in Java.
  • Hypy is a Python library which extends HYST and encapsulates the necessary machinery to run a number of up-to-date hybrid systems analysis tools, parse their outputs, and modify the models. Note that although model modifications are performed using the HYST machinery, the HYST tool does not run analysis tools nor interpret their output. The developed Hypy library fills this gap, providing an extendable and flexible architecture which simplifies development of complex analysis strategies.

The project will also involve some modelling work. In other words, the student will work on some existing industrial/academic models (or develop new ones) in order to evaluate the developed analysis techniques.

Experience in C++, Java or Python is required. In addition, some knowledge of differential equations and numerical methods will be beneficial.

Finally, we anticipate a paper to be published based on the results of this project. In this way, the student will also gain some experience in preparation of research papers.

 

Updated:  1 November 2018/Responsible Officer:  Head of School/Page Contact:  CECS Marketing