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

作     者：栾天骄 陈仪香 王江涛 LUAN Tian-jiao;CHEN Yi-xiang;WANG Jiang-tao

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

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

出 版 物：《计算机工程》 (Computer Engineering)

年 卷 期：2013年第39卷第10期

页      码：57-62,67页

摘      要：信息物理融合系统的网络化、系统化和信息化等特性使得软件系统的复杂程度不断增加。为此,引入实时系统的规范语言STeC,用于刻画具有时空一致性要求的实时系统。对于STeC语言的自动逻辑推理问题,通过拓展Maude中的关系等式和重写规则,将STeC语言转化为可执行的基于Maude的形式化描述,使用Maude自动推导功能,自动推导出系统的时间正确性。实例结果表明,该形式化描述语言Maude可有效对实时系统进行安全性验证。

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

学科分类：08[工学] 0835[0835] 081202[081202] 0812[工学-测绘类] 

核心收录：

D　O　I：10.3969/j.issn.1000-3428.2013.10.012

馆 藏 号：203796694...