MARTE顺序图到TTS4SD的转换

计算机科学 ›› 2013, Vol. 40 ›› Issue (1): 175-178.

MARTE顺序图到TTS4SD的转换

朱梅霞，武继刚

(天津工业大学计算机科学与软件学院天津300387)

出版日期:2018-11-16 发布日期:2018-11-16

Approach to Transforming MARTS Sequence Diagram to TTS4SD Models

Online:2018-11-16 Published:2018-11-16

摘要/Abstract

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

关键词: 实时系统，顺序图，CCSL，形式化方法，模型转换

Abstract: 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. ho 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 sectuence diagram and the TTS4SD,then we described the semantics of the sequence diagram by I hS4SD. Taking the semantics as basis,the checking work was carried out on the TTS4SD.An example was given to describe the above process.

Key words: Regression test,Lines of code,Select test subset, Lest requirement

朱梅霞，武继刚. MARTE顺序图到TTS4SD的转换[J]. 计算机科学, 2013, 40(1): 175-178. https://doi.org/

参考文献

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed