实时系统规范语言STeC的Maude重写系统  

Maude Rewriting System of Specification Language STeC for Real-time System

作　　者：栾天骄[1] 陈仪香[1] 王江涛[1] 

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

出　　处：《计算机工程》2013年第10期57-62,67,共7页Computer Engineering

基　　金：国家"973"计划基金资助项目(2011CB302802);国家"863"计划基金资助项目(2011AA010101);国家自然科学基金资助项目(61021004)

摘　　要：信息物理融合系统的网络化、系统化和信息化等特性使得软件系统的复杂程度不断增加。为此,引入实时系统的规范语言STeC,用于刻画具有时空一致性要求的实时系统。对于STeC语言的自动逻辑推理问题,通过拓展Maude中的关系等式和重写规则,将STeC语言转化为可执行的基于Maude的形式化描述,使用Maude自动推导功能,自动推导出系统的时间正确性。实例结果表明,该形式化描述语言Maude可有效对实时系统进行安全性验证。The characteristics of cyber physical systems such as cyberization, systematization and informationization make the software systems more and more complex. Because the classic modeling methods cannot satisfy the needs of Cyber-physical System（CPS）, the Spatio-Temporal Consistence（STeC） language for real-time systems whose core property is the consistence of time and location is introduced to model the real-time systems. In order to achieve the automatic logical reasoning in STeC, the equation and rewriting rule in Maude are applied to convert the STeC system to an executable specification description, it can analyze the result of computation and check the correctness of time in the system. Instance results show that the formal description language Maude can effective for real-time system for security verification.

关 键 词：实时系统 实时系统的规范语言 重写逻辑 形式化分析 时空一致性 操作语义 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]