形式検証arXiv:2203.09885
自動運転車のLNTによる形式モデリングとシミュレーション・テスト
Formally Modeling Autonomous Vehicles in LNT for Simulation and Testing
自動運転車と環境の相互作用を形式言語LNTで2種類モデル化し、形式検証ツールを単一コンポーネントや車両全体に適用する方法を示した論文。
著者: Lina Marsso, Radu Mateescu, Lucie Muller, Wendelin Serwe
分類: cs.LO, cs.RO
原文アブストラクト
We present two behavioral models of an autonomous vehicle and its interaction with the environment. Both models use the formal modeling language LNT provided by the CADP toolbox. This paper discusses the modeling choices and the challenges of our autonomous vehicle models, and also illustrates how formal validation tools can be applied to a single component or the overall vehicle.