信息物理系统中混合动态时序行为的形式化分析
软件工程
2019-11-01 v1
摘要
使用闭环验证确保信息物理系统（CPS）中时序行为的正确性，由于系统和环境中均存在混合动力学而具有挑战性。Simulink 和 Stateflow 是支持多种机制对实时嵌入式系统混合动力学进行建模和分析的基于模型的设计工具。本文提出了一种基于 SMT 的方法，用于对 Simulink 模块和 Stateflow 状态（S/S）建模的 CPS 的混合动态时序行为进行形式化分析。层次化互连的 S/S 被扁平化并翻译成 SMT 求解器的输入语言以进行形式化验证。提供了一个翻译算法以促进翻译。针对 S/S 模型的时序约束的形式化验证被简化为所得 SMT 编码的有效性检查。我们通过一个无人水面艇案例研究展示了该方法的适用性。
引用
@article{arxiv.1910.14306,
title = {Formal Analysis of Hybrid-Dynamic Timing Behaviors in Cyber-Physical Systems},
author = {Li Huang and Eun-Young Kang},
journal= {arXiv preprint arXiv:1910.14306},
year = {2019}
}
备注
4 pages, accepted as a work-in-progress paper in RTSS-BP2019