Formal verification of basic DEV&DESS formalism using hytech

A hybrid system is a dynamical system reacting to continuous and discrete changes simultaneously. Many researchers have proposed modeling and verification formalisms for hybrid systems, but algorithmic verification of important properties such as safety and reachability is still an on-going research area. This paper demonstrates that a basic modeling formalism for hybrid systems, DEV&DESS, is an easy-to-use input front-end of a widely-used formal verification tool, HyTech. This paper transforms basic DEV&DESS models into linear hybrid automata and performs the HyTech model checking. We are now developing translation rules from DEV&DESS models into linear hybrid automata through various case studies.