| Chair | Pieter J. Mosterman
Institute of Robotics and Mechatronics DLR Oberpfaffenhofen Tel. +49 8153 282434 |
Co-Chair | Hans Vangheluwe
School of Computer Science McGill University Tel. 514 398 44 46 |
For their execution, different formalisms such as bond graphs, differential-algebraic equation based object diagrams, state charts, and Petri nets rely on different computational models where a distinct difference between continuous and discrete event behavior exists: Even though continuous behavior is typically generated by discretizing in time, the numerical solvers used for this purpose rely on the premise that interpolation polynomials with a certain degree of smoothness, continuity, can be applied. Furthermore, communication requirements are much more stringent than for discrete event message passing. Typically, one integration step requires several evaluations of the system differential equations, possibly adapting the time step to control the integration error. This distinction between continuous and discrete behavior is fundamental to analyses such as simulation and verification of heterogeneous models and requires methodologies especially designed for mixed continuous/discrete, hybrid, dynamic systems.
Paper 1 [Paul I. Barton] addresses the consequences and technicalities of the interaction between discrete and continuous behavior domains. For example, when discrete events occur, discontinuities in otherwise smooth gradients may occur and discontinuous changes, jumps, of continuous state variables may take place. Modeling these phenomena in a clean and unambiguous way is addressed, as well as the numerical issues involved. For example, the detection of continuous variables crossing threshold values (state events) is critical to handle complex hybrid behaviors. Another issue is the possibility of run-time changes of system complexity (i.e., its index) that can sometimes be prevented by appropriate hybrid modeling techniques. Furthermore, standard continuous sensitivity analyses used in, e.g., optimal control design, do not apply when discontinuities in the continuous trajectories take place and new approaches have to be developed.
Paper 2 [Karl Henrik Johannson, John Lygeros, Shankar Sastry, and Jun Zhang] discusses some of the pitfalls of hybrid system behavior generation. It shows how execution of a hybrid dynamic system may not have a unique solution, i.e., a sort of continuous nondeterminism, or have no solution trajectory at all, i.e., no continuous behavior specification satisfies the discrete system invariant. In these cases, hybrid behavior generation requires regularization of solutions which applies implicit system knowledge to make additional constraints explicit that allow unique behavior generation.
Paper 3 [Hans Vangheluwe] To facilitate different formalisms, this paper presents a Formalism Tranformation Graph (FTG), a structure in which vertices correspond to formalisms, and edges denote whether a formalism transformation exists, is presented. A transformation is a mapping of models in the source formalism onto models in the destination formalism (with invariance of behavior). This traversal is the basis for meaningfully coupling models in different semantics: once they can be mapped onto a common formalism, closure (the coupling of sub-models in formalism F is again a valid model in formalism F) in that formalism makes the meaning of the coupled model explicit. In the context of hybrid system models, the formalism transformation converges to a common denominator which unifies continuous and discrete constructs. Typically, this is some form of event-scheduling/state event locating/differential equation formalism and corresponding solver. This paper presents a radically different approach that maps all formalisms onto Zeigler's Discrete Event System Specification (DEVS). In essence, the state variables of the continous models are discretized rather than time and the DEVS transition function will repeatedly go from one discretized state value to either the one just above or the one just below giving as output, the time till the next transition.
Paper 4 [Taeshin Park] introduces the verification problem of large systems, e.g., chemical plants. Because of the heterogeneous nature of the modeling formalisms applied, the underlying representation of such models is typically a hybrid formulation and the dense domain of continuous variables precludes the use of standard discrete state verification methods. These methods rely on explicit formulation of system behavior, and in case of the continuous domain this explicitness quickly becomes intractable, i.e., brute force exhaustive model checking (as implemented in commercial tools) becomes prohibitive (except for special cases with few continuous variables). Hybrid system verification seeks to overcome this problem by use of modularization techniques and symbolic model checking, which relies on model checking methods combined with ordered binary decision diagram (OBDDs) representations. An alternative approach is presented where system models are formulated in their implicit form, which is amenable to symbolic processing and does not require exhaustive behavior generation.
Paper 5 [Simin Nadjm-Tehrani] discusses another alternative, the use of formal methods in verification of hybrid systems. This approach is based on reperesenting the system model in languages with formal semantics, which enables translations to tools based on mathematical logic. Proof systems and static analysers can be used to perform "sanity checks" on the controller alone, e.g. proving that the controller is causal, deterministic, and has a reaction for every input. This means proving properties of an instance based on formalized characteristics of a meta model. The "proof" in this case is simply a pass at compilation stage.
Moreover, under certain restrictions on the plant (e.g. piecewise linearity), one can represent the closed loop models in the same deductive environment. This facilitates proving system properties (e.g. that an unsafe state is never reached, or given an input sequence the desired response will appear within a bounded number of steps). Here, the application of these techniques within the synchronous family of languages (Lustre, Signal, Esterel, Statecharts) will be discussed. Also, possibilites of combining discrete analysis with continuous analysis in mixed tool environments (Statecharts/MatrixX, Signal/Simulink) are described.