Modeling and Verification of Autonomous Driving Systems under Stochastic Spatio-Temporal Constraints

The decision-making process in autonomous driving systems encounters large uncertainties with environmental changes and needs to face the complex spatio-temporal evolution of multiple objectives. Formal analysis and verification are crucial to establishing reliable and safe standards. In this paper, we propose an extension of the clock constraint language CCSL to construct spatio-temporal constraint and autonomous driving safety specifications, leveraging various autonomous driving scenarios. Additionally, we introduce probabilistic spatio-temporal events and devise extensions for driving specifications that incorporate stochasticity. This specification is converted to the UPPAAL-SMC model for facilitating formal modeling and verification. Specific schemes and verification are given in conjunction with a typical autonomous driving scenario.