=Paper= {{Paper |id=Vol-2581/ase2020paper1 |storemode=property |title=Partial Consistency for Requirement Engineering with Traffic Sequence Charts |pdfUrl=https://ceur-ws.org/Vol-2581/ase2020paper1.pdf |volume=Vol-2581 |authors=Jan Steffen Becker |dblpUrl=https://dblp.org/rec/conf/se/Becker20 }} ==Partial Consistency for Requirement Engineering with Traffic Sequence Charts== https://ceur-ws.org/Vol-2581/ase2020paper1.pdf

Partial Consistency for Requirement Engineering
with Traffic Sequence Charts
Jan Steffen Becker
OFFIS – Institute for Information Technology
Oldenburg, Germany
jan.steffen.becker@offis.de

Abstract—In the context of autonomous driving, new chal- developed as a formal specification language. The contribution
lenges arise also in the requirements engineering process. The of this paper is a formal but yet practical approach to find
specification needs to deal with a complex, open and highly inconsistencies in TSC specifications.
dynamic context, which makes it hard to find an appropriate
and still comprehensible formalism for the specification. Also, Traffic Sequence Charts are a graphical specification lan-
the requirements come from different sources, such as traffic guage for traffic scenarios. As a running example, Figure 1
regulations and consumer needs, which makes it difficult but shows a TSC that specifies how the HAV under develop-
yet important to maintain requirements consistency. This work ment (white car in the figures) shall overtake slower ve-
focuses on consistency of those requirements that specify execu- hicles (black car) on a highway. The TSC is described in
tion of driving maneuvers. In previous work, Traffic Sequence
Charts have been introduced as a specification language for detail in Section II. The core idea of TSCs is to represent
those requirements. Traffic Sequence Charts are a graphical a scenario as a seamless sequence of traffic situations, so
formalism with a well-defined formal semantics that enables called snapshots. In each snapshot, the placement of symbols
formal methods to support the development process. In this describes the spatial relations of traffic participants to each
paper, a formal definition of consistency for TSCs is proposed, other and the road infrastructure. This distinguishes TSCs
and its applicability in a tool-supported development process
elaborated. Experimental results with a prototypical consistency from other formal requirements specification languages such
analysis tool for TSCs are provided. as ForSeL [4] which require to express spatial constraints
textually. In contrast to other scenario specification formats,
Index Terms—Requirements engineering, Automated driving,
Formal methods, Consistency, Traffic Sequence Charts such as OpenSCENARIO [5], TSCs allow a high degree of
freedom and abstraction. Being a graphical language with an
intuitive semantics, understanding TSCs does not require deep
I. I NTRODUCTION knowledge in formal methods. Hence, a TSC can be used to
The development of a system is typically starting with a display a requirement on the behavior of the driving function to
requirement elicitation process, which aims for a complete, different stakeholders. Furthermore, TSCs have a well-defined
unambiguous and conflict-free specification of the system formal semantics that enable the use of formal methods and a
under design. For systems like highly automated vehicles wide range of tool support and automation in the development
(HAV), the specification needs to deal with a complex, open process. As such, it is possible to identify inconsistencies in
and highly dynamic context, which makes it hard to find a TSCs automatically.
appropriate and still comprehensible formalism for the spec- Safety standards such as ISO 26262 in the automotive indus-
ification. Additionally, not only system-specific requirements try define consistency as conflict-freeness of requirements. ISO
have to be handled, but also requirements that are induced 26262 distinguishes between internal consistency, meaning a
from outside. For example, the requirements for the HAV will requirement is free of contradictions within itself, and external
contain safety goals that come from hazard and risk analysis, consistency, that is a requirement does not contradict other re-
traffic regulations, and consumer needs. This makes it hard but quirements. This informal definition of consistency as conflict-
even more important to maintain requirement consistency, i.e. freeness is too vague for the application of formal methods,
to ensure that the requirements do not conflict with each other. though. Therefor two formal definitions of consistency, called
Although inconsistencies in the requirements will probably existential and partial consistency are presented in this work.
become visible during later development steps, finding them They have originally been defined and evaluated in [6], [7] for
early saves development costs [1] and avoids implementation pattern-based functional requirements. In this paper, they are
faults caused by conflicting specifications. This work focuses lifted to TSCs. In the context of TSCs, existential consistency
on requirements that describe the behavior of the HAV as is a form of internal consistency, and partial consistency –
a traffic participant, i.e. driving maneuvers by the HAV and an extension of existential consistency – a notion of external
the situations that trigger them. For that kind of requirement, consistency. The basic idea of existential consistency is to
Traffic Sequence Charts [2], [3] (TSCs for short) have been find at least one exemplary trajectory, i.e. a timed sequence
of system states, that fulfills a TSC, or show that this is
This research was partly funded by the German Federal Ministry of
Education and Research (BMBF), under grants “ASSUME” (01IS15031H) impossible. In the latter case, the TSC is called existentially
and “CrESt” (01IS16043). inconsistent. Partial consistency does something similar for

Copyright c 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
history future
a pair of TSCs. For partial consistency, possible cases are b-board
δ≥40s
identified where the TSCs are concurrently active. For each of δ

these cases it is checked whether it is possible to fulfill both left_lane
right_lane ego.v > other.v other.a <= 0
TSCs. The term partial has been chosen, because the critical ego
other

cases are found based on a heuristic (in the case of TSCs <= 50m (1) (2)
by synchronizing the start of snapshots in the different TSCs).
Missing some conflicts in a specification is acceptable because ego.v >= other.v
+ 20[km/h]
experience shows that it is more important for industrial

consequence
acceptance to not block the development process by reporting (3) (4)
spurious conflicts that need to be checked manually than
>= 50m
certifying conflict freeness [6], [8]. It is future work to extend snapshot
partial consistency so that more conflicts can be found. >= 50m
The paper is structured as follows. Section II introduces (5)
(6)
TSCs in detail. In Section III a generalized software archi-
tecture for consistency analysis of TSCs is proposed, together
Fig. 1: TSC “Overtaking”
with the two concrete consistency notions for TSCs. This also
includes a short report on our prototypical implementation of
the approach. The paper closes with a short summary and
outlook in Section IV. semantics of a TSC is as follows: Whenever the TSC’s history
held from some point in the past until now, and the TSC’s
future will hold from now till some point in the future, then
II. T RAFFIC S EQUENCE C HARTS FOR R EQUIREMENTS
also the consequence shall hold from now on. History and
Traffic Sequence Charts are a relatively new graphical future form the so-called pre-chart of a TSC. The pre-chart is
specification language for traffic scenarios. They enable a wide drawn as a bisected dashed hexagon, where the history is in the
range of applications in the development process, because left, and the future is in the right part (in Figure 1 history and
they have an intuitive, yet formal semantics. In [9], a wide future consist of single snapshots). Everything that follows the
range of applications (including the use as a requirement pre-chart in a TSC (i.e. the second and third row of Figure 1)
specification language) have already been identified. Recent is part of the consequence. The rounded rectangle in Figure 1
work [10] exploits the use of TSCs in testing. Another work is the bulletin board of the TSC and explained later.
[11] describes a discovery process for abstract scenarios – In the following, we describe the different graphical no-
represented as TSCs – that exposes the violation of a safety tations that are used in snapshots. In a snapshot, symbols
goal. In the following, the structure and semantics for TSCs is are placed to describe the spatial relations of their real-
introduced. This paper uses only a subset of the TSC language. world counterparts. For example, the snapshots (a) and (b)
For the complete language, refer to [2]. in Figure 2 specify that the ego-vehicle (the HAV under
development, white car) is on a lane, and that there exists a
A. An Overview on TSCs second lane with another vehicle (black car) on the left of ego.
The relative placement of symbols induces somewhat strict
Figure 1 shows a TSC that specifies an overtaking scenario.
constraints: Snapshot (a) is only satisfied in traffic situations
Intuitively, the TSC specifies the following behavior of the
where front and rear of the two vehicles are exactly aligned,
HAV:
snapshot (b) is satisfied only if the front of ego is strictly
Whenever you are on the right of two lanes and between front and rear of the other vehicle. Somewhere-
there is another vehicle in front of you that is nearer boxes as in snapshot (c) can be used to weaken some of the
than 50 meters and slower than you, perform the constraints. The somewhere box in snapshot (c) means that
following operations within 40 seconds, as long as there is a vehicle somewhere on the left lane, next to or in
the other vehicle stays on the right lane and does front of ego. Note that the left border of the box is aligned with
not accelerate: the left border of the ego-symbol, so the box does not match
1) Move to the left lane, accelerate until you are cars on the left lane behind ego. To this end, snapshots speak
at least 20 km/h faster than the other vehicle, only about the presence of objects at certain positions, but do
but stay behind not restrict the existence of other objects. For example, there
2) Pass the other vehicle on the left lane could be additional cars around the ego vehicle in snapshots
3) When you are at least 50 meters in front of the (a) to (c). To specify absence, nowhere-boxes are used. They
vehicle, move back to the right lane are used analogous to somewhere-boxes, but with the opposite
As mentioned shortly in the introduction, the basic building meaning. For example, the nowhere-box in snapshot (d) states
block of TSCs are the so-called snapshots, which are the that there must not be another vehicle on the left lane next to
boxes numbered (1) to (6) in Figure 1. Every snapshot de- or in front of ego. The graphical placement of symbols in a
scribes a traffic situation. Snapshots are assembled to so-called snapshot is accomplished by textual annotations. A distance
snapshot-charts. A TSC consists of three snapshot charts, line as in snapshot (5) restricts the distance between objects
the history, the future and the consequence. Informally, the and/or boxes. The distance line in snapshot (e) states that the
pedestrians, . . . ) and their attributes. Furthermore, the world
model defines their dynamics, for example in form of hybrid
automata [12]. World models can be defined on different
(a) (b) (c) (d) abstraction levels. Especially for analysis of requirements it
other.a <= 0
might be desirable to start the development process with a very
abstract world model that does not restrict the dynamics of
>= 50m
the system, and use more detailed world models in later steps.
(e) (f) As discussed later in Section III-A, a simpler world model
lowers the complexity of an analysis and allows complete
Fig. 2: Example snapshots
model-checking. During test-case generation for example, a
more exact world model is needed.
The link between the world model and a TSC is defined in
A A
A B form of a so-called symbol dictionary. The symbol dictionary
B B links the graphical symbols used in the TSCs to object classes
(a) sequence
(c) choice in the world model (in contrast to the bulletin board, which
(b) concurrency
binds symbols to certain objects). In this paper, a very simple
δ δ≤5s A B symbol dictionary is used that consists of only a symbol for
A A B C D straight lanes and a symbol for cars. The car symbol is used
(e) hour glasses
C D with different colors to distinguish the different symbols in the
(d) negation
bulletin board.
(f) time pins

