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

BRESOLIN, Davide;GERETTI, Luca;VILLA, Tiziano
2012-01-01

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.
Hybrid Systems; Reachability; Verification
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/11562/473693
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 13
  • ???jsp.display-item.citation.isi??? ND
social impact