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.

Hybrid Systems and Verification by Abstraction

M. D. Di Benedetto;DI GENNARO S;A. D’Innocenzo
2015-01-01

Abstract

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.
978-3-319-10794-3
978-3-319-10795-0
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11697/25550
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? ND
social impact