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.
L. Benvenuti, D. Bresolin, P. Collins, A. Ferrari, L. Geretti, T. Villa (2012). Ariadne: Dominance Checking of Nonlinear Hybrid Automata Using Reachability Analysis. Springer Berlin Heidelberg [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.
