基于STeC-Stateflow转换系统的实时系统仿真与验证方法  

Real-time system simulation and verification approach based on STeC to Stateflow transformation system

作　　者：纪政[1] 李慧勇[1] 陈仪香[1] 

机构地区：[1]华东师范大学软件学院教育部软硬件协同设计技术与应用工程研究中心,上海200062

出　　处：《计算机应用研究》2014年第2期448-453,共6页Application Research of Computers

基　　金：国家"973"计划基金资助项目(2011CB302802);国家自然科学基金资助项目(61202104);上海高校知识创新工程(085)建设项目

摘　　要：物联网以及信息物理融合系统对形式化建模提出了新的挑战,引入了实时系统规范语言STeC,为刻画实时系统的时空一致性提供了规范语言。针对STeC语言建立STeC至Stateflow自动转换系统,提出一种基于STeC至Stateflow转换的仿真及验证方法,该方法使用STeC语言对实时系统进行形式化建模,再建立实时监控的Simulink仿真模型,并使用Checkmate对系统进行安全性验证。通过对京沪高铁运行的实例研究,表明该方法对高铁运行系统实时仿真的有效性,并能够验证高铁运行系统的安全性。Internet of Things or cyber-physical systems provide a new challenge for formal modeling methods related to the as- pect of physical elements such as location and time. Recently, this paper introduced a specification language called STeC to stress the spatio-temporal consistency for real-time systems. The operational and denotational semantics of and tool set related to this language have been given. The aim of this paper was to establish a STeC to Stateflow automatic transformation system and to propose a simulation and verification approach based on this transformation system. It firstly gave a formal model for an object system in STeC language, and then set up a real-time monitoring simulation model using Simulink. After that, it presen- ted a verification approach for the system safety property based on Checkmate. Finally, it gave a case about Jinghu Gaotie （high speed train） running timetable to show that the proposed approach is effect and usable.

关 键 词：实时系统 实时系统规范语言 时空一致性 系统仿真与验证 STATEFLOW Checkmate 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]