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

摘要：

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

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

分类号：TP311(计算技术、计算机技术)

资助基金：国家“973”计划基金资助项目2011CB302802；国家“863”计划基金资助项目2011AA010101；国家自然科学基金资助项目61021004

在线出版日期：2013-12-04（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：57-62,67