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

被引：2

作者：

栾天骄

陈仪香

王江涛

机构：

[1] 华东师范大学软硬件协同设计技术与应用教育部工程研究中心

来源：

计算机工程 | 2013年 / 39卷 / 10期

关键词：

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

D O I：

暂无

中图分类号：

TP316.2 [实时操作系统];

学科分类号：

081202 ; 0835 ;

摘要：

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

引用

页码：57 / 62+67 +67

页数：7

共 7 条

[1] 信息-物理融合系统若干关键问题综述 [J].

李仁发 ;

谢勇 ;

李蕊 ;

李浪 .

计算机研究与发展, 2012, 49 (06) :1149-1161

[2] 无线传感器网络 [J].

任丰原 ;

黄海宁 ;

林闯 .

软件学报, 2003, (07) :1282-1291

[3]

基于重写逻辑的SN P系统模型检测[D]. 张民.上海交通大学. 2007

[4]

A Radio Based Intelligent Railway Grade Crossing System to Avoid Collision[J] . Mostafa,Sheikh Shanawaz,Hossian,Md Mahbub,Reza,Khondker Jahid,Rashid,Gazi Maniur.International Journal of Computer Science Issues (IJCSI) . 2010 (6)

[5] Equational rules for rewriting logic [J].

Viry, P .

THEORETICAL COMPUTER SCIENCE, 2002, 285 (02) :487-517

[6] Specification of real-time and hybrid systems in rewriting logic [J].

Ölveczky, PC ;

Meseguer, J .

THEORETICAL COMPUTER SCIENCE, 2002, 285 (02) :359-405

[7]

Maude: specification and programming in rewriting logic[J] . Theoretical Computer Science . 2002 (2)

← 1 →