Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Cyber-Physical Systems (CPS) are a class of computerised system that integrate discrete computation with continuous physical processes. CPS are typically developed using a combination of discrete and continuous models, often in differing heterogeneous languages. This makes verification of trustworthiness challenging. There is a need for unifying semantic models to allow the integration of heterogeneous system components, whilst ensuring that a given set of safety properties is supported. Hoare and He’s Unifying Theories of Programming (UTP) has been designed as a framework in which the integration of languages, through the common semantic domain of the alphabetised relation calculus, can be achieved. Semantic models for discrete modelling languages in UTP are already numerous [13, 26, 30, 36], and, therefore, in this paper we focus on semantics of continuous models in the Modelica language.

Modelica [22] is a widely used language for description and modelling of hybrid dynamical systems that compose a continuously evolving physical plant with a discrete controller. Such systems are described using a mixture of differential-algebraic equations (DAEs), and event guards that trigger discontinuous jumps in system behaviour by execution of discrete equations and algorithms – so called “hybrid DAEs”. Modelica has a number of commercial implementations including DymolaFootnote 1, Wolfram SystemModelerFootnote 2, MapleSimFootnote 3 and the open-source implementation, OpenModelicaFootnote 4. However, the Modelica language has an incomplete formal semantics; though the semantics of DAEs is well known, the event iteration system currently does not have a formal semantics. Here we give a denotational semantics to a fragment of Modelica using a UTP theory of hybrid relations. Additionally to clarifying the semantics of Modelica, this allows us to consider the combination of continuous and discrete models through common theoretical factors and theory linking.

Our approach to giving a semantics to Modelica is three-fold. Firstly, we create a UTP theory of hybrid relations, building on the work of He [14, 15], Zhou [32, 33], Zhan [21], and others. This theory extends the alphabet of UTP predicates with continuous variables \(\underline{c} \in \mathrm {con}\alpha \) and is defined by novel healthiness conditions that characterise these variables as piecewise continuous functions.

Secondly, we define the operators of our hybrid relational calculus, which is similar to the imperative subset of \(\mathcal {HCSP}\)  [34], but extended with an interval operator [33] that provides a continuous specification statement. In particular we provide support for semi-explicit DAEs and continous variable preemption. As with Hybrid CSP, we base the denotational semantics around the Duration Calculus [33], though the semantics is purely relational. Moreover, we provide a uniform account of both discrete and continuous variables by linking the latter to discrete “copy” variables that give the valuation at the beginning and end of a continuous evolution. Thus, both discrete and continuous variables can be manipulated with the same operators; in the latter case this provides initial value constraints. Our model of hybrid relations has also mechanised in our UTP proof assistant, Isabelle/UTP  [10], that provides theorem proving facilities.

Thirdly, we define a preliminary denotational semantics for Modelica through a mapping into the hybrid relational calculus. This mapping primarily considers the event-handling mechanism of Modelica, whereby specific conditions on continuous variables can lead to both discontinuous jumps in variables, and also changes to the equations active in the DAE system.

The remainder of our paper is structured as follows. In Sect. 2, we provide background on hybrid systems by briefly surveying the literature, with particular emphasis on works related to the UTP. In Sect. 3 we briefly describe the UTP, and in Sect. 4 we introduce the Modelica language. In Sect. 5, we describe our UTP theory of hybrid relations. In Sect. 6, we use our UTP theory to build a hybrid relational calculus, including operators for specifying continuous invariants, differential equations, and preemption. In Sect. 7, we outline our mechanisation of the hybrid relational calculus in Isabelle [10, 23]. In Sect. 8, we use our hybrid relational calculus to give a high-level denotational semantics to the Modelica language, focusing principally on the interaction between evolution of DAEs and the event handling system. Finally in Sect. 9, we draw conclusions.

2 Related Work: Hybrid Systems

The majority of the work on hybrid systems takes inspiration from Hybrid Automata [16], an extension of finite state automata that allows the specification of continuous behaviour. A hybrid automaton consists of a finite set of states labelled by ODEs, a state invariant, and initial conditions. The states (or “modes”) are connected by transitions that are labelled with jump conditions and (optionally) events. Whilst in a state the continuous variables evolve according to the system of ODEs and the given invariant; this is known as a flow as the variable values continuously flow from one value to another. When one of the jump conditions of an outgoing edge is satisfied, the event, if present, can instantaneously execute, potentially resulting in a discontinuity, and the targeted hybrid state is activated. Thus a hybrid automata is characterised by behaviour that includes both continuous flows also discrete jumps. Hybrid automata are given a denotational semantics in terms of piecewise continuous functions [16] \(\mathbb {R} \rightarrow \mathbb {R}^n\), also called trajectories, that are continuous except for in a finite number of places.

Verification of hybrid systems was made possible through the seminal work of Platzer [27]. This work develops a logic called Differential Dynamic Logic (\(\textsf {d}\mathcal {L}\)) that allows us to specify invariants over both discrete and continuous variables. Hybrid systems are modelled using a language of hybrid programs, that combines the usual operators of an imperative language with continuous behaviour specified by differential equations. Hybrid programs are equipped with a relational semantics, and a proof calculus for \(\textsf {d}\mathcal {L}\) allows reasoning about hybrid programs. An implementation of \(\textsf {d}\mathcal {L}\) called KeYmaera [27] allows the automated verification of systems modelled as hybrid programs. Our notion of hybrid relation is inspired by Platzer’s hybrid programs, though we focus on a UTP denotational semantics as opposed to an operational semantics. Our own setting of the Duration Calculus [33] provides us with the necessary machinery to similarly justify a dynamic logic. Moreover, we observe that, with a UTP model, we are in a strong position to extend the work to deal with concurrent hybrid programs, a notion that \(\textsf {d}\mathcal {L}\) does not consider.

