Large-scale scenario databases may contain hundreds of thousands of scenarios for the verification and validation (V&V) of autonomous vehicles (AV). Scenarios in the database are often labelled with semantic Operational Design Domain (ODD) tags (e.g., WeatherRainy, RoadTypeHighway and ActorTypeTruck) to be queried via exact tag matching. Such a scenario database design has two major limitations, i.e. combinatorial scenario generation inevitably leads to many redundant scenarios, and each ODD query matches only a small number of scenarios in the database (0.2% in our case study), rendering most of the database wealth wasted. We propose a novel scenario database design and the first ODD-based query-time scenario mutation framework to address the limitations. Our case study results show that the proposed framework has the potential to fully utilize all the database scenarios at query time while eliminating scenario redundancy in the database (in our case study, given the same ODD query, the number of final matched scenarios increased by 36 times, diversity increased by 99 times, and scenario database utilization rate increased from 0.2% to 36%).

Scenario-based testing for automated driving systems (ADS) is an industry norm for safety assurance. A scenario describes situations that an automated driving systems may encounter during its operation. To ensure accurate representation of real-world situations, including human behavior and system interactions, a formal language is essential. It ensures consistent testing across diverse scenarios and facilitates compatibility with simulation tools. However, while existing scenario languages excel in describing environmental and road structure aspects, they lack the same detail for road users and drivers. We have developed a methodology to identify and incorporate relevant human factors elements into scenario languages. Our methodology focuses on understanding diverse individuals and their interactions with ADS on the road, enabling their representation in scenarios. We offer practical examples to improve language representation of human elements and actions, in WMG-SDL Level-2 for logical scenarios and BSI Flex 1889 for abstract scenario descriptions. This methodology serves as a starting point for language designers to accurately represent all road users and their interactions with ADS.

Scenario-based verification and validation (V&V) has emerged as the predominant approach for the performance evaluation of automated driving systems (ADSs). Many scenario-generation methods have been proposed to search for critical scenarios, i.e. disengagement or traffic rule violations. However, the widely adopted binary (pass/fail) criterion suffers from two main limitations, i.e., the difficulty of locating root causes and the lack of statistical guarantee of testing sufficiency. Recently, new scenario engineering approaches focusing on the intelligence of ADSs enlightened a promising pathway via dynamic driving task decomposition and function atom constraints. However, none of the state-of-the-art scenario description languages support such approaches. To fill this gap and facilitate further research into this promising direction, in this work, we propose a generic architecture to extend the existing scenario description languages for the intelligence testing of ADSs. The case study with WMG SDL demonstrates the capability and flexibility of the proposed extension design in defining intelligence function constraints.

Automated Driving Systems (ADSs), like human drivers, must be compliant with the rules of the road. However, current rules of the road are not well defined. They use inconsistent and ambiguous language. As a result, they are not sufficiently formal for machine interpretability, a necessity for applications of verification and validation (V&V) of ADSs. Rules must be defined in a way that make them usable to a variety of stakeholders. While first-order and temporal logic forms of rules of the road are needed for monitoring and verification during simulation and testing, a structured natural language for these rules is necessary for consistent definition. They must also adhering to standard vocabulary taxonomies of Operational Design Domain (ODD) and behaviour. This paper contributes a structured natural language based on formal logic, that allows rules of the road to be defined in a natural, yet precise manner, using concepts of ODD and behaviour, making them usable in the V&V of ADSs. We evaluate the effectiveness of the language on a selection of rules from the Vienna Convention on Road Traffic and the UK Highway Code.

The move towards connected and autonomous vehicles (CAVs) has gained a strong focus in recent years due to the many benefits they provide. While the autonomous aspect has seen substantial advancement in both the development and testing methodologies, the connected aspect has lagged behind, especially in the verification and validation (V&V) discussions. Integrating connectivity into the development and testing framework for CAVs is a necessity for ensuring the early deployment of cooperative driving systems. A key element within such a framework is a test scenario, which represents a set of scenery, environmental conditions, and dynamic conditions, that a system needs to be tested in. However, the connectivity element is not present in any of the current state of the art scenario description languages (SDLs) that are publicly available. This leaves a gap within the CAV development ecosystem. To accommodate for, and accelerate the development of, connected vehicle systems and their verification and validation methods, this paper proposes a novel V2X extension to the previously published two-level abstraction SDL. The extension enables communications between vehicles, infrastructures, and further additional entities to be specified as part of the scenario and be subsequently tested in virtual testing or real-world testing. Eight new V2X attributes have been added to the SDL. An example set of syntax and semantic definitions are presented in this paper targeting two different abstraction levels – level 1 aims at the abstract scenario level for non-technical end-users such as regulators, and level 2 aims at the logical and concrete scenario level for end-users such as simulation test engineers.

