Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Consistency Analysis Method for Traffic Sequence Charts

Jan Steffen Becker

TL;DR

The proposed method utilizes satisfiability modulo theories solving on two-sided approximations of possible vehicle behavior to ensure that found inconsistencies are not caused by approximations, but also occur when applying exact methods.

Abstract

The trend in the development of highly automated vehicles goes towards scenario-based methods. Traffic Sequence Charts are a visual but yet formal language for describing scenario-based requirements on highly automated vehicles. This work presents an approach for finding inconsistencies (conflicts) in a set of scenario-based requirements formalized with Traffic Sequence Charts. The proposed method utilizes satisfiability modulo theories solving on two-sided approximations of possible vehicle behavior. This ensures that found inconsistencies are not caused by approximations, but also occur when applying exact methods. Applicability and scalability of the analysis technique is evaluated in a case study.

A Consistency Analysis Method for Traffic Sequence Charts

TL;DR

The proposed method utilizes satisfiability modulo theories solving on two-sided approximations of possible vehicle behavior to ensure that found inconsistencies are not caused by approximations, but also occur when applying exact methods.

Abstract

The trend in the development of highly automated vehicles goes towards scenario-based methods. Traffic Sequence Charts are a visual but yet formal language for describing scenario-based requirements on highly automated vehicles. This work presents an approach for finding inconsistencies (conflicts) in a set of scenario-based requirements formalized with Traffic Sequence Charts. The proposed method utilizes satisfiability modulo theories solving on two-sided approximations of possible vehicle behavior. This ensures that found inconsistencies are not caused by approximations, but also occur when applying exact methods. Applicability and scalability of the analysis technique is evaluated in a case study.
Paper Structure (18 sections, 14 equations, 9 figures, 1 table, 1 algorithm)

This paper contains 18 sections, 14 equations, 9 figures, 1 table, 1 algorithm.

Table of Contents

  1. Introduction
  2. Research Problem and Objectives
  3. State of Practice
  4. Traffic Sequence Charts
  5. Interpretation of Spatial Views
  6. Chart Semantics
  7. Use Case World Model
  8. Satisfiability Modulo Theories and Bounded Model Checking
  9. Methodology and Expected Results
  10. State of Work
  11. Defining Consistency
  12. Semi-deciding Satisfiability of Basic Charts
  13. Encoding the Chart Structure
  14. Sufficient Conditions for Invariants
  15. Necessary Conditions for Invariants
  16. ...and 3 more sections

Figures (9)

  • Figure 1: A TSC and its parts. The bulletin-board declares object symbols with global scope in the TSC; the pre-chart is a triggering condition for the TSC, where history describes past behavior; the consequence is the requirement obligation that shall be maintained during the future behavior.
  • Figure 2: Syntax of basic charts
  • Figure 3: Spatial views from Example \ref{['ex:sv-semantics']}
  • Figure 4: Symbol dictionary for the running examples
  • Figure 5: The world model that is used in the use case. Each box represents an object type, arrows denote inheritance
  • ...and 4 more figures

Theorems & Definitions (8)

  • Example 1
  • Definition 1
  • Definition 2
  • Example 2
  • Definition 3
  • Example 3
  • Example 4
  • Example 5