Hybrid Systems and Verification by Abstraction

The increase of functionality offered by today’s control systems based on embedded systems requiresmore effort to verify the controlled system, as amalfunction can yield catastrophic results. These systems are usually hybrid systems, mixing continuous and discrete dynamics. When analyzing a hybrid system, the dimension of the state space is often so large that formal verification is out of the question. Its analysis can be carried out using abstraction, namely constructing a system with a smaller state space, preserving the properties to verify in the original system. Making use of a notion of diagnosability for hybrid systems, generalizing the notion of observability, in this paper it is shown an abstraction procedure translating a hybrid system into a timed automaton, in order to verify observability and diagnosability properties. The subclass of hybrid systems here considered is that of the durational graphs. We propose a procedure to check diagnosability, and show that the verification problem belongs to the complexity class P. This procedure is applied to an electromagnetic valve system for camless engines.