A formal semantics of the hybrid Chi language has been developed. The semantics of Chi is expressed in terms of a Labeled Transition System (LTS), defined in a Structural Operational Style (SOS). The Chi language has been designed with the objective of integrating continuous-time and discrete-event concepts, and is especially suited to specification of large and complex systems. It integrates the dynamics and control world view with the computer science world view. We aim to verify properties of hybrid systems specified in Chi by means of a formal translation to hybrid automata.
We use the formal semantics for improving the efficiency of the simulator by rewriting Chi models to a form for faster simulation. In the framework of the European network of excellence HYCON, workpackage 3: Tool Integration, we are integrating the Chi simulator with other simulators, such as Matlab/Simulink and Modelica.
Models have been made, among others, of parts of a beer brewery containing hundreds of tanks, a complete fruit juice production and packaging plant, and a pipeles batch plant for emulsion polymerization using mobile reactors. Simulation of such models gives insight in the dynamic behavior of the plants. Simulation results can be used in many ways to improve the plant. Some examples are:
Models of manufacturing machines can be connected to a model of a (discrete-event) control system for simulation based testing. It is our aim to use the model of the control system also for actual real-time control.