提出跨层验证方法，确保机器人系统在多层协同下的行为正确性。
Cross--layer Formal Verification of Robotic Systems
- 用抽象层模型辅助验证某一层，避免逐层孤立分析
- 通过模型精化和属性精化双重策略提升验证效率
- 适合复杂机器人系统开发与安全验证的工程师
机器人系统广泛应用于人机交互或关键任务。由于其模块化和复杂性，设计与验证常分层进行。但部分系统性质需同时考虑多层才能分析。本文提出一种跨层验证方法，通过使用其他层的抽象来验证特定层的行为。提出两种策略：对抽象层模型进行精化，或对待验证属性进行精化。结合两者可有效保持模型通用性，并缓解状态空间爆炸问题。
原文摘要 · Abstract (English)
Robotic systems are widely used to interact with humans or to perform critical tasks. As a result, it is imperative to provide guarantees about their behavior. Due to the modularity and complexity of robotic systems, their design and verification are often divided into several layers. However, some system properties can only be investigated by considering multiple layers simultaneously. We propose a cross-layer verification method to verify the expected properties of concrete robotic systems. Our method verifies one layer using abstractions of other layers. We propose two approaches: refining the models of the abstract layers and refining the property under verification. A combination of these two approaches seems to be the most promising to ensure model genericity and to avoid the state-space explosion problem.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。