MARTE顺序图到TTS4SD的转换

Approach to Transforming MARTE Sequence Diagram to TTS4SD Models

MARTE对UML的顺序图进行了扩充,使其适用于实时系统的建模阶段,但它不能直接用于正确性验证阶段。对象管理组织提出用模型转换的方法将依照MARTE构造的顺序图(记为A)转换成具有完备的验证方法和工具的形式化模型(记为B)。用B表示A的语义可以保证B能够完整且准确地模拟A的行为。提出了形式化模型——TTS4SD,用来描述MARTE顺序图的形式语义,并在此基础上展开了验证。首先给出顺序图的形式定义,把时间变迁系统(TTS)扩充成TTS4SD;然后用TTS4SD描述顺序图的形式语义,并给出从顺序图到TTS4SD的转换算法;最后对TTS4SD展开分析。通过一个实例说明了从顺序图到TTS4SD的转化过程以及基于TTS4SD的验证方法。

The sequence diagram was extended in the MARTE specification for modeling purpose,but it can not be used in the correctness verification stage.The OMG proposes to solve this problem by model transformation techniques：the model A is transformed to a formal model B which is equipped with efficient analysis or verification tools.To describe the semantics of A by model B can guarantee the bi-simulation relation between them.A model named timed transition system for sequence diagram（TTS4SD） was proposed.At first,we offered the formal syntax of the sequence diagram and the TTS4SD,then we described the semantics of the sequence diagram by TTS4SD.Taking the semantics as basis,the checking work was carried out on the TTS4SD.An example was given to describe the above process.