Fig. 3: Snapshot chart operations B. TSC Formal Semantics
In [2], [3] the semantics of TSCs are formally defined. In
the following, we recall the semantics in a condensed form.
other vehicle is at most 50 meters behind ego. Additionally, We refer the reader to the related literature for the complete
textual constraints on the objects can be placed in a snapshot, semantics.
as shown in snapshot (f). Note that the empty snapshot is Every snapshot chart SC can be translated to a multi-sorted
always satisfied. real-time logic (MSRTL) formula ϕSC that is interpreted over
Snapshot charts combine snapshots with the operations se- some world model WM.
quence, concurrency, choice, and negation shown in Figure 3. Definition 1 (Multi-sorted Real-time Logic [2], [3]). A tra-
We use rounded rectangles (e.g. A ) as placeholders for jectory over an (ordered) set X of variables is a piece-wise
arbitrary sub-charts. A sequence of two snapshots means that continuous differentiable function π : R≥0 → RX . The term
first the first snapshot has to hold, followed by the second. π t0 denotes a trajectory π time-shifted by t0 , i.e. π t0 (t) =
The snapshots directly follow each other; there is no time π(t + t0 ).
frame between the first and the second snapshot. Concurrency A MSRTL formula ϕ over variables X is of the form
means that both snapshot (charts) have to hold simultaneously,
choice means that at least one of the charts has to hold, ϕ ::= φ | ∃t : ϕ | ¬ϕ | ϕ1 ∧ ϕ2 | ϕ1 ∨ ϕ2 | [τ1 ,τ2 ) ϕ | τ1 ∼ τ2
respectively. Negation means the chart must not hold. There where φ is a predicate over X, t a time variable,, ∼ ∈ {<, ≤
are two kinds of timing constraints in TSCs. Hour glasses }, and τ1 , τ2 are linear expressions with free time variables.
constrain the duration of a snapshot chart. A full hour glass Satisfaction of a MSRTL formula ϕ by a trajectory π and a
( ) starts a clock, and the empty hour glass ( ) specifies valuation µ that assigns values to free time variables in ϕ is
a clock constraint. Another form of timing constraints are defined as follows:
synchronization lines (dotted horizontal line in Figure 3 (f), π, µ |= φ :⇔ π(0) |= φ
also called time-pins). When two snapshots are connected by a π, µ |= [τ1 ,τ2 ) ϕ :⇔ ∀t ∈ [µ(τ1 ), µ(τ2 )) : π t |= ϕ
synchronization line, they have to start at the same time point. π, µ |= ∃t : ϕ :⇔ ∃v ∈ R≥0 : π, µ ∪ {t 7→ v} |= ϕ
The bulletin board binds symbols in the snapshots to certain π, µ |= τ1 ∼ τ2 :⇔ µ(τ1 ) ∼ µ(τ2 )
objects. A symbol that is contained in the bulletin board
refers to the same object in every snapshot. The bulletin board Boolean operators are defined as usual.
(rounded box) in Figure 1 binds the white car symbol to the We write a valuation that assigns values v1 , v2 , . . . to
ego vehicle, and the lane symbols to certain lanes of the road variables t1 , t2 , . . . as {t1 7→ v1 , t2 7→ v2 , . . . }. The term
where ego is on. Also, the black car symbol is bound to another µ ∪ {t 7→ v} denotes valuation µ extended by mapping t 7→ v.
vehicle; if the black car would not be in the bulletin board, it Note that we do not define the structure of predicates φ
could be a different vehicle in any snapshot. explicitly here. We assume that the set X in the definition
A TSC is always interpreted over some world model. As its is the union of the attributes of all the objects defined by
name suggests, the world model models the different objects the world model WM. Hence, π(t) is the state of the world
that a TSC can speak about. First of all, a world model model at time t. Accordingly, the considered predicates φ are
specifies a hierarchy of object types (e.g. obstacles, lanes, cars, expressions over the world model’s state.
Now, we are ready to define TSC semantics in terms of general architecture for a TSC consistency analysis tool. The
MSRTL. architecture is independent from a concrete consistency notion,
but takes the state of the art in the analysis of dense time and
Definition 2 (Snapshot Chart Translation). A snapshot chart
hybrid systems into account. Afterwards, based on previous
SC is translated to a MSRTL formula ϕSC with free time
work, two consistency notions for TSCs are developed that can
variables bSC and eSC that stand for begin and end of the chart
be implemented within the architecture. The section concludes
in a trajectory. In the following, [x\y] denotes substitution of
with a short evaluation based on a research prototype and the
variable x by variable y.
running example.
• If SC is a snapshot node, then ϕSC := bSC < eSC ∧
[bSC ,eSC ) φ, where φ is the translation of the snapshot
content into a predicate (see [2], [3] for the translation of A. An Architecture for TSC Analysis
snapshots). For consistency checking of formal requirements, symbolic
A model checking is the means of choice in most related work
• Concurrency: If SC = then [6]–[8], [13]–[16]. An alternative approach is the simulation
B of the requirements in order to find conflicts [17]. Because
TSCs by intention have a high degree of freedom (specifying
ϕSC := ϕA [bA \bSC , eA \eSC ] ∧ ϕB [bB \bSC , eB \eSC ]
a sequence of state invariants instead of concrete trajectories),
A simulation can only give incomplete results for TSCs. Except
• Choice: If SC = then for some case studies [18], [19], model checking (and also sim-
B ulation) has not been applied to TSCs so far. Also, decidability
ϕSC := ϕA [bA \bSC , eA \eSC ] ∨ ϕB [bB \bSC , eB \eSC ] questions for TSCs have not been elaborated, yet. However,
it is possible to transfer some results for hybrid automata and
• Negation: If SC = A then Duration Calculus (DC) [20] to TSCs.
Duration Calculus is an interval logic on dense time. Al-
ϕSC := ¬ϕA [bA \bSC , eA \eSC ] though TSCs are not intended to be an interval logic, there are
many similarities between snapshot charts and DC formulas.
• Sequence: If SC = A B then
Similar to snapshot charts, DC combines state invariants using
ϕSC := ∃t : ϕA [bA \bSC , eA \t] ∧ ϕB [bB \t, eB \eSC ] boolean connectives and a sequence operator, called chop.
Timing constraints are expressed in DC by bounding the
Note, that in the above inductive definition, the substitu- duration of state invariants. Our research prototype that is
tions [x\y] only replace free variables. The resulting MSRTL shown briefly in Section III-D uses a combination of results
formula ϕSC has exactly two free time variables bSC and eSC . from [21], [22] originally developed for DC. It translates
Definition 3 (TSC Semantics). A TSC TSC with history H, snapshot charts into Satisfiability Modulo Theories (SMT) [23]
future F , and consequence C is satisfied by some trajectory problems and reduces consistency questions to the following
π, written π |= TSC, if satisfiability problem: Given a snapshot chart SC, do a tra-
jectory π ∈ T (WM) and time point e ∈ R≥0 exist such
∀b, m, e ∈ R≥0 : π, {bH 7→ b, eH 7→ m, bF 7→ m, that π, {bSC 7→ 0, eSC 7→ e} |= ϕSC ? Here and in the rest
eF 7→ e, bC 7→ m, eC 7→ e} |= ¬(ϕH ∧ ϕF ) ∨ ϕC . of the paper, T (WM) refers to all the trajectories possible
within a world model WM. Unfortunately, the translation to
Note that the original work [2], [3] defines a more expres- SMT problems based on [21], [22] does not allow dynamics
sive MSRTL. Furthermore, [2], [3] defines the translation of in the world model or negated sequences in the snapshot chart,
timing constraints and synchronization (time pins). except for some special cases.
Example 1. The consequence C of the TSC in Figure 1 is We see advantages in reducing consistency of TSCs to
translated to the MSRTL formula satisfiability of snapshot charts without negated sequences as
above also for other model-checking approaches. For example,
ϕC := ∃t1 , t2 , t3 : bC < t1 < t2 < eC in [24] a translation from a subset of DC into hybrid automata
∧ [bC ,t1 ) φ3 ∧ [t1 ,t2 ) φ4 ∧ t2 ,t3 ) φ5 [t3 ,eC ) φ6 is presented. Related work [25] gives a translation from
negation-free DC into timed regular expressions, which in
where φ3 , . . . , φ6 are the predicates derived from snapshots turn are expressible as timed automata. So we are optimistic
(3)–(6). that it is possible to define similar translations from negation-
free snapshot charts into hybrid automata. This reduces the
III. PARTIAL C ONSISTENCY FOR TSC S satisfiability problem of snapshots charts to reachability in
A lot of previous work has been done that lead to formal hybrid automata, and allows also to use a network of hybrid
definitions of requirement consistency. When lifting existing automata as a world model. A wide range of model-checking
formal consistency notions to TSCs, care must be taken that tools for hybrid automata already exists, for example [26]–[29]
they can be applied in practice. In order to integrate formal to mention a few.
methods in a development process, easy to use tool support With this considerations on model checking, we propose
is essential. In the following, we start with proposing a the layered architecture depicted in Figure 4. As an input, the
World Model WM + TSCs TSC1 , . . . , TSCn The authors of [6], [8] define consistency as follows: A set
of requirements is consistent, if there exists at least one trajec-
Derive Snapshot Charts SC1 , . . . , SCm and satisfaction problems tory that satisfies all the requirements in the set. This is called
∃πi ∈ T (WM), ei ∈ R≥0 : πi , {bSCi 7→ 0, eSCi 7→ ei } |= ϕSCi
existential consistency in [6]. Lifting existential consistency
Translate to model checking problem to TSCs means the following: A set of TSCs is existentially
for each SCi consistent, if there exists at least one trajectory that satisfies
Call backend model checker/solver all the TSCs. In the following, we restrict ourselves to a set
consisting of a single TSC and consider the case of multiple
Extract consistency result
TSCs later. By Definition 3, a trajectory satisfies a TSC if,
Trace source of (in)consistencies back to TSCs
for any time points b < m < e where the history holds from
b to m and the future holds from m to e, the consequence
Fig. 4: Architecture for a consistency analysis holds from t to e. This is problematic for two reasons: On the
one hand, the property is difficult to check, because there are
typically infinitely many triples (b, t, e) on a trajectory where
analysis takes a set of TSCs and a world model definition. The history and future hold. On the other hand, we may choose
input is translated into a set SC1 , . . . , SCn of snapshot charts a trajectory for witness, where history and future are never
and satisfaction problems of the form satisfied at all, in which case the consistency argument is not
of practical use. The authors of [6], [8] had to deal at least
∃πi ∈ T (WM), ei ∈ R≥0 : πi , {bSCi 7→ 0, eSCi 7→ ei } |= ϕSCi with the second problem. They solved this by requiring that
the premise of the requirements shall be satisfied at least once
for i = 1, . . . , n. This and the following steps are independent
on the witness trajectory. When speaking about TSCs, this
from the concrete consistency notion—the consistency notions
means that we search for a trajectory π ∈ T (WM) where the
defined in Sections III-B and III-C are only one possibility.
history occurs, directly followed by the future. Formally
The satisfaction problems are translated into an intermediate
representation that is input for a model checking tool or
∃b, m, e ∈ R≥0 : π, {bH 7→ b, eH 7→ m, bF 7→ m, eF 7→ e}
a solver. In our research prototype, this is a translation to
an SMT problem in the SMT-Lib format [30], but other |= 0 < b < m < e ∧ ϕH ∧ ϕF (1)
formats, e.g. a network of hybrid automata, are also possible. where H and F are history and future of the TSC. The
The problem descriptions are fed into a model checker or inequality 0 < b in that formula allows us to prefix the
solver backend. Finally, a consistency result is extracted from sequence of H and F with an empty snapshot and to encode
the model checker/solver results, and presented to the user.
In many cases, the model checking tools give additional it as a single chart HF = H F . Because of the empty
information on a result, that can be used to identify the cause snapshot, we can fix the start of HF to 0, while the sub-chart
of an inconsistency, or give a witness for consistency. H still starts at a time point bH > 0. Because a snapshot by
definition has a non-zero duration, bH = 0 is excluded. As a
result we can rewrite (1) as
B. Existential Consistency
∃e ∈ R≥0 : π, {bHF 7→ 0, eHF 7→ e} |= ϕHF (2)
We propose a notion for consitency of TSCs based on
previous work for pattern-based requirements [6]–[8] due to As a consistency argument, we would like to see that it is
the following reasons: at least possible to satisfy the consequence C of the TSC in
• The considered pattern languages define the semantics of parallel to the future. This brings us to our first consistency
requirements in terms of unbounded trajectories (system notion for TSCs that we call existential consistency for TSCs.
runs) Definition 4 (Existential Consistency). A TSC with history
• They allow “don’t care”s in the requirements
H, future F , and consequence C is existential consistent wrt.
• The considered requirements are structured in a
the world model WM if there exists a trajectory π ∈ T (WM)
premise/consequence scheme such that
Here, “don’t care” means that a requirement only restricts
some variables of the system, and even these restrictions may ∃e ∈ R≥0 : π, {bHFC 7→ 0, eHFC 7→ e} |= ϕHFC (3)
allow a high degree of freedom. For example, a TSC typically
with the snapshot chart
specifies the behavior of traffic participants in terms of distance
intervals. Within the interval, any behavior is valid. Also,
F
the TSCs that are considered in this paper consist of two HFC = H .
parts: the pre-chart (history and future) and the consequence. C
On any sub-trajectory, where the history is followed by the
future, the consequence must hold in parallel to the future. The Fact 1. Assume some TSC TSC with history H, future F
requirements tackled in [6]–[8] are structured similar: They and consequence C that is interpreted over some world model
specify some consequence (called action in [6], [7]) that shall WM. A trajectory π ∈ T (WM) that satisfies both π |= TSC
occur in response to some premise (called trigger in [6], [7]). and equation (2), also satisfies equation (3).
This fact follows with some basic algebra from Definitions 1 the following implication holds for every snapshot sn in the
to 3. The consequence of the fact is that existential consistency consequence C1 of the first TSC:
does not produce false warnings, in the sense that if a
(∃π1 ∈T (WM), e1 ∈R≥0 :π1 , {bSC1 7→0, eSC1 7→e1 }|=ϕSC1 )
TSC is existentially inconsistent, then it is indeed impossible
within the world model to find a trajectory that both satisfies ⇒(∃π2 ∈T (WM), e2 ∈R≥0 :π2 , {bSC2 7→0, eSC2 7→e2 }|=ϕSC2 )
the TSC and where history and future occur. Note that the with the snapshot charts
opposite is not true. A trajectory that satisfies equation (3) does
not necessarily satisfy the TSC. However, using this under-
approximation of a satisfying trajectory we get rid of the all- F1
F1 H1
quantifier in the formal definition of satisfaction of a trajectory H1 C1sn
by a TSC. Also, we can restrict ourselves to search for a prefix C1sn
SCsn
1 = SCsn
2 =
of a trajectory, instead of a complete trajectory, which would
F2
require some kind of unbounded model checking techniques H2 F2 H2
in a consistency analysis. C2