Concurrency is considered in Hybrid CSP [14, 34] (\(\mathcal {HCSP}\)), an extension of Hoare’s process calculus CSP [17] that adds support for continuous variables as described by differential equations and modelled by standard trajectories, in a similar manner to hybrid automata. \(\mathcal {HCSP}\)  [14] extends CSP with continuous variables whose behaviour is described by differential equations of the form \(\mathcal {F}(\dot{s}, s) = 0\). Interaction between discrete and continuous behaviour takes the form of preemption conditions on continuous variables, timeouts, and interruption of a continuous evolution through CSP events. \(\mathcal {HCSP}\) has a denotational semantics that is presented in a predicative style similar to the UTP [18].

Further work on \(\mathcal {HCSP}\)  [34] enriches the language to allow explicit interaction between discrete and continuous variables. This is achieved through a novel denotational semantics in terms of the Extended Duration Calculus [35], which treats variables as piecewise continuous functions. This allows a more precise semantics for operators like preemption that are defined in terms of suitable variable limits. A Hoare logic for this calculus is presented in [21], through the adoption of Platzer’s differential invariants, along with an operational semantics. Our work is heavily influenced by \(\mathcal {HCSP}\), though we focus on formalising the sequential aspects of hybrid systems, and so formalise a subset of the operators with refined definitions. Our operators formalise continuous after variables by explicitly considering left-limits which is important for Modelica event iteration.

A theorem prover for \(\mathcal {HCSP}\) called, HHL Prover [37], has also been developed and applied to verification of Simulink diagrams through a mapping into \(\mathcal {HCSP}\)  [31]. More recently the fundamentals of hybrid system modelling have been studied in a purely UTP relational setting [15]. This work has produced a language called the Hybrid Relational Modelling Language [15] (HRML), which draws on \(\mathcal {HCSP}\), but uses signals rather than CSP’s events as the main communication abstraction. Our notation is agnostic in this respect, and could be extended either to support the event or signal paradigm.

Duration Calculus [33] (\(\mathcal {DC}\)) provides specification of invariants over the continuous time domain, in order to facilitate verification real-time systems. For example, we can write \(\left\lceil x^2 > 7 \right\rceil \), which specifies all possible intervals of over which \(x^2 > 7\) is invariant. The chop operator \(P \mathop {\circ } Q\) specifies that an interval may be broken into two subsequent intervals, over which P and then Q hold, respectively. \(\mathcal {DC}\) has been extended to provide a semantics for hybrid real-time systems modelling [35], which is then used to give semantics to \(\mathcal {HCSP}\)  [34]. \(\mathcal {DC}\) can also be used to give an account to typical operators of modal and temporal logics. Thus, grounding our semantics in \(\mathcal {DC}\) enables us to form continuous specifications about hybrid systems. Different to \(\mathcal {DC}\) we provide a purely relational UTP semantics, and also explictly distinguish continuous and discrete variables, instead of modelling the latter as step functions. This distinction allows us to retain standard relational definitions of the majority of discrete UTP operators.

3 Unifying Theories of Programming

Unifying Theories of Programming [4, 18] (UTP) is a framework for the specification of formal semantics. It is based on the idea that any temporal model can be expressed as an alphabetised predicate that describes how variables change over time. This idea of “programs-as-predicates” means that the duality of programs and specifications all but disappea,rs, as programs are just a subclass of specifications. This powerful idea provides a strong basis for unification of heterogeneous languages and semantic models, since many different shapes of models can be given a uniform view. The UTP further allows that different semantic presentations, such as denotational, algebraic, axiomatic, and operational, can be formally linked through mutual embeddings. This ensures that consistency is maintained between semantic models and that tools that implement them can be combined for multi-pronged analysis and verification of models [10].

Concretely, an alphabetised relation is a pair \((\alpha P, P)\) where \(\alpha P\) is the alphabet and P is a predicate all of whose free variables belong to \(\alpha P\). The alphabet can in turn be subdivided \(\alpha (P) = \mathrm {in}\alpha (P) \cup \mathrm {out}\alpha (P)\), with input variables \(x, y \in \mathrm {in}\alpha (P)\) and output variables \(x',y' \in \mathrm {out}\alpha (P)\). The calculus provides the operators typical of first order logic. UTP predicates are ordered by a refinement partial order \(P \sqsubseteq Q\) that also defines a complete lattice. Imperative programs can be described using relational operators, such as sequential composition , if-then-else conditional , assignment \(x :=_A v\) (for expression v and alphabet A), and skip , all of which are given predicative interpretations.

More sophisticated language constructs can be expressed by enriching the theory of alphabetised relations to create UTP theories. A UTP theory consists of (i) a set of observational variables, (ii) a signature, and (iii) a set of healthiness conditions. The observational variables record behavioural semantic information about a particular program. For example, we may have an observational variable for recording the current time called \(clock : \mathbb {R}\). The signature uses these operational variables to encode the main operators of the target \({{\varvec{\mathsf{{ ht}}}}}\) language.

