HyDI: a language for symbolic hybrid systems with discrete interaction. Complex embedded systems consist of software and hardware components that operate autonomous devices interacting with the physical environment. The complexity of such systems makes the design very challenging and demands for advanced validation techniques. Hybrid automata are a clean and consolidated formal language for modeling embedded systems which include discrete and continuous dynamics. They are based on a finite-state automaton structure enriched with invariant and flow conditions to model the continuous dynamics. In this paper, we propose a new language, HYDI, for modeling Hybrid systems with Discrete Interaction. The purpose of the language is to apply state-of-the-art symbolic model checkers for infinite-state systems to the verification of complex embedded systems design. HYDI extends the standard symbolic language SMV with timing and synchronization aspects. The language distinguishes between discrete and continuous variables. Variables inside SMV modules evolve synchronously. Top-level modules represent the asynchronous components of a network and use explicit events to synchronize. The new language is automatically compiled into equivalent discrete-time infinite-state transition systems.
Keywords for this software
References in zbMATH (referenced in 3 articles )
Showing results 1 to 3 of 3.
- Bak, Stanley; Bogomolov, Sergiy; Johnson, Taylor T.: HYST: a source transformation and translation tool for hybrid automaton models (2015)
- Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano: Quantifier-free encoding of invariants for hybrid systems (2014)
- Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano: SMT-based scenario verification for hybrid systems (2013)