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.