For Automated Driving Systems (ADSs), vehicle safety and functional correctness are assessed against scenarios the ADS would encounter - within or outside its operational design domain (ODD). A scenario specifies conditions and events that an ADS is expected to respond to when deployed. Scenario specifications underpin the verification and validation (V&V) life-cycle, and are used by a diverse set of stakeholders - from engineers to regulators. Due to the diversity in stakeholder expertise, scenarios must be available at different levels of detail. Further, the chance of writing syntactically or semantically incorrect scenarios is high. Due to the high reliance of V&V on scenarios, their correctness is crucial. Therefore, present-day scenario-description languages (SDLs) need to be supported by technologies to help authors compose scenarios and provide a mechanism for easy translation into executable forms for virtual or real-life testing. This paper addresses these issues by building on the existing two-level abstraction WMG-SDL in the following ways, (1) introducing a human-readable, natural language SDL, replacing the former Level-1 SDL, and complementing the more detailed Level-2 SDL, which is now syntax aligned with the ODD Taxonomy defined in ISO 34503, and (2) providing a tool consisting of a parser and a validator to assist writing syntactically and semantically correct scenarios. Our tool may be used within a graphical scenario editing interface or on the command-line. Further, for developers, an object-oriented interface for parsed scenarios enables further development and integration with off-the-shelf ADS simulation and language tools. The tools and technologies described in this paper are to be made open-source.

We aim to mine temporal causal sequences that explain observed events (consequents) in time-series traces. Causal explanations of key events in a time-series have applications in design debugging, anomaly detection, planning, root-cause analysis and many more. We make use of decision trees and interval arithmetic to mine sequences that explain defining events in the time-series. We propose modified decision tree construction metrics to handle the non-determinism introduced by the temporal dimension. The mined sequences are expressed in a readable temporal logic language that is easy to interpret. The application of the proposed methodology is illustrated through various examples.

The notion of recurrence over continuous or dense time, as required for expressinganalog and mixed-signalbehaviors, is fundamentally different from what is offered by the recurrence operators of SystemVerilog assertions (SVAs). This article introduces the formal semantics of recurrence over dense time and provides a methodology for the runtime verification of such properties using interval arithmetic. Our property language extends SVA with dense real-time intervals and predicates containing real-valued signals. We provide a tool kit that interfaces with off-the-shelf EDA tools through the standard VPI.

In current practice a formal analysis of hybrid system models is assertion-based. The work presented here is based on features that look beyond functional correctness toward a quantitative evaluation of behavioral attributes. A feature defines a real-valued evaluation function over a specific set of traces. This paper describes an improved method for the interpretation of features over hybrid automata models. It further demonstrates how satisfiability modulo theory solvers can be used for extracting behavioral traces corresponding to corner cases of a feature. Results are demonstrated on examples from the control and circuit domains.

Circuits and systems that have to deal with real valued artifacts often need to be evaluated not only for correct behaviors, but also the margins by which they satisfy the design intent. Our definition of "features" formally extends the classical notion of "assertions" by overlaying constructs for specifying real valued functions over matches of assertions, thereby providing a powerful language framework for specifying real valued properties of the system. In this paper we present, for the first time, methods for formal evaluation of feature ranges on hybrid automata models which are extensively used for modeling switched control systems. We demonstrate the methodology over three case studies, namely a cruise control system, a DC-DC Buck Regulator and a Li-ion battery charger.

The acceptance criteria for analog designs are traditionally defined in terms of real-valued features defined over behavioral responses. For example, rise time, peak overshoot, and settling time are features of the response of a second-order system under a step input. Designers of analog and mixed-signal (AMS) designs typically like to see whether the relevant features lie within their specified ranges, and if so, by what margin. Assertions are capable of capturing the acceptance criteria, but they do not help in evaluating how well (or by what margin) the design satisfies the specification. We introduce the notion of Feature Indented Assertions (FIAs) for overlaying the definition of real-valued features over the syntactic fabric of AMS assertions. In this paper, we present the formal syntax and semantics of our language, FIA, and demonstrate its ability to capture a wide variety of AMS features. We present our dynamic feature evaluation tool that plugs into standard AMS simulators through Verilog Procedural Interfaces and evaluates features over simulation. At the heart of this tool, we have our interval arithmetic-based algorithm for monitoring features over continuous time and value domains. This algorithm is presented with corresponding proofs of correctness and with results over industrial testcases.