Computing and Software Science pp 452477  Cite as
ContinuousTime Models for System Design and Analysis
Abstract
We illustrate the ingredients of the stateoftheart of modelbased approach for the formal design and verification of cyberphysical systems. To capture the interaction between a discrete controller and its continuously evolving environment, we use the formal models of timed and hybrid automata. We explain the steps of modeling and verification in the tools Uppaal and SpaceEx using a case study based on a dualchamber implantable pacemaker monitoring a human heart. We show how to design a model as a composition of components, how to construct models at varying levels of detail, how to establish that one model is an abstraction of another, how to specify correctness requirements using temporal logic, and how to verify that a model satisfies a logical requirement.
1 Introduction
A cyberphysical system consists of computing devices communicating with one another and interacting with the physical world via sensors and actuators. Increasingly, such systems are everywhere, from smart buildings to medical devices to autonomous cars. Modelbased design offers a promising approach for assisting developers to build cyberphysical systems in a systematic manner [2, 18, 26]. In this methodology, a designer first constructs a model, with mathematically precise semantics, of the system under design, and performs extensive analysis with respect to correctness requirements before generating the implementation from the model.
Models of cyberphysical systems need to capture both the controller—the system under design, and the plant—the environment with continuously evolving physical activities in which the system operates. This typically means a combination of block diagrams, state machines, and differential equations. Furthermore, we need to define models formally, that is, in a mathematically precise manner. The formal semantics allows us to answer questions such as, “what are the possible behaviors of a component” and “what does it mean to compose two components” rigorously, and forms the basis for analysis tools. In this article we do not attempt a survey of the rich literature on formal models and analysis tools for cyberphysical systems, but aim to give an introduction to the subject using a case study (see [13] for some recent surveys).
Medical devices offer an ideal testbed for exploring the applications of formal methods in system design due to their safetycritical nature, which demands higher levels of reliability and rapidly growing complexity due to increased autonomous operation [27]. We use a dual chamber implantable pacemaker to illustrate the process of model construction and verification [10, 22, 28, 30]. The first step in modeling is to choose a modeling formalism depending on what aspects of the system a designer wants to focus on. The control algorithm of the pacemaker is best modeled as a composition of timed automata [5], while the relevant features of the heart can be described as a network of hybrid automata [4]. We introduce these two formal models using the modeling tools Uppaal [8, 25] and SpaceEx [17], respectively.
To check that the design works correctly as intended, the designer first needs to express the requirements capturing correctness in a mathematically precise manner. We explain two common ways of formalizing requirements using the pacemaker case study. The automatabased approach corresponds to designing a monitor that observes the input/output behavior of the system and enters an error state if an undesirable pattern is detected [29]. The temporallogicbased approach corresponds to writing down a formula in a specialized formal logic—TCTL (Timed Computation Tree Logic) in our case [3], which captures the desired correctness requirement. A model checker is then tasked with the job of automatically checking that the system model satisfies the requirement, and produce feedback in the form of a counterexample if this is not the case [12]. Model checkers for continuoustime systems need to symbolically explore the infinitely many reachable states of the model. While symbolic algorithms have been developed for both timed and hybrid automata, the existing technology is more scalable for timed automata [7]. Hence, we construct a timedautomatonbased model of the heart by suppressing many details of the hybrid model, and show how the model checker Uppaal can then be used to verify requirements of the pacemaker.
Since we created a simplified heart model for the purpose of verifying requirements of the pacemaker, we are faced with a new analysis problem, namely, establishing a rigorous relationship between the two versions of the heart models. Showing that one model is a refinement or abstraction of another model is another key step in modelbased design, and is essential if we want to infer properties of the more complex model based on the analysis of the simpler one [6, 11].
Related Work. In this paper, we use a dual chamber implantable pacemaker to illustrate the modeling of control software and the physical world it interacts with. Analyzing the behavior of the heart using formal methods was first proposed in [30], and our modeling of a heart cell is based on the HH model with linear differential equations from that paper. The modeling and model checking of the control algorithm within a pacemaker first appears in [22], and we use the pacemaker model as well as abstracted heart model from that paper for our case study. Note that there has been considerable research on formal modeling and verification of the pacemaker. For instance, [10] develops a more precise Simulink model of the heart cell from [30] with nonlinear differential equations, and [28] describes a translator from Uppaal to Simulink/StateFlow for this purpose.
Organization of the Paper. We begin with an overview of the heart and pacemaker models in Sect. 2. Then, in Sect. 3, we use SpaceEx to construct an abstraction of the heart, and, in Sect. 4, we use Uppaal to verify the whole heartpacemaker system. We conclude with future challenges in Sect. 5.
2 The Pacemaker Case Study
The human heart is an excellent example of a naturally occurring timed system. It spontaneously generates electrical impulses that organize the sequence of muscle contractions during each heart beat. The underlying timing pattern of these impulses is key to the proper functioning of the heart. The implantable cardiac pacemaker is a rhythm management device that monitors these patterns and corrects them via external means when needed.
Controlled by the nervous system, a specialized tissue, called the sinoatrial node, at the top of the right atrium periodically generates electrical pulses. These pulses cause both atria to contract, forcing blood into the ventricles. The electrical conduction gets delayed at the atrioventricular node, allowing the ventricles to fill fully, but then spreads rapidly across the ventricular muscles, resulting in their coordinated contraction, which pumps the blood out of the heart.
A common heart disease, called bradycardia, is due to failures in either impulse generation or impulse propagation and results in slow heart rate, leading to insufficient pumping of blood. Bradycardia can be treated by an implantable pacemaker that monitors the heart rate and delivers timely external electrical pulses to maintain an appropriate heart rate as well as atrioventricular coordination. Such a pacemaker usually has two leads fixed on the wall of the right atrium and the right ventricle. Activation of local tissue is sensed by these leads, and these sensing events act as inputs to the pacemaker. If these sensed events do not occur in a timely manner, then the pacemaker responds by producing pacing events that trigger electrical stimuli to the heart.
A modern pacemaker responds to a variety of heart conditions and can operate in different modes. We focus on two modes DDD and VDI and switching between them. In the mode DDD, the pacemaker is pacing both the atrium and the ventricle, both chambers are being sensed, and the pacemaker software responds to sensing by both activating and inhibiting further pacing, while in the mode VDI, the pacemaker paces only the ventricle, senses both chambers, and sensing causes inhibition of pacing.
2.1 Hybrid Automata: Modeling the Heart
To analyze the functionality of the pacemaker at design time, we need a model that captures how a human heart generates the sensory events. We can view the heart tissue as a network of cardiac cells, where the electric wave propagates along neighbouring cells assuring coordinated contraction. At the cellular level, the electrical signal is a change in the potential across the cell membrane, and is caused by the flow of ions, such as sodium and potassium, between the inside and outside of the cell. Mathematical modeling of the ionic processes corresponding to cell excitation has been studied extensively in computational systems biology. Typically, such a model is described using nonlinear differential equations, and consists of multiple continuous state variables corresponding to quantities such as voltage and ion concentrations and a large number of parameters.
A first step in modeling is to decide what level of detail is appropriate for the analysis task. For the purpose of this case study, we use the model proposed by [30], which is derived from the wellaccepted HodgkinHuxley (HH) model of cell excitation. It is based on the observation that change in voltage with time that describes the cell excitation upon stimulation can be clearly separated in distinct phases, namely, upstroke, repolarization and resting, such that in each phase the dynamics can be captured by linear differential equations. This behavior can then be described using hybrid automata.
The model of the whole heart consists of a composition of cells, which synchronize according to their output and input stimuli. Figure 4 shows such an example. The cells are organized in a linear fashion, where the labels out1 and out0 of a cell synchronize with the input labels in1 and in0 of the next cell. At the top of the network, we have the sinoatrial (SA) node, which is the cell that takes through in1 and in0 the input stimulus of the heart, which can come from its natural pacing or from the actuator of the pacemaker. The output labels out1 and out0 of the SA node then trigger the input labels of a second cell. The output of the second cell triggers the input of a third, and so on, creating a chain of stimuli. The whole chain can be seen as divided in two main groups, namely atrium and ventricle. The output of the cell at the boundary of the atrium then produces the output of the whole atrium, which is connected to the cell at the top of the ventricle, which is called atrioventricular (AV) node. The AV node may take the pacing coming from the atrium or from the second actuator of the pacemaker.
Hybrid automata can be classified according to the generality of their guards, differential equations, and difference equations. The more restrictive these equations are, the more feasible the analysis of the resulting behaviors. Assume that x is a state vector. A hybrid automaton has piecewise affine dynamics if all mode invariants and transition guards have the form \(x \in U\), all mode equations have the form \(\dot{x} = Ax + v\) with \(v \in V\), and all transition equations have the form \(x' = Bx + w\) with \(w \in W\), for matrices A and B, and polyhedra U, V, and W. The hybrid automaton has piecewise constant dynamics if \(A=0\). It is a timed automaton if \(A=0\) and \(V=1\). In a timed automaton, all state components always advance at the rate of time; they represent “clocks”.
2.2 Timed Automata: Modeling the Pacemaker
To first informally explain the formalism of timed automata and how they are modelled in the tool Uppaal, we will use the Open image in new window process shown in Fig. 7. Uppaal timed automaton consists of locations and edges modeling its discrete states and discrete transitions respectively. Locations and edges have labels. For example, process Open image in new window has an initial location with a circle O inscribed, which has a name label Open image in new window . The location Open image in new window has an invariant label Open image in new window meaning that the automaton may stay in Open image in new window only while the clock Open image in new window value is less or equal to the value of the Open image in new window constant. Process Open image in new window may stay in location Open image in new window for arbitrary amount of time because there is no invariant forcing it to move, it also listens for synchronizations over channels Open image in new window and Open image in new window . The reception over channel Open image in new window transitions it to Open image in new window , while the reception over Open image in new window switches it directly to location Open image in new window and reset the clock Open image in new window . The location Open image in new window has C inscribed to denote that it is committed and the automaton’s progress cannot be interrupted neither by the time delay nor any other process, therefore it has to move immediately by taking an edge transition to location Open image in new window which is labeled with synchronization Open image in new window and update Open image in new window meaning that it emits a message on channel Open image in new window and resets the clock Open image in new window so the time is counted from zero in location Open image in new window up to the bound of Open image in new window . Then process Open image in new window may move from location Open image in new window back to Open image in new window but only when the guard Open image in new window is satisfied, i.e. only after spending at least the amount Open image in new window of time in location Open image in new window . As a result, the state of a timed automaton consists of its location and variable values, and there are two kinds of transitions between states: delay (when clock values increase while satisfying the current invariant) and edgetransitions when clock values satisfy the guards, synchronize, update the value and satisfy the target location invariant.
 Integer variables.

Apart from constants, most programming and modeling languages use variable value manipulations. Likewise Uppaal allows bounded integer variables to be used and combined with clock constraints. On one hand, the value of an integer variable becomes an integral part of the state of the system. On the other hand, the integer variable value can be used as a constant in clock constraints because the integer variable value may change only upon edgetransitions between the timed automata states. An example of such integer use is demonstrated by Open image in new window in Fig. 8d, where the bound Open image in new window is changed by transition from Open image in new window to Open image in new window . Interestingly, the bounded integer variables do not increase the theoretical expressiveness of timed automata, therefore all theoretical results still apply. For example, we have compressed the representation of Open image in new window and Open image in new window in Fig. 8g and f by encoding the Open image in new window and Open image in new window counting into local integer variables Open image in new window (originally [22] enumerated into a number of distinct locations).
 Inputoutput synchronization.

In contrast to nondirected multilabel synchronizations in SpaceEx hybrid automata, the synchronizations between Uppaal processes are directed in the sense that one process is sending with exclamation mark (e.g. Open image in new window ) and the receiving process is listening with question mark ( Open image in new window respectively). By default, channel synchronizations are handshake, meaning that both sender and receiver must mutually agree for the transition to take place. Handshake synchronizations happen only in pairs of processes, i.e. only two processes may participate in the synchronization at a time, and all possible pairs are considered nondeterministically when multiple receivers are available.
 Broadcast synchronization.

In addition Uppaal supports broadcast synchronization where one sender may synchronize with multiple receivers. In contrast to handshake synchronization, the broadcast synchronization is nonblocking in a sense that the sender is not required to wait for any receivers and only the ready receivers participate in the synchronization. While the broadcast synchronization can be emulated by adding receiving selfloops in locations where the process does not implement the reception part, but in practice it is more succinct way of modeling, allows partial order reduction and verification is more efficient as the tool does not need to consider the extra edges. All the synchronizations in the pacemaker study use broadcast channels because nonblocking behavior is closer to how the independent processes communicate and it is easier to include additional processes without modifying the original behavior, which is useful in adding extra monitors for diagnostics and verification.
 Urgency.

Sometimes the modeled process needs to execute several transitions without delaying in the locations between. We call such locations urgent and draw a letter U inside to mark that time cannot progress in them.
 Atomicity.

The process in urgent location may still be interrupted by a transition in another process even though the time is not allowed to pass. Uppaal implements a committed location with C inscribed in case an uninterrupted (“atomic”) sequence of transitions is needed. Committed locations are useful in connecting multiple channel synchronizations at the same time which would be very cumbersome to model otherwise.
We have reconstructed the pacemaker model from [22] shown in Fig. 8. The overview block diagram of the processes is shown in Fig. 6 where the heart is represented by SA Node cell, two atrium and two ventricle cells. The cells can be stimulated by Open image in new window and Open image in new window channels synchronizations denoting the start and ending of the stimulus. The heart can be selfstimulating by a SA Node cell or by a pacemaker by a signal over channel Open image in new window (Atrium Pulse). Normally the atrium cells relay the signal to ventricle cells, but if the stimulus is too weak (or too short), then the ventricle is stimulated by the pacemaker over Open image in new window (Ventricle Pulse) channel. The pacemaker monitors the activity of the atrium and ventricle by receiving from the signals over the corresponding channels Open image in new window and Open image in new window . All channels used in Fig. 8 are of broadcast type, meaning that one sending event can be sensed by zero or more receivers at once and the sending process is not blocked by the absence of receivers.
Atrioventricular Interval ( Open image in new window , Fig. 8c) maintains the maximum interval between the atrium and ventricle activation by issuing ventricle pacing Open image in new window if no ventricular event received Open image in new window within Open image in new window time after the last atrial event ( Open image in new window or Open image in new window ). The interval is measured by the clock Open image in new window shared with Upper Rate Interval ( Open image in new window , Fig. 8b) which prevents pacing the ventricle too fast by resetting Open image in new window upon ventricular event ( Open image in new window or Open image in new window ).
Postventricular Atrial Refractory Period ( Open image in new window , Fig. 8d) converts atrium events Open image in new window and Open image in new window into sensed event Open image in new window and filters the sensed noise during the blanking period ( Open image in new window ) after the ventricular event followed by a refractory period ( Open image in new window ). The blocked events are converted to Open image in new window and Open image in new window for advanced diagnostics.
Ventricular Refractory Period ( Open image in new window , Fig. 7) similarly translates the ventricle peak events over Open image in new window into sensed events over Open image in new window and filters out by not retransmitting for a time interval Open image in new window after the last event.
We use the same set of constants as in the original publication [22]: Open image in new window .
3 Relating and Combining Models
Hybrid automata can be numerically simulated, or formally analyzed. While simulation generates one behavior at a time, formal analysis can answer questions about all possible behaviors of a hybrid automaton. The most basic behavioral analysis question about a hybrid automaton is the reachability question. The bounded reachability question asks, given two state sets S and T, and a time bound t, if there is a behavior from a state in S to a state in T of total duration no more than t. The unbounded reachability question asks, given two sets S and T, if there is a behavior of any duration from a state in S to a state in T. In general, both the bounded and unbounded reachability questions are formally undecidable even for hybrid automata with piecewise constant dynamics [21]. However, methods and tools have been developed for solving many interesting instances of these problems [17, 20]. Moreover, both questions can always be answered algorithmically for the special case of timed automata [5].
Unfortunately, the heartpacemaker model is not a timed automaton, as heart cells fall in the class of hybrid automata with piecewise affine dynamics, and so does their composition with the pacemaker. On the other hand, if each cell model was a timed automaton, the whole system would be a timed automaton, and therefore the verification answer solvable. Can we model each cell with timed automata, so that by verifying the resulting system we verify the original system too? To this aim, we exploit the notion of abstraction: if the timed automaton abstracts the original cell model, then any negative answer for the reachability question in the abstract composed system implies the same negative answer in the original composed system. In the following, we construct such a timed automaton, we explain its relation with the original hybrid automaton, and we demonstrate how to use SpaceEx to mechanically prove that the former abstracts the latter.
3.1 A Timed Abstraction of the Heart Cell Model
The abstraction has been constructed manually, by making the following observations about the original model in Fig. 2. Initially the cell is in resting mode, where \(v_x  v_y\) drops towards 0, therefore the invariant \(0 \le v_x  v_y \le V_T\) is always satisfied. In mode resting the events in1 and in0 can occur at any time, where in0 is ignored and in1 switches to stimulus. In stimulus the automaton is also driven by the difference \(v_x  v_y\) which may increase and force automaton to move to upstroke. The time bound \(T_{out1}\) models the largest time where \(v_x  v_y\) hits \(V_T\) and satisfies the guard for out1, i.e., \(v_x  v_y \ge V_T\). The symbol out1 may occur any time before \(T_{out1}\), as well as in1 and in0 which may happen as long as the invariant \(0 \le v_x  v_y \le V_T\) of stimulus is satisfied. Upon the occurrence of out1 the value of \(v_x  v_y\) is exactly \(V_T\), the process switches to upstroke in which it stays until the value of \(v_x  v_y\) hits exactly \(V_O\), whose time is modeled by \(V_O\). Similarly, upon get the process switches to repolarization and stays until it takes out0 when \(v_x  v_y\) hits \(V_R\), which must happen no later than \(T_{out0}\) time.
Whether the timed automaton in Fig. 9 is an abstraction of the heart cell model in Fig. 2 requires us to first rigorously define what we mean by abstraction, namely, what are the features of the original system that are to be conserved by the abstract system. Second, we need to instantiate the parameters \(T_{out0}\), \(T_{out1}\), and \(T_{get}\) and prove that the so obtained timed automaton abstracts the original hybrid automaton. We discuss these points in Sects. 3.2 and 3.3. For the time being, the construction of the timed abstraction relies on the intuition and the expertise of the designer. In this phase, the only formal requirement is that the timed automaton needs to deterministic, so that in the next phase we can construct its complement. A timed automaton is deterministic if at every mode every pair of transitions with common symbol have disjoint guards [5]. The timed abstraction of Fig. 9 is deterministic simply because at every mode each symbol has at most one switch.
3.2 The Timed Language of Hybrid Automata
A hybrid automaton A abstracts a hybrid automaton B when all observable behaviors of the latter are also observable behaviors of the former. The observable behaviors are the features of the system dynamics that we need to observe in order to decide whether a specification is satisfied. The more detailed the observable behaviors, the harder is constructing an abstraction, but the more sophisticated are the properties that we can verify. For verifying properties such as Tachycardia, Bradycardia, and so on, we want to observe sequences of labels \(\sigma = \sigma _0\sigma _1\dots \) with the exact times \(\tau = \tau _0\tau _1\dots \) at which each of these events has occurred. Each of such pairs of sequences \((\sigma , \tau )\) is called a timed word. For instance, the word that repeats the pattern \(\mathtt{in1},\mathtt{out1},\mathtt{get},\mathtt{out0}\) is a timed word when coupled with the times of staying respectively in modes resting, stimulus, upstroke, and repolarization, repeatedly. The set of all the timed words of the hybrid automaton H is called its timed language \(\mathcal {L}_H\).
The timed abstraction A is deterministic. To complement a deterministic timed automaton we need first to add dummy transitions so to make the automaton accept any timed word (on the same alphabet \(\varSigma = \{ \mathtt{in0}, \mathtt{in1}, \mathtt{out0}, \mathtt{out1}, \mathtt{get}\}\)), yet remaining deterministic. Figure 10 shows the result. From mode resting only in1 and in0 can be received, therefore we add a dummy transition, i.e., a transition to a dummy mode, which receives any other symbol, i.e., out1, out0, and get. From stimulus, in1, in0, and out1 can be received and can be received as long as \(t \le T_{out1}\), therefore we add a dummy transition with guard \(t > T_{out1}\) that receives such events, so as to ensure all guards of transitions with common symbol to be disjoint and maintain the automaton deterministic. The symbols out0 and get cannot be received at all from stimulus, therefore we add a dummy transition with unconstrained guard. Similarly, we make the same construction on modes upstroke and repolarization. Finally, one can observe that every trajectory that ends in any dummy mode corresponds to a timed word that is not in \(\mathcal {L}_A\). The dummy modes are those that recognise the complement language, thus we mark them as rejecting modes.
In summary, we formulate the question of whether the timed abstraction in Fig. 9 abstracts the heart cell model in Fig. 2 by asking SpaceEx whether the composition of the heart cell model in Fig. 2 with the complement automaton in Fig. 10 can reach any of the rejecting modes. The result is a reachability question on hybrid automata with affine dynamics.
3.3 Verifying the Abstraction Using SpaceEx
SpaceEx is a modeling framework for the composition of hybrid automata that collects several reachability analysis techniques, which are called scenarios. We can divide the currently available scenarios in three main categories: simulation based, support function based, and the polyhedra based scenarios. The simulation based scenario generates timebounded sample trajectories, and can be used to reject an abstraction, but not to verify one. The support function and the polyhedra based scenarios perform reachability analysis by generating sequences of polyhedra that overapproximate the whole space of reachable states and both are possibly suitable for verifying an abstraction. In fact, when they answer that all rejecting modes are unreachable, then the rejecting modes are actually unreachable, and the abstraction is proven. The converse is not necessarily true and, moreover, termination is not guaranteed either. For this reason, successfully concluding an abstraction proof requires several trial and error attempts in tuning the parameters and the multiple heuristic options of SpaceEx.
We use the polyhedral based scenario which is also know as the PHAVer scenario. The PHAVer scenario overapproximates the continuous flow of every mode by piecewise constant differential inclusions [16]. In other words, it turns affine dynamics of the form \(\dot{x} = Ax + v\) with \(v \in V\) into differential inclusions of the form \(\dot{x} \in U\), where U is a set the contains all values that the derivative \(\dot{x}\) can possibly take. Both such transformation and the symbolic reachability analysis on the so obtained hybrid automaton are then done by quantifier elimination, e.g., by the Fourier Motzkin algorithm [4].
The heart cell model parameters [30].
\(a_x\)  \(a_y\)  \(b_y\)  \(c_x\)  \(c_y\)  \(d_x\)  \(d_y\)  \(V_R\)  \(V_T\)  \(V_O\) 

−0.98  −0.16  −0.16  15  1.4  −0.98  −0.16  10  10  83 
\(i_{st}\)  \(T_{out1}\)  \(T_{out0}\)  \(T_{get}\)  Answer  \(i_{st}\)  \(T_{out1}\)  \(T_{get}\)  \(T_{out0}\)  Answer 

10  1  1  1  \(\{r_3\}\)  1  1  0.5  7.5  \(\{r_1\}\) 
10  1  1  10  \(\emptyset \)  1  10  0.5  7.5  \(\emptyset \) 
10  0.1  0.1  1  \(\{r_1\), \(r_2\), \(r_3\}\)  100  10  0.5  7.5  \(\emptyset \) 
10  1  0.5  10  \(\emptyset \)  100  0.01  0.5  7.5  \(\{r_1\}\) 
10  1  0.5  7.5  \(\emptyset \)  100  0.1  0.5  7.5  \(\emptyset \) 
3.4 Abstraction Refinement
\(a_x\)  \(a_y\)  \(b_y\)  \(c_x\)  \(c_y\)  \(d_x\)  \(d_y\)  \(V_R\)  \(V_T\)  \(V_O\)  \(V_{max}\)  \(i_st\)  \(T_{out1}\)  \(T_{get}\)  \(T_{out0}\)  \(T_{stim}\) 

−0.98  −0.16  −0.16  15  1.4  −0.98  −0.16  10  10  83  \(\infty \)  10  1  0.5  7.5  0 
−0.98  −0.16  −0.16  15  1.4  −0.98  −0.16  5  10  83  100  10  1  0.5  7.5  0.86 
−0.98  −0.16  −0.16  15  1.4  −0.83  −0.16  5  10  83  100  10  1  0.5  19  1.001 
In summary, we construct a sequence of time abstractions for a heart cell and formally proved that they indeed abstract its timed language. The abstraction question turns out to be a reachability question on a heart cell composed with the complement of its timed abstraction, which is a rather small system. We employ SpaceEx on this problem, and then we modify the heartpacemaker model by replacing each cell with the abstraction. The whole model is now a timed automaton, which can be verified by Uppaal.
4 Verifying Temporal Requirements
Several behavioural properties of (composite) timed and hybrid automata models may be expressed as simple reachability properties. This is already illustrated previously in Sect. 3.2, where we saw that language inclusion between the “exact” hybrid automaton model H of a heart cell and a proposed timed automaton abstraction A could be stated as a simple reachability property of rejecting locations in a product between H and the complement of A. However, it may often be more convenient to express desired properties of a timed or hybrid automaton directly as formulas of temporal logic, thus permitting properties to be combined using boolean connectives. In fact the whole spectrum of temporallogic has been extended to the setting of timed labelled transition systems, with model checking suitably extended to timed automata, see e.g. [9]. In this section we demonstrate how timed automata verification using Uppaal may be used in establishing key properties of the pacemaker.
4.1 Timed Automaton of a Heart Cell in Uppaal
4.2 Requirement Specifications

\(\mathbf {A}\Box \varphi \), which is satisfied if any reachable state satisfies \(\varphi \) (Invariance),

\(\mathbf {A}\Box _{\le T}\varphi \), which is satisfied if any state reachable within T timeunits satisfies \(\phi \) (Timebounded Invariance),

\(\mathbf {A}\Diamond \varphi \), which is satisfied if on any path the properties \(\varphi \) is (eventually) satisfied at some point (Eventual),

\(\mathbf {A}\Diamond _{\le T}\varphi \) which is satisfied if on any path the property \(\varphi \) is satisfied within T timeunits \(\varphi \) (TimeBounded Eventual),

\(\varphi \leadsto _{\le T}\psi \), which requires than whenever a state is reached satisfying \(\varphi \), then any path from this state must eventually satisfy \(\psi \) – and within a total of T timeunits. Logically, the (timebounded) leadsto property is equivalent to \(\mathbf {A}(\varphi \Rightarrow \mathbf {A}\Diamond _{\le T}\psi )\) (TimeBounded Leadsto).
For deterministic timed labelled transition systems, it may easily be shown that all of the above properties – as they all quantify universally over execution sequences out of a state – are preserved by language inclusion. Thus, if \(\mathcal{L}_H\subseteq \mathcal{L}_A\) and A has been verified to satisfy a TCTL property \(\varphi \) of the above type, then it may readily be concluded that the “exact” model H also satisfies \(\varphi \).
Moreover, as demonstrated in [1] all of the above properties may be expressed directly as a reachability property—i.e. invariance properties—of the given timed automaton composed with a monitor corresponding to the property.
4.3 Healthy Heart Requirements
In case of our chain of heart cell timed automata – using the above pattern – the duration between Open image in new window and Open image in new window is found to be bounded by the interval of [0, N]ms, where N is the number of cells in series. Due to congruence properties of abstraction, this bound is guaranteed to be valid also for the composition of hybrid heart cells in Fig. 5.
4.4 Abstraction of Cell Composition
4.5 Pacemaker Requirements
Resources used by Uppaal to verify properties from Fig. 16.
Pacemaker model  URL  LRL  

Time  Memory  Result  Time  Memory  Result  
Basic DDD  0.01 s  5.37 MB  OK  0.01 s  5.37 MB  OK 
DDDVDI  129.57 s  248.26 MB  OK  148.58 s  267.78 MB  Not OK 
5 Future Directions and Challenges
As illustrated by the case study presented in this paper, modelbased design and verification is a promising approach to the development of cyberphysical systems in a principled manner, and the foundations of this methodology lie in crossfertilization of ideas from mathematical modeling and algorithmic analysis. As systems keep getting more and more complex, and society increasingly relies upon the internet of things, advances in tools for designing such systems are crucial to ensuing the safe and reliable operation of systems. This calls for continued research in core areas of formal methods such as identification of analyzable design abstractions, analysis techniques, and scalability of tools. We conclude this paper by highlighting some directions for future research.
Scalability: Given the computational intractability of the computational problems in formal verification, developing tools that can analyze realworld systems will always remain a challenge. The experience with tools such as Uppaal demonstrates that small steps in advancing the scalability collectively contribute towards impressive results over the long haul. For the verification of hybrid systems, tools based on robustness analysis offer promising opportunities [14, 15]. Robust analysis means that results obtained should not be too sensitive with respect to the actual quantities (timing, voltages, energy, etc.) used in the underlying model. Efforts on identifying metrics that will ensure “continuity” of various behavioral properties are currently being researched for a number of quantitative modeling formalisms. As illustrated in Sect. 3, abstraction is an effective way of reducing the complexity of a system, and developing techniques for constructing abstractions automatically remains a challenge.
Quantitative Analysis: Traditionally, models and techniques used for establishing correctness and for evaluating performance have been disjoint. In our pacemaker case study, beyond functional correctness of the control algorithm, we are also interested in estimating, for instance, the average energy used by the pacemaker. A promising new direction in formal methods research these days is the development of probabilistic models, with associated tools for quantitative evaluation of system performance along with correctness (see [23]).
Applications: Given the scalability challenges, formal methods for the design and analysis of cyberphysical systems are not yet widely applicable. Thus, identifying application domains and problems where the current techniques and tools can be applied effectively is itself a challenge that requires an understanding of formal methods as well as the application domains. As our example of pacemaker suggests, medical cyberphysical systems is a promising domain, and other interesting recent case studies include an infusion pump and an artificial pancreas [27]. Another promising domain of application is ensuring the safety of controllers used in autonomous vehicles [24].
DataDriven Models: As our case study illustrates, a key step is the construction of the heart model. Mathematical models of physical systems are hard to obtain, but increasingly, due to the rapid proliferation of sensors, lots of data is available. This leads to a new research question: given the pacemaker algorithm and the property that we want to verify, can we construct a patientspecific model of the heart derived from the sensory data obtained from a patient? Deriving models suitable for formal analysis from data is a challenging, and relatively unexplored, research area.
Notes
Acknowledgements
This research was supported in part by the Austrian Science Fund (FWF) under grants S11402N23(RiSE/SHiNE) and Z211N23 (Wittgenstein Award). This research has received funding from the SinoDanish Basic Research Centre, IDEA4CPS, funded by the Danish National Research Foundation and the National Science Foundation, China, the Innovation Fund Denmark centre DiCyPS, as well as the ERC Advanced Grant LASSO.
References
 1.Aceto, L., Bouyer, P., Burgueño, A., Larsen, K.G.: The power of reachability testing for timed automata. In: Arvind, V., Ramanujam, S. (eds.) FSTTCS 1998. LNCS, vol. 1530, pp. 245–256. Springer, Heidelberg (1998). https://doi.org/10.1007/9783540493822_22CrossRefGoogle Scholar
 2.Alur, R.: Principles of CyberPhysical Systems. MIT Press, Cambridge (2015)Google Scholar
 3.Alur, R., Courcoubetis, C., Dill, D.: Modelchecking in dense realtime. Inf. Comput. 104(1), 2–34 (1993)MathSciNetCrossRefGoogle Scholar
 4.Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T., Ho, P.H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoret. Comput. Sci. 138, 3–34 (1995)MathSciNetCrossRefGoogle Scholar
 5.Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183–235 (1994)MathSciNetCrossRefGoogle Scholar
 6.Alur, R., Henzinger, T., Lafferriere, G., Pappas, G.: Discrete abstractions of hybrid systems. Proc. IEEE 88(7), 971–984 (2000)CrossRefGoogle Scholar
 7.Behrmann, G., David, A., Larsen, K., Pettersson, P., Yi, W.: Developing uppaal over 15 years. Softw.  Pract. Exp. 41(2), 133–142 (2011)CrossRefGoogle Scholar
 8.Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFMRT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004). https://doi.org/10.1007/9783540300809_7CrossRefGoogle Scholar
 9.Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Ouaknine, J., Worrell, J.: Model checking realtime systems. In: Clarke, E., Henzinger, T., Veith, H. (eds.) Handbook of Model Checking. Springer, Heidelberg (2017)zbMATHGoogle Scholar
 10.Chen, T., Diciolla, M., Kwiatkowska, M., Mereacre, A.: Quantitative verification of implantable cardiac pacemakers over hybrid heart models. Inf. Comput. 236, 87–101 (2014). Special Issue on Hybrid Systems and BiologyMathSciNetCrossRefGoogle Scholar
 11.Clarke, E., Grumberg, O., Long, D.: Model checking and abstraction. In: Proceedings of 19th ACM Symposium on Principles of Programming Languages, pp. 343–354 (1992)Google Scholar
 12.Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)zbMATHGoogle Scholar
 13.Derler, P., Lee, E.A., SangiovanniVincentelli, A.L.: Modeling cyberphysical systems. Proc. IEEE 100(1), 13–28 (2012)CrossRefGoogle Scholar
 14.Duggirala, P.S., Fan, C., Mitra, S., Viswanathan, M.: Meeting a powertrain verification challenge. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 536–543. Springer, Cham (2015). https://doi.org/10.1007/9783319216904_37CrossRefGoogle Scholar
 15.Fainekos, G.E., Sankaranarayanan, S., Ueda, K., Yazarel, H.: Verification of automotive control applications using STaLiRo. In: IEEE American Control Conference, pp. 3567–3572 (2012)Google Scholar
 16.Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 258–273. Springer, Heidelberg (2005). https://doi.org/10.1007/9783540319542_17CrossRefzbMATHGoogle Scholar
 17.Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011). https://doi.org/10.1007/9783642221101_30CrossRefGoogle Scholar
 18.Henzinger, T.A., Sifakis, J.: The embedded systems design challenge. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 1–15. Springer, Heidelberg (2006). https://doi.org/10.1007/11813040_1CrossRefGoogle Scholar
 19.Henzinger, T.A.: The theory of hybrid automata. In: Inan, M.K., Kurshan, R.P. (eds.) Verification of Digital and Hybrid Systems, vol. 170, pp. 265–292. Springer, Heidelberg (2000). https://doi.org/10.1007/9783642596155_13CrossRefGoogle Scholar
 20.Henzinger, T.A., Ho, P.H., WongToi, H.: HyTech: a model checker for hybrid systems. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 460–463. Springer, Heidelberg (1997). https://doi.org/10.1007/3540631666_48CrossRefGoogle Scholar
 21.Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94–124 (1998)MathSciNetCrossRefGoogle Scholar
 22.Jiang, Z., Pajic, M., Moarref, S., Alur, R., Mangharam, R.: Modeling and verification of a dual chamber implantable pacemaker. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 188–203. Springer, Heidelberg (2012). https://doi.org/10.1007/9783642287565_14CrossRefGoogle Scholar
 23.Kwiatkowska, M.: Quantitative verification: models, techniques, and tools. In: Proceedings of ACM SIGSOFT Symposium on Foundations of Software Engineering, pp. 449–458 (2007)Google Scholar
 24.Larsen, K.G., Mikučionis, M., Taankvist, J.H.: Safe and optimal adaptive cruise control. In: Meyer, R., Platzer, A., Wehrheim, H. (eds.) Correct System Design. LNCS, vol. 9360, pp. 260–277. Springer, Cham (2015). https://doi.org/10.1007/9783319235066_17CrossRefGoogle Scholar
 25.Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. Int. J. Softw. Tools Technol. Transf. 1(1–2), 134–152 (1997)CrossRefGoogle Scholar
 26.Lee, E.A.: What’s ahead for embedded software. IEEE Comput. 33, 18–26 (2000)CrossRefGoogle Scholar
 27.Lee, I., Sokolsky, O., Chen, S., Hatcliff, J., Jee, E., Kim, B., King, A., MullenFortino, M., Park, S., Roederer, A., Venkatasubramanian, K.: Challenges and research directions in medical cyberphysical systems. Proc. IEEE 100(1), 75–90 (2012)CrossRefGoogle Scholar
 28.Pajic, M., Jiang, Z., Lee, I., Sokolsky, O., Mangharam, R.: Safetycritical medical device development using the UPP2SF model translation tool. ACM Trans. Embed. Comput. Syst. 13(4), 127:1–127:26 (2014)Google Scholar
 29.Vardi, M., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1–37 (1994)MathSciNetCrossRefGoogle Scholar
 30.Ye, P., Entcheva, E., Grosu, R., Smolka, S.A.: Efficient modeling of excitable cells using hybrid automata. In: Proceedings of Computational Methods in System Biology, pp. 216–227 (2005)Google Scholar