MARTE顺序图到CCSL模型的转换  

Approach to transforming MARTE sequence diagram to CCSL models

作　　者：朱梅霞[1] 

机构地区：[1]天津工业大学计算机科学与软件学院,天津300387

出　　处：《计算机工程与科学》2013年第10期172-180,共9页Computer Engineering & Science

基　　金：国家自然科学基金资助项目(61173032);天津工业大学引进人才基金资助项目(20120042)

摘　　要：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.

关 键 词：实时系统 模型转换 顺序图 CCSL 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]