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.

**"Modeling, Simulation and Sensitivity Analysis of Hybrid Systems"**, slides- Paul I. Barton
- Department of Chemical Engineering,
*Massachusetts Institute of Technology*, Cambridge, MA **"Hybrid Automata: A Formal Paradigm for Heterogeneous Modeling"**, slides- Karl Henrik Johansson, John Lygeros, Jun Zhang, and Shankar Sastry
- Department of Electrical Engineering and Computer Science,
*University of California*, Berkeley, CA **"DEVS as a Common Denominator for Multi-formalism Hybrid System Modelling"**, slides- Hans L. M. Vangheluwe
- School of Computer Science,
*McGill University*, Montreal, Canada **"Implicit Model Checking: Formal verification techniqe for large-scale discrete systems"**, slides- Taeshin Park
- MC Research Innovation Center, Inc., Cambridge, MA
**"Formal methods for analysis of heterogeneous models of embedded systems"**, slides- Simin Nadjm-Tehrani
- Department of Computer and Information Science,
*Linköping University*, Linköping, Sweden