| Formal Analysis of Sequence Diagram with Time Constraints by Model Transformation |
| Download PDF |
| Meixia Zhu,Hanpin Wang,Xikui Liu,Xiaoqiong Han. Formal Analysis of Sequence Diagram with Time Constraints by Model Transformation. International Journal of Software and Informatics, 2012,6(2):327~357 |
| Hits: 5138 |
| Download times: 3352 |
|
| Fund:This work is sponsored by the National Natural Science Foundation of China under Grant Nos.60873061 and 61170299 and the National Basic Research Program of China (973 Program) under Grant Nos. 2009CB320701 and 2010CB328103. |
|
| Abstract:The Profile for the Modeling and Analysis of Real-Time Embedded Systems (MARTE) provides an extended sequence diagram with time properties (SDT). This kind of diagram is frequently used in the preliminary developing phase of the embedded real time systems (ERTS), however, it is not easy to verify the system it has described because few tools can check it directly. This is mainly due to its semi-formal style and its abstract mode in describing the behaviors of the corresponding system. The formal definition of the SDT is firstly introduced, and an extended model named timed transition system for SDT (TTS4SDT) is advanced for describing its formal semantics. By model transformation
techniques, the SDT is transformed to the intermediate model--TTS4SDT, and the transforming methods are divided into two categories: when the SDT doesn't equip with nesting structures and when it does. Two examples (one is without nesting structure and another is with) are offered to demonstrate the transforming process. Then based on the TTS4SDT, the sequence diagram is analyzed in a rigid way to eliminate the mistakes arising from the designing stage. |
| keywords:real-time systems timed transition system formal semantics MARTE model transformation |
| View Full Text View/Add Comment Download reader |
