基于模型转换的MARTE 顺序图的形式化分析

摘要：

　　本文提出了一种形式化模型—TTS4SD,用来描述MARTE规范定义的带时间约束的顺序图的形式语义并在此基础上展开分析。首先给出顺序图的形式定义, 把时间变迁系统(TTS) 扩充成TTS4SD, 用TTS4SD描述顺序图的形式语义, 最后对TTS4SD展开分析工作，这在很大程度上提高了设计阶段模型的正确性。通过一个实例说明从顺序图到TTS4SD 的转化过程以及基于TTS4SD的验证过程。

关键词： 程序设计 语义定义 算法语言 TTS4SD模型

作者: 朱梅霞 王捍贫 刘西奎

作者单位: 北京大学信息科学技术学院软件研究所,北京100871 教育部高可信软件技术重点实验室, 北京100871 山东科技大学信息科学与工程学院,青岛 266510

会议类型: 国内会议

会议名称: 2011年中国计算机学会服务计算学术会议(CCF NCSC2011)

会议地点: 济南

会议语种:中文

页码: 1-8

在线出版日期: 2011-08-18（万方平台首次上网日期，不代表论文的发表时间）