Scholarlink

Verification and validation of robotic and autonomous systems often relies on heterogeneous verification methods (e.g., formal verification, simulation-based testing and physical experiments) to build confidence in system correctness. Manually reconciling evidence from these diverse sources is both time-consuming and error-prone for safety engineers. Moreover, tool support to help safety assessors integrate heterogeneous evidence into coherent, evidence-based assurance cases is much needed. Towards addressing these challenges, in this study we propose an Eclipse plugin (ECV2), which integrates multi-source evidence from formal verification, simulation test-benches and experiment logs. It computes per-metric ranges across techniques, assigns criticality levels and automatically flags outliers. It generates human-readable, evidence-linked recommendations to guide targeted refinement. To ensure semantic consistency and objective guidance, ECV2 aligns each metric with relevant domain ontologies and assurance-case thresholds. Its interactive, colour-coded, multi-column tree view highlights criticality variances directly within the Eclipse environment. We demonstrate ECV2 through a nuclear-radiation autonomous inspection robot case study, deriving nine measurements from PRISM formal verification alongside corresponding metrics from a ROS-based patrol software simulation.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Corroborative V&V for Autonomous Systems: Integrating Evidence and Discrepancy Analysis for Safety Assurance

  • 会议论文

  • 发表日期：

    2025年

查看全文
  • Dhaminda B. Abeywickrama,
  • Christopher Bishop,
  • Simon Watson,
  • Frederic Wheeler,
  • Michael Fisher,
  • Louise Dennis

摘要

Verification and validation of robotic and autonomous systems often relies on heterogeneous verification methods (e.g., formal verification, simulation-based testing and physical experiments) to build confidence in system correctness. Manually reconciling evidence from these diverse sources is both time-consuming and error-prone for safety engineers. Moreover, tool support to help safety assessors integrate heterogeneous evidence into coherent, evidence-based assurance cases is much needed. Towards addressing these challenges, in this study we propose an Eclipse plugin (ECV2), which integrates multi-source evidence from formal verification, simulation test-benches and experiment logs. It computes per-metric ranges across techniques, assigns criticality levels and automatically flags outliers. It generates human-readable, evidence-linked recommendations to guide targeted refinement. To ensure semantic consistency and objective guidance, ECV2 aligns each metric with relevant domain ontologies and assurance-case thresholds. Its interactive, colour-coded, multi-column tree view highlights criticality variances directly within the Eclipse environment. We demonstrate ECV2 through a nuclear-radiation autonomous inspection robot case study, deriving nine measurements from PRISM formal verification alongside corresponding metrics from a ROS-based patrol software simulation.