A Multi-Agent Spatial Logic for Scenario-Based Decision Modeling and Verification in Platoon Systems

• 作者: Jingwen Xu Yanhong Huang Jianqi Shi Shengchao Qin
• 来源期刊: 计算机科学技术学报（英文版）
• 年，卷（期）: 2021,（6）
• 所属期刊栏目: Special Section on Software Systems 2021-Theme: Dependable Software Engineering
• 页码范围: 1231-1247
• 页数: 17页
• 语种: 英文
• DOI: 10.1007/s11390-021-1565-8

摘要

To cater for the scenario of coordinated transportation of multiple trucks on the highway,a platoon system for autonomous driving has been extensively explored in the industry.Before such a platoon is deployed,it is necessary to ensure the safety of its driving behavior,whereby each vehicle's behavior is commanded by the decision-making function whose decision is based on the observed driving scenario.However,there is currently a lack of verification methods to ensure the reliability of the scenario-based decision-making process in the platoon system.In this paper,we focus on the platoon driving scenario,whereby the platoon is composed of intelligent heavy trucks driving on cross-sea highways.We propose a formal modeling and verification approach to provide safety assurance for platoon vehicles'cooperative driving behaviors.The existing Multi-Lane Spatial Logic(MLSL) with a dedicated abstract model can express driving scene spatial properties and prove the safety of multi-lane traffic maneuvers under the single-vehicle perspective.To cater for the platoon system's multi-vehicle perspective,we modify the existing abstract model and propose a Multi-Agent Spatial Logic(MASL) that extends MLSL by relative orientation and multi-agent observation.We then utilize a timed automata type supporting MASL formulas to model vehicles'decision controllers for platoon driving.Taking the behavior of a human-driven vehicle(HDV) joining the platoon as a case study,we have implemented the model and verified safety properties on the UPPAAL tool to illustrate the viability of our framework.