where Hi , Fi and Ci are history, future and consequence of
C. From Existential to Partial Consistency
TSCi (i ∈ {1, 2}). The snapshot chart C1sn is derived from
Existential consistency as defined in the last section does C1 by removing all branches of choice operations that bypass
not give meaningful results for sets of TSCs in most cases. If sn.1 In both SCsn sn
1 and SC2 , the start of F2 is synchronized
we build the conjunction of equation (3) over multiple TSCs, with the start of sn in C1sn . Removing some choices from C1
e.g. searching for a trajectory π ∈ T (WM) that satisfies is necessary because it is neither allowed in TSCs nor makes
n
sense to synchronize sub-charts if one of them is part of a
^ choice.
∃ve ∈R≥0 :π, {b7→0, e7→ve }|= ϕHFCi [bHFCi \b, eHFCi \e]
i=1 Example 2. Consider the TSCs from Figure 1 and Figure 5.
The latter says, that the ego vehicle must stay on the right lane
with
and must not accelerate, as long as there is another vehicle
Fi on the left lane, near ego. They are partially inconsistent.
HFCi = Hi , Intuitively, the conflict arises when the ego vehicle approaches
Ci another car while a third vehicle is on the left lane. The
first TSC says ego shall overtake, while the second says ego
we end up in most cases with a trajectory where the futures of must keep right. The partial consistency check for these two
the different TSCs do not overlap. The result is not different TSCs consists of five cases (four cases where the future of the
than checking existential consistency of each TSC separately. second TSC is synchronized with one of the snapshots (3)–(6)
In practice, the future of a TSC usually speaks about some from the first TSC’s consequence, and one where the future
behavior of the environment that is not under control of the ego of the first TSC is synchronized with the consequence of the
vehicle. At least it is not the intended strategy for a controller second). The case where the future of the TSC in Figure 5
to satisfy its specification by forcing a violation of history is synchronized with snapshot (4) from the TSC in Figure 1
or future of the TSCs in the specification. As a consequence, reveals the inconsistency. The consequence SC42 of that case is
a consistency analysis is needed that considers the possible shown in Figure 6. The premise SC41 for that case is identical
overlappings between history and/or future of different TSCs. to SC42 , except that the snapshot (7) is omitted. The premise
Therefor we develop a second consistency notion that is called SC41 is satisfiable, which means it is possible to satisfy all parts
partial consistency for TSCs. It is inspired by the partial of the first TSC (Figure 1) while the future of the second TSC
consistency for pattern-based requirements defined in [7]. The (snapshot (7) in Figure 5) starts together with snapshot (4)
basic ideas are the following: from the first TSC. An example of a satisfying trajectory is
1) Consider pairs of TSCs. depicted in Figure 7 as a sequence of snapshots. However,
2) For every pair, determine the possible ways how the the consequence SC42 is not satisfiable, which means it is
futures of the two TSCs can overlap. We consider cases not possible to find such a trajectory that also satisfies the
where the future of the second TSC starts during the consequence of the second TSC. In SC42 , snapshots (4) and
consequence of the first one. (8) must be fulfilled concurrently, but are clearly conflicting:
3) For every possible overlapping, check if it is possible to In (4), ego is on the left lane, while in (8) it is on the right
satisfy both consequences. lane.
Obviously, not all inconsistencies within a set of TSCs can The case construction for partial consistency of two TSCs
be reduced to conflicts between pairs, therefor a possible can be generalized to three TSCs by combining SCsn sn
1 and SC2
generalization is briefly sketched at the end of this section.
a
Definition 5 (Partial Consistency). A pair TSC1 , TSC2 of 1 For example, if C
1 = c then C1a = a c and C1b =
b
TSCs is partially consistent wrt. some world model WM if b c and C1c = C1 .
as possible, consistency of TSCs can be checked on different
<= 50m abstraction levels. The consistency notions defined here are
left_lane
ego.a <= 0 independent from a concrete world model. The examples
right_lane
ego
presented in this paper show that an analysis implementation
(8)
(7) that abstracts from any differential equations in a hybrid world
model already gives meaningful consistency results and finds
conflicts in a specification. Performing consistency analysis on
Fig. 5: A TSC that prohibits lane changes and accelleration
an abstract world model is not only caused by the limitations
while there is another vehicle around ego. Note the overlapping
of current model checkers, but also driven by the fact that
somewhere-boxes.
detailed world models may not be present in early development
phases, where a consistency analysis is typically performed.
Nonetheless our first experiments with the consistency analysis
F3
H3 showed that a consistency analysis on an abstract level cannot
with a chart derived from a third TSC, and
C3 find all the conflicts in a specification. In the running example
(see Figure 1), it might be impossible for the ego vehicle to
synchronizing the start of F1 in SCsn sn
1 (resp. SC2 ) with one accelerate and to be at least 20km/h faster before passing the
snapshot from C3 , or synchronizing F3 with a snapshot from other vehicle. This conflict is not found because it depends
C1sn . This way, the consistency cases for a group of n TSCs both on the vehicle speeds at the beginning of the scenario and
can inductively be derived from the cases for n − 1 TSCs. the possible vehicle dynamics in the world model. Therefore
future research directions are to (1) find more sophisticated
D. Prototypical Implementation consistency notions that find more conflicts even on a high
We evaluated the above consistency notions in a prototypical abstract level (2) investigate into analysis methods for hybrid
implementation that has been partially already described in systems and how they can be used for consistency analysis of
Section III-A. The consistency analysis uses the Z3 SMT TSCs.
solver [31] in version 4.6.0. For the existential and partial
consistency analysis, a translation from snapshot charts to R EFERENCES
SMT is used that is based on a combination of results from
[21], [22]. The layered architecture described in Section III-A [1] P. Feiler, L. Wrage, and J. Hansson, “System architecture virtual
made it easy to implement both consistency notions and a integration: A case study,” in Embedded Real-time Software and Systems
Conference, 2010.
few similar ones using a common analysis code base. The [2] W. Damm, S. Kemper, E. Möhlmann, T. Peikenkamp, and A. Rakow,
prototype needs less than 12 seconds to analyze the partial “Traffic sequence charts - from visualization to semantics,” SFB/TR 14
consistency from Example 2 running on a Windows 7 desktop AVACS, Reports of SFB/TR 14 AVACS 117, 10 2017.
[3] W. Damm, E. Möhlmann, T. Peikenkamp, and A. Rakow, A Formal
PC with an Intel Core i5-2400 CPU @ 3.1 GHz and 4GB Semantics for Traffic Sequence Charts. Cham: Springer International
RAM2 . The translation procedure derived from [21], [22] Publishing, 2018, pp. 182–205.
cannot handle differential equations currently, and does not [4] J. Hartmann, S. Rittmann, D. Wild, and P. Scholz, “Formal incremen-
tal requirements specification of service-oriented automotive software
distinguish between continuous and discrete variables. systems,” in 2006 Second IEEE International Symposium on Service-
Oriented System Engineering (SOSE’06). IEEE, 2006, pp. 130–133.
IV. C ONCLUSION & F UTURE W ORK [5] VIRES Simulationstechnologie GmbH, “OpenSCENARIO,” online,
2018, last visited on 2019-07-01. [Online]. Available:
In this paper, two formal consistency notions for TSCs http://openscenario.org
have been presented. Beneath TSCs, a bunch of other scenario [6] C. Ellen, S. Sieverding, and H. Hungar, “Detecting consistencies and
inconsistencies of pattern-based functional requirements,” in Formal
specification languages exist [32]–[34], the most popular one is Methods for Industrial Critical Systems, FMICS 2014, Proceedings, ser.
probably the standardized exchange format OpenSCENARIO LNCS, vol. 8718. Springer, 2014, pp. 155–169.
[5]. In contrast to other approaches, TSCs are both a graphical [7] J. S. Becker, “Analyzing consistency of formal requirements,” in 18th
International Workshop on Automated Verification of Critical Systems,
language and have a well-defined formal semantics. A TSCs 2018.
define scenarios in an abstract way, i.e. one TSC captures [8] P. Filipovikj, G. Rodriguez-Navas, M. Nyberg, and C. Seceleanu,
infinitely many concrete scenarios. Therefor, TSCs are suitable “SMT-based consistency analysis of industrial systems requirements,”
in Proceedings of the Symposium on Applied Computing. ACM, 2017,
as a requirement specification language for HAV. By providing pp. 1272–1279.
formal consistency notions for TSCs, this work is a first step [9] W. Damm, S. Kemper, E. Möhlmann, T. Peikenkamp, and A. Rakow,
towards tool supported formal methods for requirements engi- “Traffic sequence charts: A visual language for capturing traffic sce-
narios,” in Embedded Real Time Software and Systems - ERTS2018,
neering with TSCs. In [19] a somewhat simpler form of TSCs February 2018.
are used to generate concrete scenarios for testing. The authors [10] W. Damm, E. Möhlmann, and A. Rakow, “Traffic sequence charts for the
of [19] observe that solving constraint systems for abstract sce- ENABLE-S3 test architecture,” in Validation & Verification of Automated
narios in a hybrid world model is a challenging task, even for Systems – Results of the ENABLE-S3 Project, 2019.
[11] ——, “A scenario discovery process based on traffic sequence charts,”
simple scenarios. In contrast to test case generation, where the in Validation & Verification of Automated Systems – Results of the
concrete scenarios need to be as close to real world behavior ENABLE-S3 Project, 2019.
[12] R. Alur, C. Courcoubetis, T. A. Henzinger, and P.-H. Ho, “Hybrid
2 The SMT scripts for the example are provided for download under https: automata: An algorithmic approach to the specification and verification
//vhome.offis.de/jbecker/ase2020.zip of hybrid systems,” in Hybrid systems. Springer, 1992, pp. 209–229.
δ δ≥40s