The domain of a UTP theory can be constrained through healthiness conditions, which act as invariants over the observational variables. For example, it is intuitively the case that time only moves forward, and so a relational observation like \(C \triangleq clock = 3 \wedge clock' = 1\) ought not to be possible. We can eliminate this kind of behaviour description with an invariant \(clock \le clock'\). In the UTP such conditions are expressed as idempotent functions, for example , so that healthiness of a predicate P can be expressed as a fixed point equation: . If we apply to C, the result is miraculous predicate and thus C is excluded from the theory signature.

UTP theories can be used to describe a domain useful for modelling particular problems – for instance, we can add further conditions to to provide a theory of real-time programs. UTP theories can also be composed to produce modelling domains that combine different language aspects. Put more simply, UTP theories provide the building blocks for a heterogeneous language’s denotational semantics [9]. Such a denotational semantics provides the “gold standard” for the meaning of language constructs and can then be used to derive other presentations, such as operational and, very often, algebraic.

4 Modelica

Modelica is an equation-based object-oriented language for describing the dynamic behaviour of CPS, standardised by the Modelica Language Specification (MLS) [22]. The MLS is described using English; therefore, its semantics is to some extent subject to interpretation. Quoting from [22, Sect. 1.2]: “The semantics of the Modelica language is specified by means of a set of rules for translating any class described in the Modelica language to a flat Modelica structure. A class must have additional properties in order that its flat Modelica structure can be further transformed into a set of differential, algebraic and discrete equations (= flat hybrid DAE). Such classes are called simulation models.”

Figure 1 illustrates the basic idea. The squiggle arrow denotes a degree of fuzziness — a simulation result is an approximation to the, in general, inaccessible exact solution of the equation system and the specification does not prescribe a particular solution approach. A classical model for a hybrid systems is the bouncing ball. A possible Modelica implementation for a ball with mass \(1\,\mathrm {kg}\) and an impact coefficient of 0.8 that falls from an initial height of \(h=1\,\mathrm {m}\) is given in Fig. 2. When the ball hits the ground, it changes its velocity v discontinuously and bounces back. and denote the time derivatives \(\dot{h}\) and \(\dot{v}\) of variables h and v, respectively. The acceleration to the ground is determined by earth’s gravitational acceleration \(g=9.81\,\mathrm {m}/\mathrm {s}^2\). The discontinuous change of variable v is modelled using a conditionally activated reinitialization equation. The ball hits the ground when condition \(h<0\) becomes true. The operator is used for reinitializing v with the negative value of v (times the impact coefficient) just before condition \(h<0\) becomes true ( returns the left limit of variable v at the event instant).

Fig. 1.
figure 1

From model to simulation result.

Full size image
Fig. 2.
figure 2

Bouncing ball in Modelica.

Full size image

Several formal specification approaches have been used to give semantics to subsets of the Modelica language. Most of the approaches describe the instantiation and flattening of Modelica models (i.e., the static semantics, corresponding to the first stage in Fig. 1) [1, 20, 28] while others are restricted to discrete-time language subsets [29].

Flat Modelica can be conceptually mapped to a set of differential, algebraic and discrete equations of the following form [22, Appendix C]:

  1. 1.

    Continuous-time behaviour. The system behaviour between events is described by a system of differential and algebraic equations (DAEs):

    $$\begin{aligned} f\big (x(t),\dot{x}(t),y(t),t,m(t_e),m_{\mathrm {pre}}(t_e),p,c(t_e)\big )&= 0 \end{aligned}$$
    (1a)
    $$\begin{aligned} g\big (x(t),y(t),t,m(t_e),m_{\mathrm {pre}}(t_e),p,c(t_e)\big )&= 0, \end{aligned}$$
    (1b)

    where t denotes time; p is a vector of parameters and constants; x(t) is a vector of dynamic variables of type Real and \(\dot{x}(t)\) is the vector of its derivatives; y(t) is a vector of algebraic variables of type Real; \(m(t_e)\) is a vector of discrete-time variables of type discrete Real, Boolean, Integer, or String which changes only at event instants \(t_e\); \(m_{\mathrm {pre}}(t_e)\) are the values of m immediately before the current event at event instant \(t_e\); and \(c(t_e)\) is a vector containing all Boolean condition expressions, e.g., if-expressions.

  2. 2.

    Discrete-time behaviour. The behaviour at an event at time \(t_e\) is described by following discrete equations:

    $$\begin{aligned} m(t_e)&:= f_m\big (x(t_e),\dot{x}(t_e),y(t_e),m_{\mathrm {pre}}(t_e),p,c(t_e)\big ) \end{aligned}$$
    (2)
    $$\begin{aligned} c(t_e)&:= f_e\big (m^{\mathbf {B}}(t_e),m_{\mathrm {pre}}^{\mathbf {B}}(t_e),p^{\mathbf {B}},rel(v(t_e))\big ). \end{aligned}$$
    (3)

    An event fires if any of the conditions \(c(t_e)\) change from false to true. The vector-valued function \(f_m\) specifies new values for the discrete variables \(m(t_e)\). The vector \(c(t_e)\) is defined by the vector-valued function \(f_e\), which contains all Boolean condition expressions evaluated at the most recent event \(t_e\); \(rel(v(t_e)) = rel([x(t);\dot{x}(t);y(t);t;m(t_e);m_{\mathrm {pre}}(t_e);p])\) is a Boolean-typed vector-valued function containing variables \(v_i\), e.g., \(v_1 > v_2,~v_3 \ge 0\); \(m^{\mathbf {B}}(t_e)\) is a vector of discrete-time variables of type Boolean, \(m^{\mathbf {B}}(t_e) \subseteq m(t_e)\), and \(m_{\mathrm {pre}}^{\mathbf {B}}(t_e)\) are the values of \(m^{\mathbf {B}}\) immediately before the current event at event instant \(t_e\); \(p^{\mathbf {B}}\) are parameters and constants of type Boolean, \(p^{\mathbf {B}} \subseteq p\).

