As autonomous systems become ubiquitous, assurance that their designers have considered all of the relevant "edge-cases" is evermore important. A number of global projects seek to address rigorous generation of such scenarios for testing and certification. We would like to extend their efforts and propose deriving concrete driving scenarios (for testing autonomous systems) from higher-level "digital twin" models representing the physical world. When encoded as infinite state machines, these models become much more expressive and "natural" for encoding than individual scenarios. Furthermore, they are susceptible to formal verification and reasoning, empowering the designers to tackle even the most complex domains.
Test Scenario Generation
The current industry efforts focus on creating/operating on scenarios directly and then ‘running’ them in simulation environments.
There are a number of recognized problems with this approach:
Coverage metrics: given a collection of ‘hand-written’ scenarios, there’s no methodology for reasoning about their coverage.
Mapping: how to map actual driving data back into a particular driving scenario. A particular ‘run’ of a scenario may exhibit non-deterministic behavior, making such mapping especially difficult.
Scalability: there are potentially many unique driving scenarios and encoding them ‘by hand’ does not scale.
“Lifting” Test Scenario Generation
We propose instead to focus on encoding ‘digital twin’ models and then use them to derive scenarios via state-space region decomposition.
There are multiple advantages to this approach:
It’s much more natural to encode such models and reason about their completeness.
Each model may be decomposed into a finite number of symbolic ‘edge cases’ or ‘regions’ of its state-space.
Scenarios may be synthesized from such regions and vice versa, given vehicle driving data, we can map it into a particular region of the model state-space.
Modeling “Digital Twins” As Infinite State Machines
Infinite state machines are the natural method for encoding ‘digital twin’ models representing particular driving geographies and the associated physical representations.
As with any formal model of a physical phenomenon, there are various degrees of representing ‘reality’.
Imandra’s Region Decomposition
Region Decomposition is a feature of Imandra inspired by Cylindrical Algebraic Decomposition (CAD) but lifted for algorithms at large. With Region Decomposition, Imandra is able to take a function (or a model) written in “pure” subset of OCaml (or ReasonML) and describe its behavior with a finite number of regions of its state-space.
Each such region of the state-space contains:
● A set of symbolic constraints on the inputs
● A symbolic invariant describing expected output
Imandra can further synthesize concrete inputs into the model satisfying a particular region - these instances will then be printed as driving scenario descriptions (e.g. CARLA’s Python Strategy Interface).
State-space Regions of “Digital Twin” Models
Given a “digital twin” state machine encoding a particular geography (with physics, etc.), each region of its state-space represents a distinct symbolic driving scenario.
Generating Test Cases
Imandra is a cloud-native automated reasoning engine allowing you to:
• Encode ‘digital twin’ models using OCaml or ReasonML
• Decompose their state-spaces to create quantitative coverage metrics (symbolic driving scenarios)
• Synthesize and print (in whatever format is best suited for your simulation environment) concrete driving scenarios
Quantifying Testing Coverage
You can actually map the driving data into regions to understand what subset of the state-space has been covered.