Algebraic Methods for Model-Checking of Timed and Hybrid Systems – MALTHY

Technology has advanced to the point that computer systems are embedded in almost any physical system from cars, trains, airplanes, robots, medical devices. Embedded systems become ever more complex and safety-critical, asserting their correctness is thus crucial. Today's embedded systems are validated by creating a (finite) number of input stimulis for which the system behaviours are validated via simulation and testing. This is inadequate for safety-critical embedded systems that operate inside some changing and unpredictable environment, and rigorous validation methods should go beyond ``value-based'' analysis and should be able to cope with large sets of unspecified, uncertain behaviors.

Model checking is a technique that can replace infinitely-many simulation runs in order to check if all the executions of a system satisfies a given property, and it has been successfully used for software verification. Embedded systems combine challenges in modelling continuous dynamics and distributed computing systems. The theory of hybrid systems offers a rigorous mathematical framework suitable for reasoning about the interaction between different types of dynamics (discrete and continuous, logical and numerical). For such systems, model checking faces the fundamental problem that almost all interesting properties are formally undecidable. Hence the focus is not on exact verification of properties, but more on approximations of reachable states, for validating safety and liveness properties. However, with modern embedded systems becoming more complex, limitations of the existing model checking tools are showing, due to increasing computational complexity. In this arms race, the most crucial factor for further success of model checking is to have efficient basic data structures and algorithms.

The main objective of this proposal is to advance the state of the art of real-time and hybrid model checking by applying advanced algebraic methods and tools from linear algebra, mathematical programming (convex and semi-algebraic optimization) and tropical geometry. These include new data structures (tropical polyhedra, zonotopes, and ellipsoids) and new algorithms (based on policy iteration or cone programming).

To achieve this objective, we propose to investigate three types of algebraic methods:
- Tropical methods, to handle more efficiently disjunctive invariants which arise in model checking, in particular of timed systems.
- Sub-polyhedral abstract domains, with a view of greatly improving the efficiency of model checking of hybrid systems.
- Convex semi-algebraic methods, to provide more expressive set representation methods allowing more accurate analysis verification of hybrid systems.

The data structures and algorithms resulting from the project will be integrated in the libraries (APRON) and our tools for real-time and hybrid model checking (pyECDAR, HybridFluctuat and SpaceEx) to increase their scope and efficiency.

Furthermore, another important objective of this project is to demonstrate that model checking can be exported to industry and contribute to increase confidence in safety-critical embedded systems design. To this end, we will apply our results to verification of medical devices, through the case studies of infusion pumps provided by the partner Object Direct. This choice of application is motivated by the recent interest in safety of medical devices which are often based on embedded architecture. To ensure their safety, the complex interactions between the devices and the patient physiology should be accurately captured, and for this purpose hybrid systems provide an appropriate modelling framework.