文章基本信息

标题：Formal Synthesis of Safe Stop Tactical Planners for an Automated Vehicle ⁎
本地全文：下载
作者：Jonas Krook ; Roozbeh Kianfar ; Martin Fabian 等
期刊名称：IFAC PapersOnLine
印刷版ISSN：2405-8963
出版年度：2020
卷号：53
期号：4
页码：445-452
DOI：10.1016/j.ifacol.2021.04.059
语种：English
出版社：Elsevier
摘要：AbstractAutomated vehicles need a safe back-up solution in the presence of system degradations since a driver cannot be expected to take control on short notice. In the event of a degradation, the vehicle is required to reach a minimal risk condition via a minimal risk maneuver. The activation of such maneuvers is safety critical, and a correct implementation of the tactical planner that takes the activation decision is paramount. One way to ensure correctness is to employ formal methods since they can provide proofs thereof. Earlier, a tactical planner was formally verified to activate a minimal risk maneuver if and only if a failure occurs. Formal verification has some drawbacks, so this paper investigates the applicability of using the tools Supremica and TuLiP to synthesize correct-by-construction tactical planners. These two tools amend some of the verification’s drawbacks, but also introduce their own.
关键词：KeywordsAutomated DrivingSupervisory Control TheoryReactive Synthesis