Imandra for
Autonomous Systems
As autonomous systems become ubiquitous, assurance that their designers have considered all of the relevant "edge-cases" is ever more important. Many global projects seek to address the rigorous generation of such scenarios for testing and certification. We strive 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 several 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
Instead, we propose 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 can take a function (or a model) written in the "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
State machine encoding 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.
State Explorer
The following regions were decomposed from the simple intersection model.
Select a region below
for details
- Velocity
- Steady
- Braking
- Accelerating
- Lights
- Green
- Yellow
- Red
- Yellow&Red
- Passing
- Will pass
- Won't pass
Region Name
Constraints
Invariant
We work with many of the world's largest and most trusted brands, universities and government agencies.
And we would be delighted to work with you.
Let's talkTalk
to an Expert
Schedule a contact
Not sure
if we can help?
We'd be happy to discuss your project to suggest the best solution.
Schedulea case analysis