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

• 作者: 栾天骄 王江涛 陈仪香
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: 实时系统 实时系统的规范语言 重写逻辑 形式化分析 时空一致性 操作语义
• 年，卷（期）: 2013,（10）
• 所属期刊栏目: 体系结构与软件技术
• 页码范围: 57-62,67
• 页数: 7页
• 分类号: TP311
• 字数: 4887字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2013.10.012

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈仪香	华东师范大学软硬件协同设计技术与应用教育部工程研究中心	20	64	4.0	7.0
2	王江涛	华东师范大学软硬件协同设计技术与应用教育部工程研究中心	24	64	4.0	7.0
3	栾天骄	华东师范大学软硬件协同设计技术与应用教育部工程研究中心	2	5	2.0	2.0