论文标题
集成正式验证和基于仿真的断言检查,以证实的V&V流程
Integrating Formal Verification and Simulation-based Assertion Checking in a Corroborative V&V Process
论文作者
论文摘要
自动化车辆(AV)在运输域中迅速成熟。但是,AV设计问题的复杂性使得没有任何一种技术足以对安全性,可靠性或可信度等关键属性进行足够的验证。在本视觉论文中,提出了使用模拟的断言检查的空间流量逻辑和基于代理的验证方法与验证方法的组合。我们绘制如何在称为佐证验证和验证(V&V)的方法框架内整合相应方法。佐证的V&V框架标识了三种不同的AVS(正式验证,基于模拟的测试,现实世界实验)的三个不同的验证和验证级别,并指定了这些级别之间的联系和证据。我们为正式设计验证和基于仿真的测试的证据之间必须建立的形式关系的规范,以相互证实并增强验证和验证的保证信心。
Automated Vehicles (AVs) are rapidly maturing in the transportation domain. However, the complexity of the AV design problem is such that no single technique is sufficient to provide adequate validation of key properties such as safety, reliability or trustworthiness. In this vision paper, a combination of a spatial traffic logic and agent-based verification methods with a validation method that uses assertion checking of simulations is proposed. We sketch how to integrate the respective approaches within a methodological framework called Corroborative Verification and Validation (V&V).The Corroborative V&V framework identifies three different verification and validation levels for AVs (formal verification, simulation-based testing, real-world experiments) and specifies connections and evidence between these levels. We define specifications for the formal relationships that must be established between processes, system models and requirements models for the evidence from formal design verification and simulation-based testing to corroborate each other and enhance assurance confidence from verification and validation.