Formal Verification of Continuous Systems

The purpose of this thesis is to develop a method for verifying timed temporal properties of continuous dynamical systems, and to develop a method for verifying the safety of an interconnection of continuous systems. The methods must be scalable in the number of continuous variables and the verification procedures should be algorithmically synthesizable.

Autonomous control plays an important role in many safety-critical systems. This implies that a malfunction in the control system can have catastrophic consequences, e.g., in space applications where a design flaw can result in large economic losses. Furthermore, a malfunction in the control system of a surgical robot may cause death of patients. The previous examples involve complex systems that are required to operate according to complex specifications. The 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. In this thesis, an abstraction approach is taken to the verification problem. 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, the continuous systems are abstracted by timed automata; hence, the Lie derivatives of the functions subdividing the state space are also 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.