Simulation means that an initial value problem (IVP) is solved. The equations define a DAE which may have discontinuities and a variable structure and may be controlled by a discrete-event system.

5 Theory of Hybrid Relations

We now proceed to describe our theory of hybrid relations to enable the definition of a relational calculus for modelling sequential hybrid processes. Our model unifies the treatment of discrete and continuous variables so that the same operators may be used for manipulating both. In Modelica, DAEs are used to describe continuously evolving dynamic behaviour of a system. Thus, in the UTP, we first introduce a theory of continuous time processes that embeds trajectories into alphabetised predicates and shows how continuous variables evolve over a given interval. These intervals are used to divide up the evolution of a system into piecewise continuous segments.

Our theory is based on vanilla UTP alphabetised relations, and so is insensitive to termination and stability of continuous processes. Following the UTP philosophy, we consider hybrid behaviour in isolation, and then later augment it with additional structure to allow the finer expression of such properties. Our theory can, for instance, be embedded into timed reactive designs [13, 30].

Alphabet. Our model of continuous time introduces observational variables \( ti , ti ' : \mathbb {R}_{\ge 0}\) that define the start and end time of the current computation interval, as in \(\mathcal {DC}\)  [35]. We also introduce the expression \(\ell \) to denote the duration of the current interval, where \(\ell \triangleq ti ' - ti \).

As already said, the alphabetised relational calculus divides the alphabet into input \(\mathrm {in}\alpha (P)\) and output variables \(\mathrm {out}\alpha (P)\). Inspired by [15], we add a further subdivision \(\underline{x}, \underline{y}, \underline{z} \in \mathrm {con}\alpha (P)\), the set of continuous variables, that is orthogonal to the discrete program variables, that is \(\mathrm {con}\alpha (P) \cap (\mathrm {in}\alpha (P) \cup \mathrm {out}\alpha (P)) = \emptyset \). The elements of \(\mathrm {con}\alpha (P)\) are the variables to be used in differential equations and other continuous constructs.

