A Consistency Analysis Method for Traffic Sequence Charts

Kurzfassung

Increasing vehicle automation requires new methods for developing and verifying highly automated driving systems, as traditional approaches cannot cover the diversity of traffic situations and environmental conditions. This thesis addresses scenario-based development using Traffic Sequence Charts (TSCs), a formal language for specifying abstract traffic scenarios graphically. The work focuses on the consistency problem for TSCs, i.e., detecting contradictions within and between scenario-based requirements. First, formal definitions of consistency for TSCs are introduced and analyzed. Starting with ideal notions of consistency, weaker approximations are developed and formally related. Secondly, an automated consistency analysis is presented that translates the weaker notions into decidable satisfiability modulo theories problems. The proposed techniques are evaluated in case studies showcasing practical applicability and scalability.