MakSafe framework checks vehicle safety rules using smart forecasting
MakSafe: A Spatiotemporal Semantic Framework for Formal Specification and Compliance Checking of Road Vehicle Safety Rules
Computation and LanguageSymbolic Computation
Summary
Road vehicles have many safety rules that are hard to check because traffic is always changing. The authors created MakSafe, a system that uses clear rules and smart predictions about vehicle actions to decide if a situation is safe or not without slowing down due to rigid time steps. It can quickly find which parts of a traffic scenario are safe or risky and update its verdict if the vehicle changes control. This helps ensure vehicles follow safety rules even in complex traffic.
What this means in practice
- •For automotive safety engineers: Check automated vehicle safety rules accurately and efficiently in diverse traffic scenarios using MakSafe’s semantic forecasting.
- •For traffic simulation developers: Integrate MakSafe to evaluate vehicle safety compliance over various traffic densities and control updates in simulations.
Authors
Maksym Labzhaniia, Julien Deantoni, Marie-Agn{è}s Peraldi-Frati, Fr{é}d{é}ric Mallet
Abstract
Scenario-based validation is essential for automated road vehicles but cannot cover the full variability of openworld traffic. We present MakSafe, a formal spatiotemporal framework for specifying and checking road vehicle safety rules through semantic zones, action-based forecasting, and trace-tree reasoning, avoiding uniform time discretization. We formalize the road network, vehicle states, and occupancy zones, then build executable rules for front-vehicle identification and timeto-collision (TTC) verification. The evaluation combines a tracedependent case study with a scalability benchmark over traffic density (N ), horizon (H), and branch factor (B). MakSafe yields branch-specific verdicts, deriving safe and unsafe outcomes from the same initial scene, and re-evaluates a scenario after a control update. A single rule check stays well below a millisecond across the reported sweep, and longer horizons slow the TTC check.