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. Mö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. Mö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. Mö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. Mö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. Frä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. Frä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. Donzé, 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. Frä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. Bienmü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. Hörmaier, F. Lorber, D. Ničković, 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. Mö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. Bienmü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.