利用组合方法对自主出租车系统进行建模与验证
系统与控制
2023-04-27 v1 系统与控制
摘要
我们将组合形式化建模与验证方法应用于自主飞机滑行系统。我们提供了对建模方法的见解，并确定了若干需要进一步发展的研究领域。具体而言，我们确定了以下需求：(1) 以不同规范语言表达的视点组合语义，以及推理异构声明式模型的工具；(2) 用于自主系统的形式化模型库，以加速建模并实现高效推理；(3) 将自动化推理工具生成的验证结果提升到规范层的方法；(4) 用于推理不完美实现的概率契约框架；(5) 自主系统的标准高层功能架构；(6) 高阶契约理论。我们认为，满足这些研究需求（及其他）可改进形式化方法在自主系统（包括学习使能系统）设计中的采用，并增强对其安全运行的信心。
引用
@article{arxiv.2304.13517,
title = {Leveraging Compositional Methods for Modeling and Verification of an Autonomous Taxi System},
author = {Alessandro Pinto and Anthony Corso and Edward Schmerling},
journal= {arXiv preprint arXiv:2304.13517},
year = {2023}
}
备注
2023 International Conference on Assured Autonomy (ICAA)