other.a <= 0

ego.v > other.v (2)

<= 50m >= 50m
(1)
ego.v >= other.v
+ 20[km/h]
>= 50m
(3) (4) (6)
(5)

<= 50m

(7)

ego.a <= 0

(8)

Fig. 6: Consequence (SC2 ) for the partial inconsistency

(1) (2)+(3)+(7) (2)+(4)+(7) [21] M. Fränzle and M. R. Hansen, “Deciding an interval logic with accumu-
10m lated durations,” in International Conference on Tools and Algorithms
for the Construction and Analysis of Systems, ser. LNCS, vol. 4424.
Springer, 2007, pp. 201–215.
50m [22] B. Sharma, P. K. Pandya, and S. Chakraborty, “Bounded validity
checking of interval duration logic.” in TACAS, vol. 5. Springer, 2005,
pp. 301–316.
[23] C. W. Barrett, R. Sebastiani, S. A. Seshia, and C. Tinelli, “Satisfiability
(2)+(5)+(7) (2)+(6)+(7) modulo theories.” Handbook of satisfiability, vol. 185, pp. 825–885,
2009.
50m [24] A. Bouajjani, Y. Lakhnech, and R. Robbana, “From duration calculus
to linear hybrid automata.” in LNCS, vol. 939, 07 1995, pp. 196–210.
60m
[25] M. Fränzle, “Model-checking dense-time duration calculus,” Formal
Asp. Comput., vol. 16, no. 2, pp. 121–139, 2004.
[26] T. A. Henzinger, P.-H. Ho, and H. Wong-Toi, “Hytech: A model
checker for hybrid systems,” International Journal on Software Tools
Fig. 7: Illustration of a trajectory that satisfies SC1 . The for Technology Transfer, vol. 1, no. 1-2, pp. 110–122, 1997.
numbers above the snapshots show which snapshot nodes from [27] G. Frehse, C. Le Guernic, A. Donzé, S. Cotton, R. Ray, O. Lebeltel,
R. Ripado, A. Girard, T. Dang, and O. Maler, “SpaceEx: Scalable ver-
Figure 6 are satisfied in each step. ification of hybrid systems,” in International Conference on Computer
Aided Verification. Springer, 2011, pp. 379–395.
[28] A. Eggers, N. Ramdani, N. Nedialkov, and M. Fränzle, “Improving SAT
[13] A. Post, I. Menzel, J. Hoenicke, and A. Podelski, “Automotive behavioral modulo ODE for hybrid systems analysis by combining different enclo-
requirements expressed in a specification pattern system: a case study at sure methods,” in International Conference on Software Engineering and
BOSCH,” Requirements Engineering, vol. 17, no. 1, pp. 19–33, 2012. Formal Methods. Springer, 2011, pp. 172–187.
[14] A. Post, J. Hoenicke, and A. Podelski, “rt-inconsistency: A new property [29] E. Althaus, B. Beber, W. Damm, S. Disch, W. Hagemann, A. Rakow,
for real-time requirements,” in Fundamental Approaches to Software C. Scholl, U. Waldmann, and B. Wirtz, “Verification of linear hybrid
Engineering - 14th International Conference, FASE 2011. Proceedings, systems with large discrete state spaces using counterexample-guided
2011, pp. 34–49. abstraction refinement,” Science of Computer Programming, vol. 148,
[15] T. Bienmüller, T. Teige, A. Eggers, and M. Stasch, “Modeling re- pp. 123–160, 2017.
quirements for quantitative consistency analysis and automatic test case [30] D. R. Cok, The SMT-LIBv2 Language and Tools: A Tutorial,
generation,” in FM&MDD 2016, ser. Computing Science Technical 1st ed., 11 2013. [Online]. Available: http://smtlib.github.io/jSMTLIB/
Report Series, vol. CS-TR-1503. Newcastle University, 2016. SMTLIBTutorial.pdf
[16] B. K. Aichernig, K. Hörmaier, F. Lorber, D. Ničković, and S. Tiran, [31] L. de Moura and N. Bjørner, “Z3: An efficient SMT solver,” in Tools
“Require, test and trace IT,” in Formal Methods for Industrial Critical and Algorithms for the Construction and Analysis of Systems: 14th
Systems - 20th International Workshop, FMICS 2015, Proceedings, ser. International Conference, TACAS 2008. Proceedings. Springer, 2008,
LNCS, vol. 9128. Springer, 2015, pp. 113–127. pp. 337–340.
[17] B. Jeannet and F. Gaucher, “Debugging embedded systems requirements [32] P. Suresh and R. Mourant, “A tile manager for deploying scenarios in
with STIMULUS: an automotive case-study,” in 8th European Congress virtual driving environments,” in Driving Simulation Conference, 2005,
on Embedded Real Time Software and Systems (ERTS 2016), 2016. pp. 21–29.
[18] S. Gerwinn, E. Möhlmann, and A. Sieper, “Statistical model checking [33] I. H. C. Wassink, E. M. A. G. van Dijk, J. Zwiers, A. Nijholt, J. Kuipers,
for scenario-based verification of ADAS,” in Control Strategies for Ad- and A. O. Brugman, Bringing Hollywood to the Driving School:
vanced Driver Assistance Systems and Autonomous Driving Functions. Dynamic Scenario Generation in Simulations and Games. Springer,
Springer, 2019, pp. 67–87. 2005, pp. 288–292.
[19] A. Eggers, M. Stasch, T. Teige, T. Bienmüller, and U. Brockmeyer, [34] J. Kearney, P. Willemsen, S. Donikian, and F. Devillers, “Sce-
“Constraint systems from traffic scenarios for the validation of au- nario languages for driving simulation,” in Driving Simulation
tonomous driving,” in Third International Workshop on Satisfiability Conference, DSC’99, 1999, pp. 377–393, [Online]. Available:
Checking and Symbolic Computation, Part of FLOC 2018, 2018. www.cs.uiowa.edu/ kearney/pubs/dsc99 kearney.pdf.
[20] Z. Chaochen, C. Hoare, and A. Ravn, “A calculus of durations,”
Information Processing Letters, vol. 40, pp. 269–276, 12 1991.