Search

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.

This paper proposes an LMI-based algorithm for abstracting dynamical systems by timed automata, which enables automatic formal verification of linear systems. The proposed abstraction is based on partitioning the state space of the system using positive invariant sets, generated by Lyapunov functions. This partitioning ensures that the vector field of the dynamical system is transversal to all facets of the cells, which induces some desirable properties of the abstraction. The algorithm is based on identifying intersections of level sets of quadratic Lyapunov functions, and determining the minimum and maximum time that a trajectory of the system can stay in a set, defined as the set-difference of sub-level sets of Lyapunov functions. The proposed algorithm applies for linear systems and can therefore be efficiently implemented using LMI-based tools.

This report is the deliverable 2.4 in the project Distributed Control ofLarge-Scale Oshore Wind Farms with the acronym Aeolus. The objectiveof this deliverable is to provide an understanding of the wind eld model anddynamic variations superimposed on the mean eld.In this report a dynamical model is developed for the wind ow in a wind farm based on nite volume method. Afterwards the model is transferred into a discrete framework called combinatorial, which determines the future behavior of the discrete system. In this regard, the dynamical model is de-rived and it is explained in terms of ordinary dierential equations (ODE).Considering some assumptions on the ow model (e.g. steadiness), the sys-tem can be approximated by a linear n dimensional system. Partitioningthe state space into cells is performed by dening Lyapunov function sets,such that each cell is the region between two neighboring level surfaces ofLyapunov functions. The resulting discrete system facilitates a supervisoryapproach to the control.