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

doi:10.3969/j.issn.1000-1220.2013.01.018

CORC > 北京大学 > 信息科学技术学院

	基于模型转换的MARTE顺序图的形式化分析; Formal Analysis of Sequence Diagram in MARTE by Model Transformation Techniques
	朱梅霞 ; 王捍贫 ; 刘西奎 ; 韩晓琼
刊名	小型微型计算机系统
	2013
关键词	实时系统形式化方法时间变迁系统验证 MARTE
DOI	10.3969/j.issn.1000-1220.2013.01.018
英文摘要	作为一项新规范,MARTE有许多方面亟待完善.如何对依照MARTE设计的模型开展验证是待解决问题之一.对象管理组织提出用模型转换的方法将依照MARTE设计的模型(记为A)转换成另一种具有完备的验证方法和工具的形式化模型(记为B),然后对B进行验证和精化,以完成A的验证和精化工作.此思想面临的难题是如何保证B能够完整且准确地模拟A的行为.提出了形式化模型-TrS4SD,用来描述MARTE规范定义的带时间约束的顺序图的形式语义并在此基础上展开分析.首先给出顺序图的形式定义,把时阃变迁系统(TrS)扩充成TrS4SD,用TrS4SD描述顺序图的形式语义,最后对TrS4SD展开分析.这在一定程度上提高了设计阶段模型的正确性.通过一个实例说明从顺序图到TrS4SD的转化过程以及基于TTS4SD的验证方法.; 国家自然科学基金项目; 国家"九七三"重点基础研究发展计划项目; 中文核心期刊要目总览(PKU); 中国科技核心期刊(ISTIC); 中国科学引文数据库(CSCD); 0; 1; 100-106; 34
语种	中文
内容类型	期刊论文
源URL	[http://ir.pku.edu.cn/handle/20.500.11897/285669]
专题	信息科学技术学院
推荐引用方式 GB/T 7714	朱梅霞,王捍贫,刘西奎,等. 基于模型转换的MARTE顺序图的形式化分析, Formal Analysis of Sequence Diagram in MARTE by Model Transformation Techniques[J]. 小型微型计算机系统,2013.
APA	朱梅霞,王捍贫,刘西奎,&韩晓琼.(2013).基于模型转换的MARTE顺序图的形式化分析.小型微型计算机系统.
MLA	朱梅霞,et al."基于模型转换的MARTE顺序图的形式化分析".小型微型计算机系统 (2013).