Many of today's industrial systems exhibit mixed discrete-event/continuous-time behaviour. Typical examples are batch processes from the process industry, digitally controlled plants, automobiles and aircraft. Models play an important role in the design process of such systems, providing means to evaluate design decisions at an early stage. Models written in a specification formalism present only the relevant system aspects. Such models contribute significantly to the understanding of the functionality of the systems. Hybrid systems are used increasingly in safety-critical applications, and therefore, their reliability is becoming more and more important. For verification purposes, formal semantic models and frameworks are used.
The Chi language is a hybrid specification formalism, suitable for the description of discrete-event, continuous-time and hybrid systems. It is a concurrent language, where the discrete-event part is based on Communicating Sequential Processes and the continuous-time part is based on Differential Algebraic Equations (DAEs). Models written in the Chi language can be executed by the Chi simulator.
The contribution of the present work is twofold. First, the hybrid Chi language semantics is specified. This is an extension to the discrete-event semantics that had already been developed in a previous work. Second, the existing discrete-event simulator has been extended to execute hybrid models. To make a specification language suitable for the design and analysis of complex systems, it needs to have a precise semantics. Specifically, a hybrid language semantics has to preserve the pure continuous-time and the pure discrete-event functionality while integrating the two smoothly. In the case of the Chi language, it is also important that models can be executed efficiently, using existing numerical algorithms.
Differential and algebraic variables with corresponding operators are defined in the Chi language. This distinction emphasizes the physical role of the variables, and in this way supports the development of physically correct models. Steady-state initialization is supported directly by the language. Currently, index 0 and 1 systems of DAEs can be solved directly. Higher index systems can be modelled by using substitute equations.
The semantics of model composition is an important issue in hybrid languages. Model composition is well defined for pure discrete models by CSP. This thesis treats the continuous aspects of model composition. Continuous variables of sub-models are connected by the so-called channels in the Chi language. After studying existing hybrid languages, algebraic equations have been chosen to be the meaning of connections between continuous variables. This, together with using only local variables in processes, have contributed significantly to more clear and robust models. Furthermore, state-event conditions are evaluated only in consistent states leading to more predictable model behaviour.
The mathematical model of continuous state calculation is specified together with the hybrid language semantics; the latter in the form of a computational model. According to this model, discrete phases are divided into sub-phases, each ending with a consistent initial state calculation. Within each sub-phase, processes work with local variables only and interaction between sub-models is restricted to explicit communication. This simplifies reasoning about model behaviour.
The Chi simulator has been extended to execute hybrid models. It integrates a nonlinear equation solver to solve the initial state problem and a DAE solver to solve the DAEs during the continuous phases. The local continuous variables of processes are dynamically mapped onto a global variable set that the solvers work with, to increase performance. The Chi simulator allows sophisticated logging of continuous variables, such that their trajectory can be visualized by third party software. The user may also request a detailed trace file to be generated.
In the future, formal methods and techniques should be developed, based on the operational semantics defined in this thesis, to carry out formal analysis of hybrid Chi models. A possible extension to the Chi language is to include dimension information in the data types. In the present work, it is proposed to perform physical correctness checking based on this information. To extend the range of the physical systems that can be modelled in Chi, it is necessary to be able to specify the so-called instantaneous equations. The performance of the Chi simulator can further be enhanced by optimizing the equations, based on symbolic analysis and manipulation.
Ph.D.thesis, Eindhoven University of Technology, 1999.