信息物理系统性质轨迹检测：弥合信息-物理鸿沟
软件工程
2021-09-16 v3 形式语言与自动机理论
计算机科学中的逻辑
摘要
信息物理系统结合了软件与物理组件。面向信息物理系统（CPS）的规范驱动轨迹检测工具通常为用户提供一种规范语言以表达其关注的需求，以及一种自动过程来检查这些需求是否在 CPS 的执行轨迹上成立。尽管存在若干种面向 CPS 的规范语言，它们往往表达力不足，难以对涉及软件与物理组件及其交互的复杂 CPS 性质进行规范。本文提出（i）信号混合逻辑（HLS），一种基于逻辑的语言，可规范复杂的 CPS 需求；（ii）ThEodorE，一种高效的基于 SMT 的轨迹检测过程。该过程将在一个执行轨迹上检查 CPS 需求的问题，归约为检查一个 SMT 公式的可满足性。我们通过卫星领域一个具有代表性的工业案例研究评估了我们的贡献。我们考虑案例研究中的 212 条需求以评估 HLS 的表达力，HLS 能够表达全部 212 条需求。我们还通过运行针对 747 个轨迹-需求组合的轨迹检测过程来评估 ThEodorE 的适用性，ThEodorE 能够在 74.5% 的案例中给出判定结果。最后，我们将 HLS 与 ThEodorE 同文献中其他规范语言与轨迹检测工具进行了比较。结果表明，从实践角度看，我们的方法在表达力与性能之间提供了更好的权衡。
引用
@article{arxiv.2009.12250,
title = {Trace-Checking CPS Properties: Bridging the Cyber-Physical Gap},
author = {Claudio Menghi and Enrico Viganò and Domenico Bianculli and Lionel C. Briand},
journal= {arXiv preprint arXiv:2009.12250},
year = {2021}
}