| MARTE顺序图到TTS4SD的转换 |
| |
| 引用本文： | 朱梅霞,武继刚.MARTE顺序图到TTS4SD的转换[J].计算机科学,2013,40(1):175-178. |
| |
| 作者姓名： | 朱梅霞 武继刚 |
| |
| 作者单位： | (天津工业大学计算机科学与软件学院 天津300387) |
| |
| 基金项目： | 国家自然科学基金(61173032)资助 |
| |
| 摘 要： | MARTE对UML的顺序图进行了扩充,使其适用于实时系统的建模阶段,但它不能直接用于正确性验证阶段。对象管理组织提出用模型转换的方法将依照MARTE构造的顺序图(记为A)转换成具有完备的验证方法和工具的形式化模型(记为B)。用B表示A的语义可以保证B能够完整且准确地模拟A的行为。提出了形式化模型——TTS4SD,用来描述MARTE顺序图的形式语义,并在此基础上展开了验证。首先给出顺序图的形式定义,把时间变迁系统(TTS)扩充成TTS4SD;然后用TTS4SD描述顺序图的形式语义,并给出从顺序图到TTS4SD的转换算法;最后对TTS4SD展开分析。通过一个实例说明了从顺序图到TTS4SD的转化过程以及基于TTS4SD的验证方法。
|
| 关 键 词： | 实时系统 顺序图 CCSL 形式化方法 模型转换 |
Approach to Transforming MARTS Sequence Diagram to TTS4SD Models |
| |
| ZHU Mei-xia,WU Ji-gang.Approach to Transforming MARTS Sequence Diagram to TTS4SD Models[J].Computer Science,2013,40(1):175-178. |
| |
| Authors: | ZHU Mei-xia WU Ji-gang |
| |
| Affiliation: | (School of Computer Science and Software Engineering,Tianjin Polytechnic University,Tianjin 300387,China) |
| |
| 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. |
| |
| Keywords: | Regression test Lines of code Select test subset Lest requirement |
| 本文献已被 CNKI 等数据库收录！ |
|
点击此处可从《计算机科学》下载全文 |
|
