基于模型转换的MARTE顺序图的形式化分析-论文.pdf

《基于模型转换的MARTE顺序图的形式化分析-论文.pdf》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、小型微型计算机系统2013年1月第1期JournalofChineseComputerSystemsVo1．34No．12013基于模型转换的MARTE顺序图的形式化分析朱梅霞，王捍贫，刘西奎，韩晓琼，‘(天津工业大学计算机科学与软件学院，天津300387)(北京大学信息科学技术学院软件研究所，北京100871)(教育部高可信软件技术重点实验室，北京100871)(山东科技大学信息科学与工程学院，山东青岛266510)E·mail：ilryx8292@126．com摘要：作为一项新规范，MARTE有许多方面亟待完善．如

2、何对依照MARTE设计的模型开展验证是待解决问题之一．对象管理组织提出用模型转换的方法将依照MARTE设计的模型(记为A)转换成另一种具有完备的验证方法和工具的形式化模型(记为B)，然后对B进行验证和精化，以完成A的验证和精化工作．此思想面临的难题是如何保证B能够完整且准确地模拟A的行为．提出了形式化模型-TTS4SD，用来描述MARTE规范定义的带时间约束的顺序图的形式语义并在此基础上展开分析．首先给出顺序图的形式定义，把时间变迁系统(TTs)扩充成"I"FS4SD，用TTS4SD描述顺序图的形式语义，最后对TrS4

3、SD展开分析．这在一定程度上提高了设计阶段模型的正确性．通过一个实例说明从顺序图到1trs4sD的转化过程以及基于TTS4SD的验证方法．关键词：实时系统；形式化方法；MARTE；时间变迁系统；验证中图分类号：TP311文献标识码：A文章编号：10001220(2013)01-0100-07FormalAnalysisofSequenceDiagraminMARTEbyModelTransformationTechniquesZHUMeixia，WANGHan—pin·，LIUXi．kui，HANXiao．qiong·

4、(TianjinUniversityofTechnology，ComputerScienceandSoftwareEngineering，Tianjin300387)(InstituteofSoftware，SchoolofElectronicsEngineeringandComputerScience，PekingUniversity，Beijing100871，China)(KeyLaboratoryofHighConfidenceSoftwareTechnologies，MinistryofEducation，P

5、ekingUniversity，Beijing100871，China)(CollegeofInformationEngineering，ShandongUniversityofScienceandTechnology，Qingdao266510，China)Abstract：Asanewprofile，themodelingandanalysisforreal·timeembeddedsystemsspecification(MARTE)isdeficientinanalysisaspect．Inordertocon

6、querthisdefect，theobjectmanagementgroup(OMG)proposestosolvethisproblembymodeltransformationtechniques：themodel(A)whichisdescribedaccordingtoMARTEistransformedtoaformalmodelBwhichisequippedwitheffi—cientanalysisorverificationtools．Anewmodelnamedtimedtransitionsys

7、temforsequencediagram(Trs4SD)iSusedfordescri—bingtheformalsemanticsofthesequencediagramwithtimepropertiesthatwasdefinedinMARTE．Takingthesemanticsasbasis，thecheckingworkiscarriedoutontheTTS4SD．Unlikemostoftheexistingworks，thesemanticsareputtopracticalapplicationf

8、romtheoreticalaspectbyofferingthetransformingalgorithmsfromsequencediagramtoTTS4SD．ThenbasedontheTTS4SD，thesequencediagramisanalyzedinarigidwaytoeliminatethemistakesa