Integration of Model-Checking Tools: from Discrete to Hybrid Models

To develop correct models for Hybrid and Discrete control systems requires a modeling language to express all important aspects of system behavior. Enabling one modeling language to understand the models developed in other languages is a challenge in re-usability of models. In this paper we have integrated a model-checking UppAal tool (Timed Automata) with HYTECH model-checker (Hybrid Automata) by extending UppAal syntax with hybrid aspects. We also contribute to abstract syntax for the modeling language of UPPAAL tool. The integration of both tools and enhanced expressiveness allows UPPAAL to model hybrid systems and get them verified by HYTECH tool.