MARTE顺序图到CCSL模型的转换

Approach to transforming MARTE sequence diagram to CCSL models

CCSL定义的模型可对系统的时间属性进行建模,基于Observer技术,还可对CCSL模型的正确性进行分析。但与顺序图相比,CCSL模型不利于用户理解。利用形式化方法实现了顺序图到CCSL模型的转换并证明了两者的互模拟关系。这在一定程度上扩大了MARTE在软件设计中的应用范围和效率:用顺序图对系统的动态行为进行建模,使用户和设计者对系统行为达成一致;将顺序图转换成CCSL模型进行分析,以保证模型的正确性。

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.