摘要
作为一项新规范,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.
出处
《小型微型计算机系统》
CSCD
北大核心
2013年第1期100-106,共7页
Journal of Chinese Computer Systems
基金
国家自然科学基金项目(60873061)资助
国家"九七三"重点基础研究发展计划项目(2009CB320701
2010CB328103)资助