We assume that all variables consist of a name, type, and optional decoration. For example, the name in the variables x, \(x'\), and \(\underline{x}\) is the same – x – but the decorations differ. We introduce the distinguished continuous variable \(\underline{t}\) that denotes the current instant in an algebraic or differential equation. An alphabetised predicate P whose alphabet can be so partitioned, i.e. \(\alpha (P) = \mathrm {in}\alpha (P) \cup \mathrm {out}\alpha (P) \cup \mathrm {con}\alpha (P)\), is called a hybrid relation.

Continuous variables come in two varieties that allows us to talk about a particular instant or about the whole time continuum:

  • instant variables – these are continuous variables of type \(\mathbb {R}\) that refer to the value at a particular instant;

  • trajectory variables – these are time-dependent variables of type \(\mathbb {R}_{\ge 0} \rightarrow \mathbb {R}\) and give the values over a whole trajectory.

Trajectory variables are total rather than partial functions. This has the advantage that composition operators need not consider explicit combination of trajectories through overriding. Instead, composition further constrains the trajectory functions, potentially over disjoint time domains (as is the case for;). Valuations of the trajectory exist outside \([ ti , ti ')\), but they have no relevance.

We require that each trajectory variable \(\underline{x} : \mathbb {R}_{\ge 0} \rightarrow \mathbb {R}\) is accompanied by discrete before and after “copy” variables with the same name – \(x, x' : \mathbb {R}\) – that record the values at the start and limit of the current interval. This, crucially, allows us to use the standard operators of relational calculus for manipulating continuous variables via discrete copies. This allows us to consider the set of purely discrete variables that are not discrete copies of a continuous variable:

$$\mathrm {dis}\alpha (P) = \{x \in \mathrm {in}\alpha (P) ~|~ \underline{x} \notin \mathrm {con}\alpha (P)\} \cup \{x' \in \mathrm {out}\alpha (P) ~|~ \underline{x} \notin \mathrm {con}\alpha (P)\}$$

We introduce the following \(\mathop { @ }\) operator borrowed from [6] that lifts a predicate in instant variables to one in trajectory variables.

Definition 1

Continuous variable lifting

$$\begin{aligned} P \mathop { @ }\tau\triangleq & {} \{\underline{x} \mapsto \underline{x}(\tau ) ~|~ \underline{x} \in \mathrm {con}\alpha (P) \setminus \{\underline{t}\}\} \dagger P \end{aligned}$$

The dagger (\(\dagger \)) operator is a nominal substitution operator. It applies the given partial function, which maps variables to expressions, as a substitution to the given predicate, so that \(P[v/x] = \{x \mapsto v\} \dagger P\). We construct a substitution that maps every flat continuous variable (other than the distinguished time variable \(\underline{t} \in [ ti .. ti ')\)) to a corresponding variable lifted over the time domain. The effect of this is to state that the predicate holds for values of continuous variables at a particular instant \(\tau \), a variable that is potentially free in P. Each flat continuous variable \(\underline{x} : T\) is thus transformed to have a time-dependent function \(\underline{x} : \mathbb {R} \rightarrow T\) type. This operator is used to lift time predicates over intervals.

Healthiness conditions. We introduce two healthiness conditions:

where \(\begin{array}{l} \mathbb {R}_\mathsf {oseq}~\triangleq ~ \{x : seq \,\mathbb {R} ~|~ \forall n< \#{x} - 1 @ x_n < x_{n + 1}\} \\[1ex] f \mathop {\,\textsf {cont-on}\,}[m, n) ~\triangleq ~ \forall t \in [m, n) @ \underset{x \rightarrow t}{\lim }\, f(x) = f(t) \end{array}\) states that time may only ever go forward, as should be the case, and thus the time interval is well-defined. states that every continuous variable \(\underline{v}\) should be piecewise continuous, that is, that for non-empty intervals there exists a finite number of points (range of I) between \( ti \) and \( ti '\) where discontinuities occur. We define the set of totally ordered sequences \(\mathbb {R}_\mathsf {oseq}\) that captures this set of discontinuities, and the continuity of f is defined in the usual way by requiring that at each point in \([ ti , ti ')\), the limit correctly predicts where the function goes.

and are idempotent, monotone, and commutative as they are both conjunctive. We then have that also satisfies all these properties. Furthermore it defines a complete lattice.

Theorem 1

predicates form a complete lattice under and \(\bigsqcup \), with and .

Proof

By conjunctivity of . Properties of conjunctive healthiness conditions are proved in [12]. \(\square \)

Table 1. Signature of hybrid relational calculus
Full size table

6 Hybrid Relational Calculus

The signature of our theory is given in Table 1. It consists of the standard operators of the alphabetised relational calculus together with operators to specify intervals \(\left\lceil \left\lceil P \right\rceil \right\rceil \), differential algebraic equations , and preemption \(P \left[ \, b \, \right] Q\). Using this calculus, we can describe the bouncing ball example from Fig. 2:

Example 1

Bouncing ball in hybrid relational calculus

This hybrid program has two continuous variables for height \(\underline{h}\) and velocity \(\underline{v}\). Initially we set these two variables to 1 and 0, and then initiate the system of ODEs. The system evolves until \(\underline{h} < 0\), at which point a discrete command is executed that assigns \(-v \cdot 0.8\) to v, that is, the velocity is reversed with a dampening factor. The system infinitely iterates, allowing the system dynamics to continue evolving, but with new initial values. Such a system only requires an ODE with no algebraic equations; to illustrate DAEs we give another example.

Example 2

Cartesian pendulum in hybrid relational calculus

This system consists of four differential and one algebraic equation in terms of the position (x, y), horizontal and vertical velocities u and v, and the length l of the pendulum cable. The differential equations describe the horizontal and vertical components of the pendulum’s movement vector, governed by the laws of conservation of energy and gravity using a constant \(\lambda \) previously defined. The algebraic equation ties x and y together through the Pythagorean theorem, ensuring that the length of the cable must be respected by the movement. \(\square \)

We note that many of the standard operators of the alphabetised relational calculus retain their standard denotational semantics [18] in this setting, but over the expanded alphabet. Indeed, an alphabetised relation is simply a hybrid relation with the degenerate alphabet \(\mathrm {con}\alpha (P) = \emptyset \). For continuous variables, sequential composition behaves like conjunction. In particular, if we have , with P and Q representing evolutions over disjoint intervals, then their sequential composition combines the corresponding trajectories when they agree on variable valuations. Put another way, the final condition of P also defines the initial condition for Q as in the Z schema composition operator.

Similarly, other operators like the Kleene star and Omega iteration operators \(P^{\star }\) and \(P^{\omega }\), being defined solely in terms of sequential composition, disjunction (internal choice), , and fixed point operators, also remain valid in this context. Thus we already have the core operators of an imperative programming language at our disposal. We prove that these core operators satisfy our two healthiness conditions in Isabelle (cf. Sect. 7), but for now we state the following theorem.

Theorem 2

The following operators of relational calculus , , \(P^{\star }\), , \(x := v\), and are closed.

The maximally nondeterministic relation is of course not healthy, and so we supplement our theory with . We define the interval operator from \(\mathcal {DC}\)  [33] and our own variant.

Definition 2

Interval operators

\(\left\lceil P \right\rceil \) is a continuous specification statement that P holds at every instant over all non-empty right-open intervals from \( ti \) to \( ti '\); it corresponds to the standard \(\mathcal {DC}\) operator. We apply to ensure that all variables are also piecewise continuous. In this setting we can use sequential composition to express the \(\mathcal {DC}\) chop operator (\(P \circ Q\)) to decompose an interval. Our additional interval operator \(\left\lceil \left\lceil P \right\rceil \right\rceil \) pairs continuous variables with discrete variables at the start and limit of the interval, whilst holding other discrete variables constant. The initial condition of each continuous variable \(\underline{x}\) in the interval is constrained by the valuation of the corresponding discrete copy x. Likewise, the condition at the limit of the interval is recorded in the corresponding discrete after variable \(x'\).

Crucially, this provides a uniform view of discrete and continuous variables when handled over an interval, and allows the use of standard relational operators for their manipulation. Moreover, by taking the limit rather than the final value of a continuous variable we do not constrain the trajectory valuation at \( ti '\) meaning it can be defined by a suitable discontinuous discrete assignment at this instant. Following [14] we ground our definition of differential equation systems in this interval operator. This will, for example, allow us to formally refine a DAE, under given initial conditions, to a suitable solution expressed using the interval operator. Intervals satisfy a number of standard laws of \(\mathcal {DC}\) illustrated in Table 2, which we prove in Sect. 7.

Table 2. Algebraic laws of durations
Full size table

We next introduce an operator, adapted from \(\mathcal {HCSP}\)  [21, 34], to describe the evolution of a system of differential-algebraic equations.

Definition 3

DAE system in semi-explicit form

figure a

A DAE consists of a set of n functions \(f_i : \mathbb {R} \times \mathbb {R}^n \times \mathbb {R}^m \rightarrow \mathbb {R}\) each of which defines the derivative of variable \(\underline{v}_i\) in terms of the independent time variable \(\underline{t}\) and \(n+m\) dependent variables. It also contains algebraic constraints \(b_j : \mathbb {R} \times \mathbb {R}^n \times \mathbb {R}^m \rightarrow \mathbb {R}\) that must be invariant for any solution and do not refer to derivatives. For \(m=0\) the DAE corresponds to an ODE, which we write as \(\left\langle \, F_n \, \right\rangle \). The DAE operator is defined using the interval operator to be all non-empty intervals over which a solution satisfying both the ODEs and algebraic constraint exists. Non-emptiness is important as it means that a DAE must make progress: it cannot simply take zero time since \(\ell > 0\), and so a DAE cannot directly cause “chattering Zeno” effects when placed in the context of a loop, though normal Zeno effects remain a possibility.

As previously explained, at the initial time (\( ti \)) each continuous variable \(\underline{v}_i\) of the system is equated to the value of the corresponding discrete input variable \(v_i\). To obtain a well defined problem description, we require the following conditions to hold [2]: (i) the system of equations is consistent and neither underdetermined nor overdetermined; (ii) the discrete input variables \(v_i\) provide consistent initial conditions (ICsFootnote 5); (iii) the equations are specific enough to define a unique solution during the interval \(\ell \). The system is then allowed to evolve from this point in the interval between \( ti \) and \( ti '\) according to the DAEs. At the end of the interval, the corresponding output discrete variables are assigned. During the evolution all discrete variables and unconstrained continuous variables are held constant.

Finally, we define the preemption operator, adapted from \(\mathcal {HCSP}\).

Definition 4

Preemption operator

Intuitively, P is a continuous process that evolves until the predicate B is satisfied, at which point Q is activated. This operator is used to capture events in Modelica. The semantics is defined as a disjunction of two predicates. The first predicate states that, if B holds in the initial state of \( ti \), then Q is activated immediately. Otherwise, P is activated and can evolve while B remains false (potentially indefinitely). The second predicate states that \(\lnot B\) holds on the interval \([ ti , ti ')\) until instant \( ti '\), when B switches to a true valuation; during that inverval P is executing. Following this, P is terminated and Q is activated.

7 Mechanisation in Isabelle/UTP

Our Isabelle [23] mechanisation serves two purposes: firstly it validates the model by enabling us to prove algebraic laws, and secondly it enables theorem proving for hybrid programs. It is based in a shallow embedding of the UTPFootnote 6, which provides direct proof automation through a combination of Isabelle/Circus  [5] and our own deep model [10]. UTP relations are represented by predicates over bindings, and bindings over a given alphabet are represented using record types, where each field corresponds to a variable. The model is based on a UTP expression type ranging over alphabet type and with return type . Alphabetised predicates are expressions with a boolean return type, and relations are predicates over a product type .

We mimic the syntax of UTP predicates as given in most standard publications (e.g. [4, 18]). Where this is not possible, we supplement the same syntax with an added subscript u. For example, equality in Isabelle “\(=\)” denotes HOL equality, so we use \(=_u\) for UTP equality. Input variable and output variable expressions are written and respectively. We also make use of Isabelle’s implementation of Cauchy real numbers and analysis [7, 11]. Our proofs make heavy use of Isabelle’s automated proof facilities like auto and sledgehammer [3]. This has allowed us to use Isabelle to validate the healthiness conditions and definitions given in the previous sections. We prove that they respect appropriate laws, which increases confidence in the correctness of our UTP theory. This section has been compiled using Isabelle’s document preparation system: all definitions and theorems have been mechanically verifiedFootnote 7.

figure b

A hybrid state represents the alphabet, or equivalently the state of the hybrid relation, at a particular instant. We represent this using a record with three fields: denoting the state variables, denoting the time, and denoting the trajectory of continuous variables. The record type is parametrised by the discrete portion of the alphabet, denoted by type and the continuous portion denoted by type . The state field’s type is a product of the discrete and continuous state, whilst the trajectory refers only to the continuous state. Intuitively, this encodes the distinction between discrete and continuous variables. A hybrid relation is then a homogeneous relation (hrelation) over the hybrid state. We next give the healthiness conditions of our theory.

figure c

is broadly the same as in Sect. 6, though we additionally require that the initial time be no less than zero; this is due to our use of the standard type that also encompasses negative numbers.

figure d

also explicitly requires that the trajectory sequence I is both sorted and distinct, which equates to it being linearly sorted as required.

figure e

We also have to add an auxiliary healthiness condition . This allows us to use standard HOL binary relations, where there is only inputs and outputs, to represent hybrid relations. Specifically, we have two copies of the trajectory, a before version and an after version and so this healthiness condition ensures the trajectory remains constant throughout. Monotonicity and idempotence of the healthiness conditions is proved by our automated relational calculus tactic. With our healthiness conditions defined, we can proceed to define the operators. The basic operators, such as and \(\mathop { @ }\) are elided here, and we instead focus on the continuous operators. We first define the two interval operators.

figure f

Definition corresponds to the interval operator \(\left\lceil P \right\rceil \), and has an almost identical definition. In our mechanisation, an interval can be written as \(\lceil P \rceil _H\) where is a predicate with the time variable \(\tau \) free.

figure g

Our modified interval operator \(\left\lceil \left\lceil P \right\rceil \right\rceil \), represented here by conjoins the standard interval operator with predicates that ensure that discrete variables remain const and that continuous variable copies match the initial value in the trajectory, and the left limit of the trajectory at the end. Here \(\pi _n\) is a function that returns the nth element of a product, represents function application, and \(lim _u(x \rightarrow t^-)\) denotes the left-limit. This interval operator is written \(\lceil |P|\rceil _H\), again with \(\tau \) free.

Next we define the operators for ODEs and DAEs. The first step is to formally mechanise the notion of time derivatives \((\dot{x})\). Thus we define a predicate hasDerivAt that relates ODEs to solution functions using the lifting package [19].

figure h

An explicit system of ODEs (’c ODE) is encoded as a function , where the real is the time parameter, and is a vector of real variables. We require that be within the type class of real vector spaces. Isabelle’s Multivariate Analysis library contains a function has-vector-derivative that relates a solution function \(\mathcal {F} : \mathbb {R} \rightarrow \mathbb {R}^n\) with its derivatives \(\dot{\mathcal {F}} : \mathbb {R}^n\) at instant \(\tau \) within a particular range. It represents the Fréchet derivative of differential equations in a vector space. We use this to define a construct where is a solution function, is the system of ODEs. This predicate is accompanied by a large number of rules that can be used to certify derivatives of polynomial functions. We now use these to encode operators for ODEs, DAEs, and ODEs under an initial condition.

figure i

We choose to implement ODEs and DAEs as separate constructs, as the definitions are simpler, though equivalent to those in the previous section. An ODE specifies that a solution function \(\mathcal {F}\) to the given ODE must exist and that at each point of the interval the values of all continuous variables () track this solution function. A DAE is then simply an ODE constrained with the algebraic predicate throughout the interval. We also provide a representation of ODEs as explicit initial value problems by where gives initial values to all continuous variables.

Finally, we prove some key laws about our hybrid relational calculus. Firstly we show that sequential composition is closed, which partly validates our healthiness conditions with respect to the standard relational calculus. This is proved by an apply-style Isabelle proof which is omitted.

figure j

In order to demonstrate the use of ODEs in this framework, we take the ODE from the bouncing ball example, and show how its solution can be expressed as a refinement statement.

figure k

As in Example 1, we specify the ODE with two variables, v and h that will give the velocity and height about the ground of the ball. We refine this in the window \(time = 0\) as it makes the solution simpler via an appropriate conjunction. Given initial conditions of \(v_0\) and \(h_0\) for the respective variables, solutions to the ODE equations are \(v_0 - g\cdot \tau \) and \((v_0\cdot \tau - g\cdot \tau ^2)/2 + h_0\), respectively. The solutions are proved correct in Isabelle automatically by application of our relational calculus tactic rel-tac, followed by existential introduction (exI) to introduce the ODE solution, application of the auto tactic, and then finally application of our own tactic vderiv-tac. This tactic recursively applies the set of introduction for differentiation in an effort to show that a given ODE is the derivative of a given solution. This example serves to demonstrate how a theorem prover can reason about differential equations in terms of their solution intervals making use of refinement and the Duration Calculus.

8 Modelica Semantics

In this section we give a semantics for flat Modelica whose models are given by a set of conditional differential, algebraic, and discrete equations. More specifically, we assume that a Modelica model consists of a set of dynamic variables x, algebraic variables y, and discrete variables q, and

  • a set of \(k \in \mathbb {N}_{>0}\) conditional DAEs, consisting of:

    • differential equations \(\dot{x} = \mathcal {F}_i(x, y, q)\) for \(i \in 1..k\);

    • algebraic equations \(y = \mathcal {B}_i(x, y, q)\) for \(i \in 1..k\);

    • boolean DAE guards \(\mathcal {G}_i(x, y, q)\) for \(i \in 1..k-1\), that give the conditions under which the corresponding set of differential and algebraic equations is active in terms of the values of discrete and continuous variables at initialisation or the previous event. We assume that at least one set of equations is active at any time;

  • a set of \(l \in \mathbb {N}\) boolean event conditions \(\mathcal {C}_i(x, y, q)\) for \(i \in 1..l\), that trigger an event when changing value. These must be specified in terms of the core Modelica relational operators, namely \(\le \), <, \(=\), and \(\ne \);

  • a set of \(m \in \mathbb {N}\) conditional discrete equation blocks, consisting of:

    • n boolean discrete-event guards \(\mathcal {H}_{i,j}(x, y, q, q_{pre })\) for \(i \in 1..m\), \(j \in 1..n\);

    • n discrete equations/algorithms \(\mathcal {P}_{i,j}(x, y, q, q_{pre })\) for \(i \in 1..m\), \(j \in 1..n\). We assume the discrete equations are sorted into a suitable sequence.

Each conditional DAE describes a possible continuous behaviour using a collection of differential and algebraic equations. The particular behaviour to be executed is chosen based on the evaluation of the guards, which take as input the valuations of the discrete and continuous variables at the (re)start of the continuous evolution. The possible events that can occur are described by a collection of boolean event conditions, which act as guards that can stop the continuous evolution. Once one or more of these guards changes value an event is fired, and possible discrete behaviour is executed. Usually such guards are implemented in terms of a zero crossing function, though our semantics specifies them abstractly. The appropriate discrete behaviours are then chosen through a collection of discrete event guards, and the resulting behaviour by an appropriate discrete equation that may be specified by a suitable algorithm.

Fig. 3.
figure 3

Overall semantics of a Modelica model \(\mathcal {M}\)

Full size image

We give the semantics for such a Modelica model \(\mathcal {M}\), which is shown in Fig. 3, in terms of four main definitions.

Init denotes the initialisation phase of a Modelica model, where initial values are assigned to the discrete and continuous variables. For now, we assume that initial values u, v, and w can be unambiguously assigned to each. Following initialisation, an infinite loop is entered representing the main body of behaviour.

DAE denotes the conditional system of differential and algebraic equations active during the continuous evolution of the model. It is represented by a conditional predicate that selects an appropriate set of differential and algebraic equations based on initial values of discrete and continuous variables.

Events denotes the event preemption condition, and is a disjunction of all possible event conditions (“relations” in Modelica terminology) in the Modelica model. In this way, the DAE remains active until one of the event conditions changes from its initial value, at which point it is preempted.

Finally, Discr describes possible discrete behaviour to be executed during event iteration; a finite event loop adapted from the pseudo code given on page 263 of [22]. The initial value of all discrete variables is first copied by creation of a local variable \(q_{pre }\) that holds the initial value of q. Each conditional discrete equation is then evaluated, which may lead to updates to q, and then the procedure iterates. The event iteration terminates when no more updates to q are made: a fixed point is reached. In Modelica the existence of a fixed point is not guaranteed and event iteration can potentially lead to an infinite loop.

To illustrate, we use the bouncing ball Modelica example from Fig. 2. It has continuous variables representing the height of the ball above the ground h and the velocity of the ball v. For giving a semantics to this we convert the expression to an expression, so we need only consider semantics of the latter, using the conceptual mapping in Sect. 8.3.5.1 of [22], which will yield:

figure l

An additional variable of type Boolean is added, and assigned the condition of the statement. The equation itself is replaced by an equation whose condition is that c is true now, and was not true previously – i.e. it has become true at the current instant. We can now give the semantics of this model.

Example 3

Bouncing ball semantics in hybrid relational calculus

We assign initial values for the three variables, and assume that the condition c is false initially. The DAE is then activated and evolves until the valuation of the guard \(h < 0\) at time t is different from the initial value, that is \((\underline{h}< 0) \ne (h < 0)\). We note that \(\underline{h}\) and h are two different variables: \(\underline{h}\) denotes h at time t, whilst h denotes its value at the beginning of the present DAE evolution, so the inequality corresponds to the value of this boolean guard changing. At this point, the event iteration begins. We create a variable to denote the previous value of c, and then enter into the event loop. We then assign c to \(c_{pre }\), and evaluate the discrete equations. First of all, we evaluate the new value of c, which is the event condition. Secondly, if c is true and different from its previous value, we also update v, otherwise we skip. The loop terminates once the value of c has stablised (which it has in the second iteration). Following this, we iterate the whole loop and restart the DAE with the new initial values.

This example serves to illustrate the behaviour of a Modelica model in the hybrid relational calculus. Our preliminary semantics considers a fragment of the event handling mechanism, excluding practical problems of initialization and numerical integration of DAEs. Present limitations include the separation of continuous and discrete equations during the event handling mechanism. More complete Modelica semantics require to solve a mixed system of the discrete and continuous equations during events. We will consider these in future iterations of this semantics, define a more complete translation, and apply it to more substantive examples.

9 Conclusions

We have presented a denotational semantics for the dynamical systems modelling language Modelica, in terms of a hybrid relational calculus that has been mechanised in Isabelle. The semantics elaborates the event iteration system, showing how continuous evolution transitions to discrete behaviour and vice-versa. Nevertheless, our translation is currently relatively informal and thus in future work we will define a comprehensive mapping from Modelica to hybrid relations, including its expression language and collection of imperative language constructs. We will also combine our theory of hybrid relations with timed reactive designs [13] to provide a rich semantic model providing termination, stability, and concurrency in the form of CSP.

This work supports the goals of a large EU project called INTO-CPSFootnote 8, which aims at building an integrated tool-chain for model based development of Cyber-Physical Systems. This tool-chain will support the integration of heterogeneous discrete and continuous system models through the Functional Mockup Interface [8] (FMI), a language that allows the composition of continuous time and discrete event models, and their concurrent simulation to support empirical evaluation. We will use our UTP theory of hybrid relations combined with timed reactive designs to develop a common semantic domain into which all these language can be mapped and verified.

We also plan to further experiment with theorem proving in Isabelle, for example through a mechanisation of Hybrid Hoare Logic [37]. As stated in Sect. 8, Modelica does not guarantee that event iteration terminates and so we could use such a prover, in the context of reactive designs, to verify termination.