在模型检测中对于网络物理系统的环境建模
摘要：保证网络物理系统（CPS）的安全性和有效性是个挑战，因为它们的操作环境变化多样。模型检测已经被提出用于验证CPS，但是环境模型要么过于具体以至于无法捕捉到环境的变化性，要么过于抽象以至于专业人士在应用领域无法解释反例。针对这个问题，需要领域专家既懂形式方法又懂应用领域，才能提供特定领域的解决方案，这限制了模型检测在CPS验证中的有效应用。本文提出一种基于时钟自动机的领域无关框架，用于在模型检测过程中对环境模型进行抽象和细化。该框架维护了一个环境模型的抽象树，提供可解释的反例，并保证了对环境行为的全面覆盖。借助这个框架，应用领域的专家可以有效地使用模型检测，而不需要形式方法的专业知识。
作者：Guangyao Chen and Zhihao Jiang
论文ID：2105.01236
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2021-05-05