Abstract:

The clock constraint specification language (CCSL) is a modeling language defined in the MARTE. By Observer technique, the verification of the CCSL models can be realized. However, compared with SD, CCSL models cannot be easily understood by the users. (1) Based on formal methods, a transforming technique is proposed to transform SD to CCSL models; (2) The bisimulation relation between SD and the corresponding CCSL models is also proved. The proposed method, to a certain extent, extends MARTE’s range of application: in order to make the users and the designers to reach a consensus, the system’s dynamic behavior is modeled by SD at first, then, the SD is transformed to CCSL models to check whether the system can meet the requirement. An example is running through to expound our method.

Key words: real-time systems;model transformation;sequence diagram;CCSL