基于模型转换的MARTE顺序图的形式化分析

摘要：

作为一项新规范,MARTE有许多方面亟待完善.如何对依照MARTE设计的模型开展验证是待解决问题之一.对象管理组织提出用模型转换的方法将依照MARTE设计的模型(记为A)转换成另一种具有完备的验证方法和工具的形式化模型(记为B),然后对B进行验证和精化,以完成A的验证和精化工作.此思想面临的难题是如何保证B能够完整且准确地模拟A的行为.提出了形式化模型-TrS4SD,用来描述MARTE规范定义的带时间约束的顺序图的形式语义并在此基础上展开分析.首先给出顺序图的形式定义,把时阃变迁系统(TrS)扩充成TrS4SD,用TrS4SD描述顺序图的形式语义,最后对TrS4SD展开分析.这在一定程度上提高了设计阶段模型的正确性.通过一个实例说明从顺序图到TrS4SD的转化过程以及基于TTS4SD的验证方法.

关键词：实时系统、形式化方法、MARTE、时间变迁系统、验证

所属期刊栏目：34

分类号：TP311(计算技术、计算机技术)

资助基金：国家自然科学基金项目60873061;国家"九七三"重点基础研究发展计划项目2009CB320701,2010CB328103

在线出版日期：2013-05-13（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：100-106