User Tools

Site Tools


vanbeek:research_subjects

home | research subjects | publications | address

Research subjects

Verification of hybrid systems

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.

Hybrid language and simulator design

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.

Design and optimization of hybrid plants

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:

  1. The time-dependent behavior (throughput, lead-time etc.) of new plant can be predicted by means of simulation.
  2. The current plant may be simulated with different scheduling strategies to determine how operation of the plant can be improved.
  3. The investment in new production equipment can be supported by means of simulation results.

Modelling techniques

  1. Models of large plants can be quite complex. Simulation results need to be reliable, because of the big financial consequences of investment decisions. Experience has shown that use of good modelling techniques can considerably reduce the complexity of the models, and thus increase confidence in their correctness.
  2. Mechanical phenomena are in principle of a continuous nature. In many cases, however, the exact continuous dynamical behavior is not known, or would be too complex to describe. Examples of such cases are dry friction and colliding objects. In such cases, certain phenomena, such as a collision, may be modeled as discrete-events that occur at specific points of time. In this way, model complexity may be considerably reduced. Currently, the choice for a continuous-time or hybrid model depends mainly on the familiarity of a modeler with hybrid languages and his intuition regarding the kind of phenomena that are best represented with hybrid models. An attempt is made to formalize this intuition.

Specification of hybrid simulation models of manufacturing machines

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.

vanbeek/research_subjects.txt · Last modified: Wednesday, 19 March 2008 : 15:56:32 (external edit)