一种用于 informing 和验证形式化验证方法的自主飞行器连续时间模型
机器人学
2016-09-02 v1
摘要
若要使自主车辆得到广泛应用，我们必须确保其安全运行。为此，必须开发适用于该领域的验证与确认 (V&V) 方法。模型检测是一种形式化技术，允许我们穷尽地探索系统抽象模型的路径。使用如 PRISM 这样的概率模型检测器，我们可以确定诸如任务预期时间或特定任务失败发生的概率等属性。然而，由于抽象过程中的信息丢失，复杂系统的模型检测十分困难。对于受外部影响的系统（如自主车辆），这一点尤为突出。另一种解决方案是使用蒙特卡洛模拟来探索系统连续时间模型的结果。这种方法的主要缺点是其非穷尽性，因为并非分析了系统的所有执行过程。因此，我们致力于开发一个自主车辆的形式化验证框架，在开发的初始阶段利用蒙特卡洛模拟来 informing 和验证我们的符号模型。在本文中，我们提出了一种执行自主任务的四旋翼无人机的连续时间模型。我们将该模型应用于蒙特卡洛模拟，以获取特定的任务属性，从而为形式化验证中采用的符号模型提供信息。
引用
@article{arxiv.1609.00177,
title = {A Continuous-Time Model of an Autonomous Aerial Vehicle to Inform and Validate Formal Verification Methods},
author = {Murray L. Ireland and Ruth Hoffmann and Alice Miller and Gethin Norman and Sandor M. Veres},
journal= {arXiv preprint arXiv:1609.00177},
year = {2016}
}