Conformance Testing of Cyber-Physical Systems: A Comparative Study
Electronic Communications of the EASST
Volume 70 (2014)
Proceedings of the
14th International Workshop on
Automated Verification of Critical Systems (AVoCS 2014)
Conformance Testing of Cyber-Physical Systems:
A Comparative Study
Morteza Mohaqeqi, Mohammad Reza Mousavi and Walid Taha
16 pages
Guest Editors: Marieke Huisman, Jaco van de Pol
Managing Editors: Tiziana Margaria, Julia Padberg, Gabriele Taentzer
ECEASST Home Page: http://www.easst.org/eceasst/ ISSN 1863-2122
http://www.easst.org/eceasst/
ECEASST
Conformance Testing of Cyber-Physical Systems:
A Comparative Study
Morteza Mohaqeqi1, Mohammad Reza Mousavi2 and Walid Taha3 ∗
1 m.mohaqeqi@ut.ac.ir
School of Electrical and Computer Engineering, University of Tehran, Iran
Center for Research on Embedded Systems, Halmstad University, Sweden
2 m.r.mousavi@hh.se
Center for Research on Embedded Systems, Halmstad University, Sweden
3 walid.taha@hh.se
Center for Research on Embedded Systems, Halmstad University, Sweden
Rice University, USA
Abstract: For systematic and automatic testing of cyber-physical systems, in which
a set of test cases is generated based on a formal specification, a number of notions
of conformance testing have been proposed. In this paper, we review two existing
theories of conformance testing for cyber-physical systems and compare them. We
point out their fundamental differences, and prove under which assumptions they
coincide.
Keywords: Hybrid systems, conformance testing, (hybrid) timed state sequences,
and hybrid labeled transition systems.
1 Introduction
Cyber-physical systems are “integrations of computation, networking, and physical processes”
[1]. Such systems are interdisciplinary by their nature and hence, experts from different dis-
ciplines have brought in different techniques for their specification, design, and analysis. This
enables cross-fertilization of approaches among several disciplines but to achieve that, it requires
reconciliation among the different techniques.
Model-based testing of cyber-physical systems is a relatively new concept that has been stud-
ied by few researchers from different backgrounds, e.g., regarding the integration of discrete
and continuous dynamics (i.e., the so-called hybrid systems) models for testing [BK06, vO06,
vO09, ABW09, BWA10, Dan10, WLT13, AHF+14, AFM14] and considering (asynchronous)
networked systems and models and hence such a reconciliation has yet to take place.
Two notable examples of model-based testing theories for these systems in the literature are:
the hioco relation by van Osch in [vO06, vO09] and the conformance relation by Abbas et al. in
[AHF+14], which we refer to as hconf. (Note that both approaches focus on the hybrid systems
modeling aspect of cyber-physical systems and do not address their distributed and networked
∗ This author was supported by the US NSF CPS award 1136099.
1 / 16 Volume 70 (2014)
mailto:m.mohaqeqi@ut.ac.ir
mailto:m.r.mousavi@hh.se
mailto:walid.taha@hh.se
Conformance Testing of CyPhy Systems
nature; for the latter, see, e.g., [WW09, SP10, NKM+14] .) The hioco theory is based on hybrid
transition systems formalism, which allows to specify both discrete input and output actions, and
continuous behavior. On the other hand, under hconf, the conformance relation is considered
as a measure of distance between the observable discretized (sampled) behavior of systems.
These two approaches are substantially different since they stem, respectively, from the computer
science- and control theory point of view on model-based testing. Our general goal of research is
to come up with a notion that reconciles these two views, and we start with a formal and in-depth
comparison. Concerning the specific research question addressed in this paper, we were mainly
intrigued by the following statement from [AHF+14]:
It can be verified that the hioco relation by van Osch is an exact version of (T,J,(τ,ε))-
closeness (τ = ε = 0) with the role of inputs and outputs made explicit.
We aimed at formalizing and proving this claim. (Note that “the exact version of (T,J,(τ,ε))-
closeness” is what we call “hconf” in the remainder of this paper.)1 However, even if we set aside
the issue of explicit input and output, it turns out there are other fundamental differences between
the two notions that went unnoticed in this statement. Hence, we will first point out the main
differences between the two notions (which will also guide our future research in reconciling
them) and subsequently, seek a restricted setting in which the above-mentioned claim does hold.
We then formalize and prove the above-mentioned statement in this restricted setting.
As a common ground for our comparison, we use a restricted subset of Hybrid Automata, of
which the restrictions are given and motivated in the remainder of this paper. We then translate
this subset into the semantic domains of the two notions of conformance and show that the
notions of conformance for the translated hybrid automata coincide in both domains.
1.1 Running Example
We consider a bouncing ball as a simple example of a system exhibiting both continuous and
discrete behavior. The ball is dropped with an initial height and an initial velocity. Naturally, it
is under the force of gravity. However, a vertical force can also be applied to the ball, which is
considered as the input to this system. Collision with the floor leads to a bounce, which causes
the ball to move in the reverse direction with the speed reduced by a factor ρ . The movement
of the ball between two consecutive collisions is accounted as a continuous behavior, while the
collision with the floor is considered a discrete jump.
We can use a hybrid automaton to formally specify the behavior of the ball. We define three
continuous variables h, v, and a for specifying the behavior of the ball, where h denotes the
height, v denotes the vertical velocity, and a is the (vertical downward) acceleration caused by
the force exerted on the ball. Consequently, the dynamics of this system can be captured by
a hybrid automaton with one location, as shown in Fig. 1a. The dynamics associated to this
location is specified as ḣ = v and v̇ =−g−a, where g is the gravity constant.
Figure 1b shows the behavior of the system, starting with initial condition h = 5 and v = 2,
while no vertical force is applied to the system.
1 Informally, two observed behavior satisfy (T,J,(τ,ε))-closeness relation if in each interval of length τ , there exists
one point in each of them with difference less than ε .
Proc. AVoCS 2014 2 / 16
ECEASST
l0
ḣ = v
v̇ =−g−a
Guard :
{
h = 0
v ≤ 0
Reset :
{
h+ = 0
v+ =−ρ v
(a) Hybrid automaton
0
2
4
6
8
0
5
10
15
20
0
1
2
3
4
5
6
7
8
jumps
f
3
f
2
time
f
1
H
e
ig
h
t
(h
)
(b) A sample behavior of the ball
Figure 1: Bouncing ball example
1.2 Related Work
In the realm of model-based conformance testing, Tretmans proposed the theory of input/output
(I/O) conformance (ioco) testing for discrete event systems [Tre96]. Afterwards, this theory was
extended to real-time systems [BB05], where in addition to discrete states of the system, the
evolution of a continuous variable, namely time, is modeled.
Conformance testing for cyber-physical systems (of which formal models are called hybrid
systems in this paper), also, has been approached by a relatively small number of studies. In
addition to the two aforementioned studies [vO06] and [AHF+14], which will be explained in
detail in the next sections, conformance testing of hybrid systems using some notion of over-
approximation has been proposed in [ABW09] and [BWA10]. These studies exploited a quali-
tative reasoning in order to obtain a discrete representation (abstraction) of a hybrid system. In
a qualitative system, the continuous domains are abstracted into finite sets of quality levels and
intervals. They proposed a method for obtaining a qualitative transition system from a hybrid
system, which provides a discrete-event view to the system. Then, the ioco relation is applied to
the obtained transition system. While this approach leads to finite representation of the hybrid
system, it suffers from information loss occurred in the abstraction step.
Bringmann et al. [BK06] used stream-processing functions [MS97] for specifying test cases
for hybrid systems. In this formalism, the continuous behavior of the variables is captured by the
notion of streams. A stream-processing function or component relates a stream on input variables
to a stream of output ones. Based on this notion, they propose a language for describing the test
sets. They focus on how to specify test cases for hybrid systems. However, they provide no
formal definition for conformance relation of hybrid systems.
In addition, Woehrle et al. [WLT13] investigated the problem of conformance testing of cyber-
physical systems through measurement of a number of physical quantities like power consump-
tion of the computing system. They employed timed automata to specify the system behavior.
Then, the measured physical variable is compared against the automata to verify that if the sys-
tem behavior conforms to its specification. Their method does not actually model the hybrid
behavior of a system, but only considers time as a continuous variable. A conformance rela-
3 / 16 Volume 70 (2014)
Conformance Testing of CyPhy Systems
tion for hybrid systems has been also defined based on the notion of hybrid automata in [Dan10].
While the underlying formalism is different from the hybrid labeled transition system that is used
by van Osch [vO06], the semantic model of the two conformance relations is similar [Dan10].
1.3 Paper Organization
The remainder of this paper is structured as follows. In Section 2, we review the hioco and hconf
theories and point out the fundamental differences both between their semantic models and their
conformance relations. In order to show the equivalence of the two conformance relations under
specific assumptions, we first provide a method for translating a given hybrid automaton (in the
restricted semantic domain) to each of the models in Section 3. Then, in Section 4, we show that,
based on the proposed translation method, the two notions of conformance coincide. The paper
concludes in Section 5, where we also describe our plan for future work.
2 Formal Definitions and Fundamental Differences
In this section, we first formally introduce system models that are used in the two aforementioned
approaches, namely [vO06] and [AHF+14]. Afterwards, we point out the fundamental differ-
ences in their modeling approach and their assumptions. These will motivate the assumptions
that we have made to pave the way for a meaningful comparison between the two conformance
relations. Then, we review the conformance relations proposed by the two studies, and state the
fundamental differences between them.
2.1 Formal Models
In the following, we first introduce some basic definitions. Then, we formally specify the system
models employed in [vO06] and [AHF+14], namely, hybrid labeled transition system and hybrid-
timed state sequence model, respectively.
2.1.1 Basic Definitions
A hybrid system is a system exhibiting both continuous and discrete behavior. The continuous
behavior of the system is captured by the valuation of a set of continuous variables, denoted by
V . We assume that V is partitioned into a set of input variables, denoted by VI , and a set of output
variables, denoted by VO. A valuation on V is defined as a function which assigns a value to
each variable v ∈ V ; here, only variables of type real are considered. The set of all valuations
of V is denoted by Val(V ) and is defined as the set of all functions V → R. To describe the
(non-interrupted) continuous evolution of the system, we use the following notion of trajectory
[LSV03].
Definition 1 (Trajectory [vO06]) Let D ⊂R be an interval (here, singleton sets of numbers are
also considered as intervals). A trajectory σ is a function σ : D→Val(V ) that maps each element
in interval D to a valuation. The set of all trajectories associated to V is denoted by trajs(V).
Proc. AVoCS 2014 4 / 16
ECEASST
Beside continuous evolution, a hybrid system features discrete changes, called jumps or switches.
A jump happens instantly, leading to a possibly noncontinuous change.
Further, we consider a restriction operator on the functions as follows.
Definition 2 (Function Restriction) Consider an interval D ⊂ R, a set V of variables, and a
function f : D → Val(V ); we define the restricted function f ↓V ′ for some V ′⊆V as the function
of type D → Val(V ′), such that for each d ∈ D, f (d) ↓ V ′ is obtained from f (d) after removing
variables not in V ′.
2.1.2 Hybrid Labeled Transition System
In the approach adopted by van Osch [vO06], a hybrid system is modeled as a hybrid labeled
transition system (HLTS). An HLTS, formally defined below, consists of a set of states with
discrete (action) and continuous (trajectory) transitions between them. Actions are partitioned
into three classes, namely, input-, output-, and internal actions. The latter class is not observable
from outside.
Definition 3 (Hybrid Labeled Transition System [vO06]) A hybrid labeled transition system
(HLTS) H, over a given set A of actions, is a 5-tuple (S,s0,V,L,→), where
• S is a (possibly infinite) set of states;
• s0 ∈ S is the initial state;
• V = VI ]VO is a set of (resp. input or output) continuous variables;
• L = A]trajs(V) is a set of (resp. action or trajectory) labels;
• →⊆S×(L∪{ξ})×S specifies the transition relation, where ξ denotes the internal action.
We may write s
l→ s′ instead of (s,l,s′)∈→. Moreover, we define a notion of generalized transi-
tion relation for an HLTS as follows. For the purpose of this paper, we assume the set of actions
to be empty. We will also henceforth simplify the definitions for this restricted subset of HLTSs.
Definition 4 (Generalized Transition Relation) Consider an HLTS H = (S,s0,V,L,→). A gen-
eralized transition relation for H is defined as the smallest relation ⇒⊆ S×(L)∗×S where
• s ε⇒ s;
• if s
ξ
→ s′, then s ε⇒ s′,
• ∀l ∈ L, if s l→ s, then s l⇒ s;
• ∀α,β ∈ L∗, if s α⇒ s′′ and s′′
β
⇒ s′, then s
α β
⇒ s′;
We write s
α⇒ to denote that there exists a s′ ∈ S such that s α⇒ s′. The behavior of a system is
specified by its set of traces, which are finite sequences of trajectories. (The internal actions are
abstracted away in the traces.)
5 / 16 Volume 70 (2014)
Conformance Testing of CyPhy Systems
Definition 5 (Trace) For HLTS H, a trace is a finite sequence α ∈ L∗ such that s0
α⇒, where s0
is the initial state of H.
The length of a trace is defined as the number of elements of the sequence and is represented
by |α|. We denote the set of all traces of H by traces(H).
Example 1 Consider the bouncing ball example. Collision with the floor can be considered as
an internal action. Also, the curves f1, f2, and f3 in Fig. 1b denote some trajectories of the
system (projected only to one variable h). Hence, the sequences f1 f2 and f1 f2 f3 are two traces
of this system.
An HLTS can be input-enabled, as defined in the following.
Definition 6 (Input-Enabled HLTS) An HLTS is input-enabled if
∀s ∈ S,∀τ ∈ trajs(VI) : ∃τ′ ∈ trajs(V ) such that τ′ ↓VI = τ ∧s
τ
′
⇒.
2.1.3 Timed State Sequence (TSS) Model
The approach proposed in [AHF+14] specifies a hybrid system as a mapping from pairs of initial
conditions and input signals to output signals. The input and output signals of the system are
described through a notion of timed-state sequence (TSS). (We slightly adapt the notation to
make it consistent among the different semantic models.)
Definition 7 (Hybrid-Timed State Sequence (TSS) [AHF+14]) Consider N ∈N, T = R≥0×N,
and a set of variables V . A hybrid-timed state sequence (TSS) is defined as pair (x,σ), where x ∈
(Val(V ))N and σ ∈TN . The i th element of a TSS (x,σ) is denoted by (xi,σ i), where σ i=(ti, ji)∈
T. Also, we denote the set of all TSSs defined over the set of variables V , considering a specific
N ∈N, by TSS(V,N).
A TSS describes the valuation of a set of (input/output) variables in a finite number of time
instants. In this notion, a time instant is denoted by a pair (t, j), where t is a real number
denoting the real time, and j is an integer which denotes the number of discrete jumps until that
time instant. We refer to this semantic model as the TSS model.
Example 2 The sequence ((1,1,1),((0,0),(4.5,0),(6,1))) is a TSS for the running example,
defined for the variable a, where the tuple (1,1,1) denotes the value of a in three time instants
(0,0),(4.5,0), and (6,1). For instance, the pair (6,1) shows the instant that real time is 6 and the
system has experienced one discrete jump. Similarly, the sequence
((5,6.55,7.1,6.65,5.2,2.75,0.19),((0,0),(1,0),(2,0),(3,0),(4,0),(5,0),(6,1)))
denotes an output TSS for the considered system, denoting a valuation of the output variable h.
Assume a set of input variables VI with a corresponding compact set of possible values Val(VI)
and a set of output variables VO with a set of possible valuations Val(VO). Accordingly, the set of
Proc. AVoCS 2014 6 / 16
ECEASST
input TSSs and output TSSs can be respectively defined by TSS(VI,N) and TSS(VO,N). Also,
let H be the set of initial conditions.
A hybrid system can be viewed as a mapping between the initial condition and the input TSSs
(u,σu)∈TSS(VI,N) to the output TSSs (y,σy)∈TSS(VO,N).
Definition 8 (Hybrid System [AHF+14]) Hybrid system H is modeled as a mapping:
H : H ×TSS(VI,N) 7→TSS(VO,N)
We write yH(h0,(u,σu)) to denote the output TSS to which the pair (u,σu) is mapped by H,
considering h0 as the initial condition. In [AHF+14], it is assumed that the system is always
input-enabled, with the following definition of input-enabledness.
Definition 9 (Input-Enabled System) A hybrid system H is input-enabled if
∀h0 ∈ H,∀(u,σu)∈TSS(VI,N) : ∃(y,σy)∈TSS(VO,N) such that (y,σy) = yH(h0,(u,σu)).
In other words, the system is input-enabled if it produces an output for every initial condition
and input TSS.
2.2 Differences in Semantic Models
The following list provides an overview of the fundamental differences among the two underly-
ing semantic models, reviewed in Subsection 2.1. After explaining each difference, we state the
assumption we have made for the common semantic domains that makes a meaningful compari-
son possible.
• Explicit discrete interactions vs. unlabeled jumps. In HLTSs, an explicit notion of in-
put/output actions is introduced, while TSSs provide no explicit means for modeling dis-
crete input/output actions of the system. In order to have a unified semantic model for
the two models, we do not consider explicit interactions in HLTSs and model all discrete
jumps of the system as internal actions when using HLTSs. (A1)
• Partial specifications vs. input-enabled models. HLTSs used for hioco allow for partial
specifications, in which the (output) response to certain (input) traces is left unspecified.
However, the input-enabledness assumption made in the TSS model implies that for ev-
ery sequence of input signal, the model should specify an output behavior of the system,
expressed in terms of an output TSS. To allow for a meaningful comparison, we only
consider input-enabled models. (A2)
• Unique initial state vs. arbitrary initial condition. HLTSs specify a unique initial state,
while TSSs allow for arbitrary initial conditions. In order to make the two models com-
patible, we assume a singleton set of initial condition for the TSS model. (A3)
• Nondeterministic specifications vs. deterministic models. HLTSs allow for non-deteminism
both in the discrete and the continuous behavior, as an abstraction mechanism for unspec-
ified / irrelevant details. However, hybrid systems in the hconf model are mappings from
input TSSs to output TSSs and hence, are deterministic in nature. To make the comparison
possible, we only consider deterministic models. (A4)
7 / 16 Volume 70 (2014)
Conformance Testing of CyPhy Systems
• Continuous trajectories vs. discretized samples. HLTSs allow for specification of con-
tinuous trajectories while hybrid systems in the hconf theory are necessarily discretized.
This alone may not be a major issue (i.e., hioco is also defined for discretized samples
in [vO09, Chapter 6]); however, in combination with determinism and input-enabledness
this assumption has far-reaching consequences, namely, if two continuous input trajecto-
ries have the same discretized behavior for one arbitrary sampling, they should lead to the
same output behavior. To make the comparison feasible, we assume the latter property in
the models studied in the remainder of this paper. (A5)
Considering these differences one comes away with the impression that the two models have
distinct purposes and strengths. In particular, HLTSs as the semantic models of hioco are suit-
able for high-level partial specifications that leave some room for future design decisions and
also only specify certain aspects of the system. However, TSSs used as the semantic models
of hconf are suitable for low level specifications that provide a complete and deterministic (dis-
cretized) recipe for implementation. An ideal notion of conformance, in our view, should relax
assumptions (A1)-(A5). In other words, an ideal theory of conformance should combine the lib-
eral semantic domain of hioco with the practical conformance relation of hconf, as pointed out
in the next section.
2.3 Conformance Relations
In this subsection, we review the two designated notions of conformance testing for hybrid sys-
tems, based on the formal models defined in Subsection 2.1.
2.3.1 HIOCO
In this section, we review the hybrid input-output conformance (hioco) theory [vO06], simplified
according to the assumptions made in Section 2.2.
Definition 10 (after Operator) For an HLTS H and a trace α ∈ traces(H), we define
H after α =
{
s
∣∣∣s0 α⇒ s}
Definition 11 (Trajectories of a State) For an HLTS H and a state s, traj(s) is defined as
traj(s) =
{
σ ∈ trajs(V )| s σ⇒
}
This definition can also be extended to a set of states C ⊆ S as traj(C) =
⋃
s∈C traj(s)
Using the above-given definitions, we are now ready to define the notion of hioco (simplified
by neglecting discrete actions and restriction to input-enabled specifications).
Definition 12 (Hybrid I/O Conformance [vO06]) Consider an HLTS S; an input-enabled HLTS
I is said to be hybrid input-output conforming to S, denoted by Ihioco S, if and only if for all
traces α ∈ traces(S):
Proc. AVoCS 2014 8 / 16
ECEASST
traj (I after α)⊆ traj (S after α)
The symmetric kernel of hioco, is denoted by =hioco. Under the assumption of Section 2.2,
hioco is a pre-order and =hioco is an equivalence relation.
2.3.2 HCONF
To define the notion of conformance, the notion of (τ,ε)-closeness is defined to measure how
much a given TSS deviates from another TSS. Informally, two TSSs are said to be (τ,ε)-close
if, for any time interval of length τ , and each sampled point in one, there exists a sample point in
the other such that the difference between the valuations in the two points is less than ε . Based
on this notion, two systems are conforming if, for all combinations of initial conditions and input
TSSs, the respective output TSS of the two systems are close to each other.
In order to be consistent with the hioco conformance relation, we only consider the confor-
mance relation for TSS models for (0,0)-closeness [AHF+14]. Consider a maximum number of
jumps N ∈N for which we are to perform the test.
Definition 13 (hconf [AHF+14]) Two systems HM and HI are said to be conforming if for any
input TSS (u,σu)∈TSS(VI,N)
yHM (h0,(u,σu)) = yHI (h0,(u,σu))
We write HM hconf HI to denote that two systems HM and HI are conforming.
2.4 Differences in Conformance Relations
In addition to the fundamental differences in the semantic domain, which stated in Subsec-
tion 2.2, there are also fundamental differences in the way the two conformance relations are
defined. Below, we provide a concise list of such fundamental differences:
• Pre-order vs. equivalence relation. The conformance relation hioco is a pre-order (for
input-enabled specifications), while hconf is an equivalence relation. This stems from a
fundamental difference in whether the implementation may choose from the alternative
behaviors of the specification (pre-order view), or the implementation should implement
the behavior prescribed by the specification (equivalence view). (The notion of closeness
in hconf to some extent remedies this, and allows for deviations in the implementation.)
In order to make our comparison possible, we consider the symmetric kernel of hioco for
input-enabled specification, denoted by =hioco, and compare it with hconf.
• Projecting on specification traces/trajectories vs. considering all traces. Since the semantic
model of hioco allows for partial specification, the conformance relation also exploits that
by comparing the behavior of the implementation and specification only with respect to
those traces specified in the specification. This can potentially create major differences
between hioco and hconf. However, since we restricted our specifications to input-enabled
and deterministic ones, this difference is not visible in our results to follow.
9 / 16 Volume 70 (2014)
Conformance Testing of CyPhy Systems
• Exact vs. approximate comparison of trajectories. Conformance relation hioco compares
the continuous behaviors precisely, while hconf defines a notion of temporal and spatial
closeness is used to represent and measure the deviation of the implementation from the
specification. As indicated in the aforementioned claim of [AHF+14], we only consider
the exact version of hconf and compare it with hioco.
• Sensitivity to quiescence. In order to reject implementations that do not produce any
output when they should, the notion of quiescence is employed in hioco. Also, to denote
existence or absence of continuous trajectories the notion of agile states is introduced.
These notion are altogether absent in hconf, because hconf does not allow for the absence
of outputs. In the case of deterministic input-enabled models (both for specifications and
implementations, implied by our assumptions (A1)-(A5)), this difference is immaterial;
however, once the models are relaxed to allow for non-deterministic and/or partial models,
this difference may differentiate between the two notions of conformance.
3 Translating Hybrid Automata to the Other Models
In this section, we employ the notion of hybrid automata as a general formalism for hybrid sys-
tems and show how a hybrid automaton satisfying assumptions (A1)-(A5) can be translated to
each of the two considered semantic domains. For the purpose of this paper, we deal with a min-
imal definition of hybrid automaton as considered in [GST09], in which there is no distinction
between input and output actions.
Definition 14 (Hybrid Automata [GST09]) A hybrid automaton is defined as a tuple (Loc, V ,
(l0,v0), →, I, F ), where
• Loc is a finite set of locations;
• V is the set of continuous variables;
• l0 denotes the initial location and v0 is an initial valuation of V;
• →⊆ Loc×B(V )×Reset(V )×Loc is the set of jumps where:
– B(V )⊆ Val(V ) indicates the guards under which the switch may be performed, and
– Reset(V ) =
⋃
V ′⊆V Val(V
′) is the set of all value assignments to all or a subset of the
variables V ;
• I : Loc → B(V ) determines the allowed valuation of variables in each location (called the
invariant of the location);
• F : Loc → B(V
⋃
V̇ ) describes some constraints on variables and their derivatives and
specifies the allowed continuous behavior in each location.
As before, we write l
g,r
→ l′ for (l,g,r,l′)∈→.
The dynamic behavior of a hybrid automaton can be specified by a set of solutions. A solution
to a hybrid automaton is a function on a hybrid time domain, which is defined as follows.
Proc. AVoCS 2014 10 / 16
ECEASST
Definition 15 (Hybrid Time Domain [GT06, GST09]) A set E ⊂ R≥0 ×N is a hybrid time
domain if either:
• E =
⋃J−1
j=0([t j,t j+1], j), for a finite J, where t0 = 0 and t0 ≤ t1 ≤ t2 ≤ ...≤ tJ , tJ ≤ ∞; or
• E =
⋃
∞
j=0([t j,t j+1], j) , with t0 = 0 and t0 ≤ t1 ≤ t2 ≤ ...
For a hybrid time domain, we define time interval I j to be [t j,t j+1]. A time instant in the hybrid
time domain E is defined as a pair (t, j)∈ E.
Definition 16 (Solution of a Hybrid Automaton [Lem00]) A solution to the hybrid automaton
HA = (Loc,V,(l0,v0),→,I,F) is a function x : E → Loc×Val(V ), where E is a hybrid time
domain partitioned into a finite number J of intervals, and
• x(0,0) = (l0,v0);
• for a fixed j, x(t, j) : t → l j ×Val(V ) is a function over real time that satisfies I(l j) and
F(l j); and
• ∀ j ( J−1 > j ≥ 0) : ∃g ∈B(V ),r ∈ Reset(V ) such that
(
l j
g,r
−→ l j+1
)
∧
(x(t j+1, j)↓V satisfies g) ∧ (x(t j+1, j + 1)↓V = r).
The set of all solutions of a hybrid automaton HA is denoted by Solutions(HA). For a given
hybrid automaton HA, the determinism assumption (A4) yields:
∀s,s′ ∈ Solutions(HA) : (s ↓VI = s′ ↓VI)⇒ (s ↓VO = s′ ↓VO)
The length of a solution s is defined as the number of intervals in dom s.
3.1 Translating Hybrid Automata to Hybrid Labeled Transition Systems
According to Definition 3 and Definition 14, a hybrid automaton denotes an HLTS, as follows.
Definition 17 (T.UHLT S [vO06]) A hybrid automaton HA = (Loc,V,(l0,v0),→,I,F) can be
converted to an equivalent HLTS THAUHLT S = (Loc×Val(V ),(l0,v0),trajs(V ),→), where
• →={(l,u) σ→ (l′,u′)|
(
∃g,r : l
g,r
−→ l′
)
∧(u ∈ g)∧(u ∈ I(l))∧(u′ ∈ r)∧(u′ ∈ I(l′))∧
(u = σ.fval∧u′ = σ.lval)}
⋃
{(l,u) σ→(l,u′)|∃σ∈trajs(V ) : (u = σ.fval)∧(u′ = σ.lval)∧(σ satisfies F(l))∧(∀t ∈dom(σ) :
σ(t)∈ I(l))}
where, σ.fval and σ.lval respectively denote the value of σ at its starting (first) point and
ending (last) point.
3.2 Translating Hybrid Automata to Timed State Sequences
In order to convert a hybrid automaton to a TSS, we use the concept of the solution of the hybrid
automata.
11 / 16 Volume 70 (2014)
Conformance Testing of CyPhy Systems
Definition 18 (T.UT SS) Consider a hybrid automaton HA with the set of input variables VI and
the set of output variables VO. Further, let Solutions(HA) denote the set of all solutions of HA.
Thus, the TSS model which is defined by HA, denoted by THAUTSS, is the mapping:
H : (u,σu) 7→ (y,σy)
that is constructed from the set of solutions in such a way that, for any solution x∈Solutions(HA),
any input TSS (u,σu) obtained by discretizing x ↓VI is mapped to an output TSS (y,σy), where
• σy = σu;
• yi = x(ti, ji)↓VO, where (ti, ji) is the i th element of σu.
4 Equivalence of hioco and hconf
Theorem 1 Given a specification S in terms of a hybrid automaton and an implementation
of which the behavior is expressed by a hybrid automaton I. If both S and I satisfy conditions
A1-A5, then it holds that TSUT SS hconf TIUT SS if and only if TSUHLT S =hioco TIUHLT S.
Proof. The idea of the proof is that we define a notion of hybrid conformance relation for hybrid
automata and show that both hioco and hconf are equivalent to this notion of conformance. The
proof comprises the following two steps:
1. TSUHLT S =hioco TIUHLT S ⇔
∀s ∈ Solutions(S),∀s′ ∈ Solutions(I) : (s ↓VI = s′ ↓VI)⇒ (s ↓VO = s′ ↓VO)
2. TSUT SS hconf TIUT SS ⇔
∀s ∈ Solutions(S),∀s′ ∈ Solutions(I) : (s ↓VI = s′ ↓VI)⇒ (s ↓VO = s′ ↓VO)
To prove step 1, we provide a method for converting a solution in a hybrid automaton H to
an equivalent trace in the respective HLTS, and conversely, to convert a trace to a corresponding
solution.
Lemma 1 (Traces and Solutions Equivalence) Given a solution s ∈ Solutions(H), one can
uniquely obtain a trace τ ∈ traces(THUHLT S), with |τ|= |s|, and vice versa.
Proof. For a fixed N ≥ 0, consider a trace τ = α0α1...αN−1 ∈ traces(THU) with |τ| = N, and
let D j denote the continuous time interval over which α j is defined. We can associate a solution
s ∈ Solutions(H) with τ as follows. We specify the domain of s as dom s =
⋃N−1
j=0 I j, where I j is
defined as:
• I0 = [D0,0];
• I j = ([t j,t j+1], j), where t j+1 = t j +|D j| for j > 0;
Proc. AVoCS 2014 12 / 16
ECEASST
in which |D j| denotes the length of time interval D j. Furthermore, the value of the solution
s at time instant (t, j) is specified by the value of the respective trajectory at that instant, i.e.,
s(t, j) = α j(t −t j). Conversely, it can be shown that given a solution s ∈ Solutions(H), one can
uniquely obtain a trace τ ∈ traces(THUHLT S), with |τ|= |s|.
Next, we show that TSUHLT S =hioco TIUHLT S means that traces(TSUHLT S) = traces(TIUHLT S).
Then, using Lemma 1, the first step of the proof can be readily concluded.
Lemma 2 Consider two hybrid automata S and I. It holds that TSUHLT S =hioco TIUHLT S if and
only if traces(TSUHLT S) = traces(TIUHLT S).
Proof. For an HLTS H, let tracesN(H) denote the set of all traces of H which are of length N.
In other words, tracesN(H) = {α ∈ traces(H) : |α|= N}. The goal is to show, given TSUHLT S
=hioco TIUHLT S, that tracesN(TSUHLT S) = tracesN(TIUHLT S) for any N ≥ 0. We proceed by
induction on N.
We consider N = 0 as the base of induction, which includes empty trace ε . According to
Definition 4, and also with regard to Definition 5, it holds that ε ∈ traces(TSUHLT S) and ε ∈
traces(TIUHLT S). Therefore, traces0(TSUHLT S) = traces0(TIUHLT S).
For the induction step, assuming that tracesN(S) = tracesN(I), we need to show tracesN+1(S) =
tracesN+1(I). To this end, consider that tracesN+1(I) and tracesN+1(S), which can be defined as
follows:
tracesN+1(I) ={τ α | τ ∈ tracesN(I)∧α ∈ traj (I after τ)}
and
tracesN+1(S) ={τ α | τ ∈ tracesN(S)∧α ∈ traj (S after τ)}
We have that tracesN(S) = tracesN(I), and also according to Definition 12, traj (S after τ) =
traj (I after τ), we have tracesN+1(S) = tracesN+1(I), which completes the induction step.
(Note that according to assumptions A2 and A4 in Subsection 2.2, Definition 12 establishes the
former equality.)
For step 2 of the proof of Theorem 1, we first show that if Solutions(S) = Solutions(I) then
TSUT SS hconf TIUT SS. Note that the method for translating a hybrid automaton to a TSS described
in Definition 18 is deterministic. Moreover, the translation method constructs the respective TSS
solely based on the set of solutions of the hybrid automaton. Therefore, for two hybrid automata
S and I with the same set of solutions, the resultant TSSs are trivially equal. According to
Definition 13, this means that TSUT SS hconf TIUT SS.
To prove step 2, we further need to show that if TSUT SS hconf TIUT SS then Solutions(S) =
Solutions(I). We proceed with proof by contradiction. Assume that TSUT SS hconf TIUT SS and
Solutions(S) 6= Solutions(I). Therefore, it holds that
∃s ∈ Solutions(I) such that ∀s′ ∈ Solutions(S) : s 6= s′.
But, due the assumption that the considered hybrid automata are input-enabled, there exists an
s′ ∈ Solutions(I) for which s ↓ VI = s′ ↓ VI . But, as s 6= s′, we can conclude s ↓ VO 6= s′ ↓ VO,
which means that there is a time instant (t, j) for which s(t, j) 6= s′(t, j). Consider the input TSS
13 / 16 Volume 70 (2014)
Conformance Testing of CyPhy Systems
obtained by discretization of s, denoted as u that includes time instant (t, j). According to the
translation method from hybrid automaton to TSS described in Definition 18, the output TSS
to which TSUT SS maps the input TSS u differs from that of TIUT SS, which contradicts with the
assumption of TIUT SS hconf TIUT SS.
5 Conclusion
We studied two fundamental notions of conformance testing for cyber-physical systems, which
are to our knowledge the most notable notions of their kind. We have pointed out fundamental
differences, both in their semantic domains and in their definition of conformance. We identified
a set of conditions under which the two notions are comparable. We proved that under such
conditions, the two notions coincide.
While hioco is based on a richer and more expressive semantic domain, it suffers from prac-
tical concerns, which are related to its underlying infinite state-space. On the other hand, hconf
provides a more practical approach to checking conformance, but it ignores some important
aspects in modeling, including explicit discrete interactions, nondeterminism, and partial speci-
fications.
The dichotomy reflected in the difference in the two notions suggests that a natural next step
would be to define a more general notion of conformance testing for cyber-physical systems,
which consolidates the theoretical expressiveness of hioco with the practical approach of hconf
to conformance checking. Defining a test-case generation algorithm and proving soundness
and adequacy of the generated test cases (given some testing hypothesis) are among the future
milestones. Applying the resulting theory and tools to concrete cases of cyber-physical systems
is a necessary step in validating our future research.
Acknowledgements: We would like to thank the anonymous reviewers of AVOCS’14, Hous-
sam Abbas, Harsh Beohar, Pieter Cuijpers, Jim Kapinski, Mehdi Kargahi, and Mahsa Varshosaz
for their helpful comments.
Bibliography
[1] Cyber-Physical Systems - Concept Map, http://cyberphysicalsystems.org/ . Re-
trieved October 2014.
[AHF+14] H. Abbas, B. Hoxha, G. Fainekos, J. V. Deshmukh, J. Kapinski, K. Ueda. Confor-
mance testing as falsification for cyber-physical systems. In ICCPS. 2014.
Full paper available from: http://arxiv.org/abs/1401.5200
[AFM14] H. Abbas, G. Fainekos, and H. Mittelmann. Formal property verification in a confor-
mance testing framework. In MEMOCODE. 2014.
[ABW09] B. K. Aichernig, H. Brandl, F. Wotawa. Conformance testing of hybrid systems with
qualitative reasoning models. ENTCS 253(2):53–69, Oct. 2009.
Proc. AVoCS 2014 14 / 16
http://cyberphysicalsystems.org/
http://arxiv.org/abs/1401.5200
ECEASST
[AD94] R. Alur, D. L. Dill. A theory of timed automata. Theoretical computer science
126(2):183–235, 1994.
[BB05] L. B. Briones, E. Brinksma. A Test Generation Framework for Quiescent Real-time
Systems. In Proceedings of the 4th International Conference on Formal Approaches
to Software Testing. FATES’04, pp. 64–78. Springer-Verlag, Berlin, Heidelberg,
2005.
[BK06] E. Bringmann, A. Krämer. Systematic Testing of the Continuous Behavior of Au-
tomotive Systems. In Proceedings of the 2006 International Workshop on Software
Engineering for Automotive Systems. SEAS ’06, pp. 13–20. ACM, 2006.
[BWA10] H. Brandl, M. Weiglhofer, B. Aichernig. Automated Conformance Verification of
Hybrid Systems. In International Conference on Quality Software (QSIC). Pp. 3–12.
July 2010.
[CR08] P. J. Cuijpers, M. A. Reniers. Lost in translation: Hybrid-time flows vs. real-time
transitions. In Hybrid Systems: Computation and Control. Pp. 116–129. Springer,
2008.
[CRH02] P. J. L. Cuijpers, M. A. Reniers, W. P. M. H. Heemels. Hybrid transition systems.
Computer Science Reports 02-12, TU Eindhoven, 2002.
[Dan10] T. Dang. Model-based testing of hybrid systems. Monograph in Model-Based Testing
for Embedded Systems, CRC Press, 2010.
[GST09] R. Goebel, R. Sanfelice, A. Teel. Hybrid dynamical systems. IEEE Control Systems
Magazine 29(2):28–93, April 2009.
[GT06] R. Goebel, A. R. Teel. Solutions to Hybrid Inclusions via Set and Graphical Conver-
gence with Stability Theory Applications. Automatica 42(4):573–587, Apr. 2006.
[Lem00] M. Lemmon. On the Existence of Solutions to Controlled Hybrid Automata. In Hy-
brid Systems: Computation and Control. LNCS 1790, pp. 229–242. Springer, 2000.
[Lib03] D. Liberzon. Switching in systems and control. Springer, 2003.
[LSV03] N. Lynch, R. Segala, F. Vaandrager. Hybrid i/o automata. Information and Compu-
tation 185(1):105–157, 2003.
[MS97] O. Müller, P. Scholz. Functional specification of real-time and hybrid systems. In
Hybrid and Real-Time Systems. LNCS 1201, pp. 273–285. Springer, 1997.
[NKM+14] N. Noroozi, R. Khosravi, M.R. Mousavi, T.A.C. Willemse. Synchrony and Asyn-
chrony in Conformance Testing. Journal of Software and Systems Modeling,
Springer, 2014. In Press.
[vO06] M. van Osch. Hybrid input-output conformance and test generation. In Formal Ap-
proaches to Software Testing and Runtime Verification. LNCS 4262, pp. 70–84.
Springer, 2006.
15 / 16 Volume 70 (2014)
Conformance Testing of CyPhy Systems
[vO09] M. van Osch. Automated Model-based Testing of Hybrid Systems. Faculty of Math-
ematics and Computer Science, TU Eindhoven, 2009.
[SP10] A. Simao, A. Petrenko. From test purposes to asynchronous test cases. In Proc. of
ICSTW 2010, pp. 110. IEEE CS, 2010.
[Tre96] J. Tretmans. Test Generation with inputs, outputs and repetitive quiescence. Software
- Concepts and Tools 17(3):103–120, 1996.
[WW09] M. Weiglhofer, F. Wotawa. Asynchronous input-output conformance testing. In
Proc. of COMPSAC09, pp. 154159. IEEE CS, 2009.
[WLT13] M. Woehrle, K. Lampka, L. Thiele. Conformance testing for cyber-physical systems.
ACM Trans. Embed. Comput. Syst. 11(4):84:1–84:23, Jan. 2013.
Proc. AVoCS 2014 16 / 16
Introduction
Running Example
Related Work
Paper Organization
Formal Definitions and Fundamental Differences
Formal Models
Basic Definitions
Hybrid Labeled Transition System
Timed State Sequence (TSS) Model
Differences in Semantic Models
Conformance Relations
HIOCO
HCONF
Differences in Conformance Relations
Translating Hybrid Automata to the Other Models
Translating Hybrid Automata to Hybrid Labeled Transition Systems
Translating Hybrid Automata to Timed State Sequences
Equivalence of hioco and hconf
Conclusion