STeC到Stateflow转换：实时系统仿真与安全验证

本文主要探讨了在物联网和信息物理融合系统背景下，实时系统形式化建模的新挑战。文章介绍了一种基于STeC（实时系统规范语言）的实时系统仿真与验证方法，通过构建STeC到Stateflow的转换系统，结合Simulink仿真和Checkmate工具，对实时系统的时空一致性进行深入分析和安全验证。 实时系统是指那些对时间有严格要求的系统，它们必须在预定义的时间限制内完成任务，否则可能导致系统失效或出现严重后果。STeC语言是一种专门用于描述实时系统时空一致性的规范语言，它能精确地表示系统的行为和约束，为实时系统的建模提供了一种形式化的方法。 在该研究中，作者提出了一种将STeC语言转换为Stateflow模型的方法。Stateflow是MATLAB Simulink中的一个组件，用于描述复杂系统的行为，特别是具有并发、顺序和条件行为的系统。通过将STeC模型转换为Stateflow，可以利用Simulink强大的仿真能力，对实时系统进行动态行为的模拟和分析。 Simulink模型可以实现实时监控，帮助理解系统在不同条件下的运行状态。而Checkmate则是一个用于系统安全性验证的工具，它可以检测模型是否满足预定的安全属性，确保系统的安全运行。在京沪高铁运行的实例中，这种方法成功地验证了高铁运行系统的实时仿真效果和安全性，证明了该方法的有效性和实用性。 论文还提到了该研究得到了国家自然科学基金和上海高校知识创新工程的支持，表明了这一领域研究的重要性和学术价值。作者团队包括纪政、李慧勇和陈仪香，他们在软件工程、软硬件协同设计、物联网、实时协同规范语言设计、程序语义模型以及软件可信度量与评估等领域有着深入的研究。 关键词涵盖了实时系统、实时系统规范语言、时空一致性、系统仿真与验证、Stateflow和Checkmate，这些都强调了研究的核心内容和技术工具。论文的发表不仅有助于推动实时系统建模和验证技术的发展，也为相关领域的工程实践提供了有价值的参考。