|
|||||
|
|
| 基于模型转换的MARTE顺序图的形式化分析 | |
| 引用本文： | 朱梅霞,王捍贫,刘西奎,韩晓琼.基于模型转换的MARTE顺序图的形式化分析[J].小型微型计算机系统,2013,34(1):100-106. |
| 作者姓名： | 朱梅霞 王捍贫 刘西奎 韩晓琼 |
| 作者单位： | 1. 天津工业大学计算机科学与软件学院,天津,300387 2. 北京大学信息科学技术学院软件研究所,北京100871;教育部高可信软件技术重点实验室,北京100871 3. 山东科技大学信息科学与工程学院,山东青岛,266510 |
| 基金项目： | 国家自然科学基金项目(60873061)资助;国家“九七三”重点基础研究发展计划项目(2009CB320701,2010CB328103)资助 |
| 摘 要： | 作为一项新规范,MARTE有许多方面亟待完善.如何对依照MARTE设计的模型开展验证是待解决问题之一.对象管理组织提出用模型转换的方法将依照MARTE设计的模型(记为A)转换成另一种具有完备的验证方法和工具的形式化模型(记为B),然后对B进行验证和精化,以完成A的验证和精化工作.此思想面临的难题是如何保证B能够完整且准确地模拟A的行为.提出了形式化模型-TrS4SD,用来描述MARTE规范定义的带时间约束的顺序图的形式语义并在此基础上展开分析.首先给出顺序图的形式定义,把时阃变迁系统(TrS)扩充成TrS4SD,用TrS4SD描述顺序图的形式语义,最后对TrS4SD展开分析.这在一定程度上提高了设计阶段模型的正确性.通过一个实例说明从顺序图到TrS4SD的转化过程以及基于TTS4SD的验证方法. |
| 关 键 词： | 实时系统 形式化方法 MARTE 时间变迁系统 验证 |
Formal Analysis of Sequence Diagram in MARTE by Model Transformation Techniques |
|
| ZHU Mei-xia , WANG Han-pin , LIU Xi-kui , HAN Xiao-qiong.Formal Analysis of Sequence Diagram in MARTE by Model Transformation Techniques[J].Mini-micro Systems,2013,34(1):100-106. | |
| Authors: | ZHU Mei-xia WANG Han-pin LIU Xi-kui HAN Xiao-qiong |
| Affiliation: | 2,3 1(Tianjin University of Technology,Computer Science and Software Engineering,Tianjin 300387) 2(Institute of Software,School of Electronics Engineering and Computer Science,Peking University,Beijing 100871,China) 3(Key Laboratory of High Confidence Software Technologies,Ministry of Education,Peking University,Beijing 100871,China) 4(College of Information Engineering,Shandong University of Science and Technology,Qingdao 266510,China) |
| Abstract: | |
| Keywords: | |
| 本文献已被 CNKI 万方数据 等数据库收录！ | |