When designing embedded systems, often the need arises to model systems having a mixed discrete and continuous behavior. Such hybrid systems commonly consist of a discrete control part that operates in a continuous environment and may be represented by hybrid automata. We recently proposed an open-source framework for hybrid automata analysis, called Ariadne, which exploits approximation techniques based on the theory of computable analysis. In this paper we will show how the approximation capabilities of Ariadne can be used to verify nonlinear hybrid automata inside a design space by means of reachability analysis. In particular, we will use the tool to solve a problem of dominance checking.
Ariadne: Dominance Checking of Nonlinear Hybrid Automata Using Reachability Analysis / L. Benvenuti; D. Bresolin; P. Collins; A. Ferrari; L. Geretti; T. Villa. - STAMPA. - 7550:(2012), pp. 79-91. (Intervento presentato al convegno 6th International Workshop on Reachability Problems tenutosi a Bordeaux, Francia nel 2012) [10.1007/978-3-642-33512-9_8].
Ariadne: Dominance Checking of Nonlinear Hybrid Automata Using Reachability Analysis
BRESOLIN, DAVIDE;
2012
Abstract
When designing embedded systems, often the need arises to model systems having a mixed discrete and continuous behavior. Such hybrid systems commonly consist of a discrete control part that operates in a continuous environment and may be represented by hybrid automata. We recently proposed an open-source framework for hybrid automata analysis, called Ariadne, which exploits approximation techniques based on the theory of computable analysis. In this paper we will show how the approximation capabilities of Ariadne can be used to verify nonlinear hybrid automata inside a design space by means of reachability analysis. In particular, we will use the tool to solve a problem of dominance checking.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.