动态环境中安全关键自主系统的验证
软件工程
2016-12-16 v1 计算机与社会
机器人学
摘要
在高度异构、动态的环境中部署自主系统的需求日益增长，例如医院中的服务机器人或高速公路上的自动驾驶汽车。由于这些环境中的不确定性，在设计时针对系统与环境模型获得的验证结果可能无法转移到运行时的系统行为。对于在动态环境中运行的自主系统，运动安全和碰撞避免是关键要求。关于这些要求，Macek等人[6]定义了被动安全属性，要求当自主系统运动时不能发生任何碰撞。为验证该属性，我们采用两阶段过程，结合设计时使用静态验证方法和运行时使用动态验证方法。在设计阶段，我们利用UPPAAL将自主系统及其环境形式化为定时自动机，将安全属性形式化为TCTL公式，并针对该属性验证这些模型的正确性。对于运行时阶段，我们构建了一个监视器以检查设计时的假设在运行时是否也正确。如果当前对环境系统的观察与初始系统假设不符，监视器向系统发送反馈，系统进入被动安全状态。
引用
@article{arxiv.1612.04977,
title = {Towards the Verification of Safety-critical Autonomous Systems in Dynamic Environments},
author = {Adina Aniculaesei and Daniel Arnsberger and Falk Howar and Andreas Rausch},
journal= {arXiv preprint arXiv:1612.04977},
year = {2016}
}
备注
In Proceedings V2CPS-16, arXiv:1612.04023