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

Formal Analysis of Sequence Diagram in MARTE by Model Transformation Techniques

作　　者：朱梅霞[1] 王捍贫[2,3] 刘西奎[4] 韩晓琼[2,3] 

机构地区：[1]天津工业大学计算机科学与软件学院,天津300387 [2]北京大学信息科学技术学院软件研究所,北京100871 [3]教育部高可信软件技术重点实验室,北京100871 [4]山东科技大学信息科学与工程学院,山东青岛266510

出　　处：《小型微型计算机系统》2013年第1期100-106,共7页Journal of Chinese Computer Systems

基　　金：国家自然科学基金项目(60873061)资助;国家"九七三"重点基础研究发展计划项目(2009CB320701;2010CB328103)资助

摘　　要：作为一项新规范,MARTE有许多方面亟待完善.如何对依照MARTE设计的模型开展验证是待解决问题之一.对象管理组织提出用模型转换的方法将依照MARTE设计的模型(记为A)转换成另一种具有完备的验证方法和工具的形式化模型(记为B),然后对B进行验证和精化,以完成A的验证和精化工作.此思想面临的难题是如何保证B能够完整且准确地模拟A的行为.提出了形式化模型-TTS4SD,用来描述MARTE规范定义的带时间约束的顺序图的形式语义并在此基础上展开分析.首先给出顺序图的形式定义,把时间变迁系统(TTS)扩充成TTS4SD,用TTS4SD描述顺序图的形式语义,最后对TTS4SD展开分析.这在一定程度上提高了设计阶段模型的正确性.通过一个实例说明从顺序图到TTS4SD的转化过程以及基于TTS4SD的验证方法.As a new profile,the modeling and analysis for real-time embedded systems specification（MARTE） is deficient in analysis aspect.In order to conquer this defect,the object management group（OMG） proposes to solve this problem by model transformation techniques： the model（A） which is described according to MARTE is transformed to a formal model B which is equipped with efficient analysis or verification tools.A new model named timed transition system for sequence diagram（TTS4SD） is used for describing the formal semantics of the sequence diagram with time properties that was defined in MARTE.Taking the semantics as basis,the checking work is carried out on the TTS4SD.Unlike most of the existing works,the semantics are put to practical application from theoretical aspect by offering the transforming algorithms from sequence diagram to TTS4SD.Then based on the TTS4SD,the sequence diagram is analyzed in a rigid way to eliminate the mistakes arising from the designing stage.An example is running through to describe the above process.

关 键 词：实时系统 形式化方法 MARTE 时间变迁系统 验证 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]