Stateflow 的有界不变式检查
软件工程
2022-09-29 v1 形式语言与自动机理论
摘要
Stateflow 模型是复杂的软件模型，常作为使用 Matlab Simulink 设计的工业安全关键软件解决方案的一部分。作为安全关键解决方案的组成部分，这些模型需要应用严格的验证技术以保证其正确性。本文提出一种基于反证的的形式化验证方法，用于针对不变式性质分析 Stateflow 模型，该方法基于有界模型检查（BMC）。我们技术的核心在于：i) 将 Stateflow 模型的状态空间表示为关于模型符号配置的符号迁移系统（STS），以及 ii) 应用增量 BMC，在迁移系统的后继关系每次展开后生成验证结果。为此，我们从已有的结构操作语义（SOS）出发，为 Stateflow 开发了符号结构操作语义（SSOS），并证明了两种语义间不变式性质的保持。我们将基于符号配置的 STS 有界不变式检查定义为可满足性问题。我们开发了用于自动生成 STS 初始谓词与后继谓词的流程，以及以利用标准现成可满足性求解器的工具形式实现的该技术原型。最后，我们通过对一个示例模型与两个工业模型应用该工具，给出了初步性能结果。
引用
@article{arxiv.2209.14028,
title = {Bounded Invariant Checking for Stateflow},
author = {Predrag Filipovikj and Gustav Ung and Dilian Gurov and Mattias Nyberg},
journal= {arXiv preprint arXiv:2209.14028},
year = {2022}
}
备注
In Proceedings FMAS2022 ASYDE2022, arXiv:2209.13181. arXiv admin note: substantial text overlap with arXiv:2103.06248