Hybrid Systems Modeling and Verification with DEVS (WIP)

Hybrid systems (where continuous and discrete phenomena interact) are found in many natural and artificial systems. An important example, real-time embedded systems usually include discrete-event controllers interacting with a continuous plant. Verifying these real-time systems for correct behavior is of utmost importance, as results of incorrect behavior are usually catastrophic. To complement the use of Modeling and Simulation study of such hybrid real-time systems, we extend here the verification method, based on RTA-DEVS, hybrid Timed Automata and the QSS that was introduced in [1], which allows verifying real-time hybrid systems modeled by DEVS formalism. This extension allows the transformation of the QSS model into overapproximation TA model using interval arithmetic to solve the limitation introduced by the purely integer arithmetic available in UPPAAL.