PhD defence by Christoffer Sloth

In partial fulfillment of the terms for obtaining the PhD degree, Christoffer Sloth will give a lecture on the following subject:

Formal Verification of Continuous Systems

on Friday 5th of October 2012, 13.00,

in room 0.2.13 at Selma Lagerlöfs Vej 300

Abstract:
The purpose of this lecture is to present a method for verifying timed temporal properties of continuous dynamical systems, and a method for verifying the safety of an interconnection of continuous systems.

Autonomous control plays an important role in many safety-critical systems. This implies that a malfunction in the control system can have catastrophic consequences. A malfunction in the control system of a surgical robot may cause death of patients. However, such systems cannot be formally verified by modern verification techniques, due to the high complexity of both the dynamical system and the specification. Therefore, there is a need for methods capable of verifying complex specifications of complex systems.

The verification of high dimensional continuous dynamical systems is the key to verifying general systems. A method is developed for abstracting continuous dynamical systems by timed automata.

This method is based on subdividing the state space into cells by use of subdivisioning functions that are decreasing along the vector field. To allow the verification of timed temporal properties, continuous systems are abstracted by timed automata; hence, the Lie derivatives of the functions subdividing the state space are used to generate time information for the abstraction. An algorithm for generating the abstraction for polynomial vector fields is developed based on sum of squares programming. In addition, a necessary and sufficient condition is provided for identifying the subdivisioning functions that allow the generation of complete abstractions. A complete abstraction makes it possible to verify and falsify timed temporal properties of continuous dynamical systems, whereas a sound abstraction allows the verification of universally quantified timed temporal properties on positive normal form of continuous dynamical systems.

To allow safety verification of higher dimensional dynamical systems, a compositional safety verification technique is developed. It is shown that dual decomposition can be applied on the problem of generating barrier certificates, resulting in a compositional formulation of the safety verification problem. This makes the barrier certificate method applicable to the verification of high dimensional systems, but at the cost of conservatism in terms of constraining the barrier functions to be additively separable.

The developed abstraction method enables verification of timed specifications for continuous dynamical systems, which other methods are not capable of. In addition, the increased information in the abstraction in terms of time makes the method useful for, e.g., improved safety verification.

Finally, the compositional safety verification allows verification of high dimensional systems.

Members of the assessment committee are Professor Antoine Girard, Université Joseph Fourier, France, Professor John Lygeros, Eidgenossiche Techniche Hochschule, Switzerland, and Professor Anders P. Ravn, Aalborg University, Denmark. Professor Rafael Wisniewski is Christoffer Sloth's supervisor.
All interested parties are welcome. After the defense the department will be hosting a small reception in cluster 1.