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: 4756
Download times: 2934
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



Top Paper  |  FAQ  |  Guest Editors  |  Email Alert  |  Links  |  Copyright  |  Contact Us

© Copyright by Institute of Software, the Chinese Academy of Sciences

京公网安备 11040202500065号