From Simulation to Verification: A Flexible Interface for Scenario Description in Autoware Autonomous Driving Ecosystem

Autoware, a real-world autonomous driving platform, lacks a flexible scenario description mechanism. A prior study [1] introduced the first runtime verification framework for Autoware, integrating AWSIM-Script—a domain-specific language (DSL) for describing traffic scenarios in AWSIM-Labs—with AW-Checker, a temporal-logic-based model checker applied to simulation-generated execution traces. This framework represents the only practical verification tool currently available for Autoware, since traditional formal verification techniques are infeasible for large, industrial-scale ADSs. With this framework, scenarios written in AWSIM-Script are executed in AWSIM-Labs, traces are collected, and offline verification is performed using AW-Checker. However, AWSIM-Script imposes two major limitations. First, because the language is embedded within AWSIM-Labs and offers only a small set of predefined behaviors (e.g., lane following and lane change), extending it requires modifying the language grammar and recompiling the simulator. The tasks are effort-consuming and demand specialized technical expertise. Second, it supports only simple event triggers based on time or distance, and lacks the expressiveness needed for richer state-based triggers, such as “the car starts moving when the ego vehicle’s speed exceeds 10 km/h.”

To address these limitations and to enhance the verification capability of the existing framework, this paper presents AWSIM-ScriptPy, a Python-based client library that replaces the rigid grammar of AWSIM-Script with a flexible, programmable scenario interface. AWSIM-ScriptPy adopts a client–simulator architecture, in which AWSIM-Labs acts as a simulation server while scenario descriptions and control logic are executed on the client side. Users can compose complex behaviors using modular actions, define custom state-based triggers, and dynamically interact with the simulator without recompilation. This design allows the introduction of new behaviors entirely through the client-side, simplifying scenario experimentation. Python was chosen for its user-friendly syntax and ease of use, allowing users to describe behaviors and conditions with minimal technical overhead. In addition to enabling the description and execution of highly complex scenarios, AWSIM-ScriptPy allows post- simulation verification based on AW-Checker [1], enabling users to generate traces that can be formally analyzed using temporal logic specifications. This strengthens the tool’s role within a broader “simulation-to-verification” pipeline for ADSs.

Overview

The figure at the top page gives an overview of AWSIM-ScriptPy and its integration with the post-simulation verification workflow using AW-CheckerPy, a Python wrapper for AW-Checker [1]. The blue blocks represent the new components introduced in this work, whereas the gray blocks indicate components employed from prior studies. AWSIM-ScriptPy comprises client components implemented in Python and a server-side interface integrated into AWSIM-Labs. The client components provide a lightweight, user-friendly framework for describing scenarios, while the server-side interface handles requests from the client and communicates with the simulator’s internal components to perform corresponding actions.

This client–server separation mechanism allows scenario specifiers to focus entirely on writing high-level scenario logic in Python, without needing in-depth knowledge of simulator internals. As a result, AWSIM-SCRIPTPY makes it possible to quickly prototype, execute, and evaluate AD scenarios in AWSIM-Labs with minimal development effort. Execution traces can be obtained after scenario simulation using a runtime monitor [1]. With these execution traces, post- simulation verification of desired properties can be conducted using AW-CheckerPy.

The language usage, some example scenarios, and demonstrations are available in this GitHub repository: https://github.com/fomaad/AWSIM-ScriptPy.

Reference

[1] Safety Analysis of Autonomous Driving Systems: A Simulation-based Runtime Verification Approach. Duong Dinh Tran, Takashi Tomita, and Toshiaki Aoki. IEEE Transactions on Reliability, 2025.

Publications

From Simulation to Verification: A Flexible Interface for Scenario Description in Autoware Autonomous Driving Ecosystem. Duong Dinh Tran, Peter Riviere, Takashi Tomita, and Toshiaki Aoki. In the 50th IEEE International Conference on Computers, Software, and Applications, COMPSAC 2026 (to appear), 2026