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

• 作者: 刘西奎 朱梅霞 王捍贫 韩晓琼
• 来源期刊: 小型微型计算机系统
• 学科: 工学
• 关键词: 实时系统 形式化方法 MARTE 时间变迁系统 验证
• 年，卷（期）: 2013,（1）
• 所属期刊栏目: 计算机软件与数据库技术
• 页码范围: 100-106
• 页数: 7页
• 分类号: TP311
• 字数: 7693字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王捍贫	北京大学信息科学技术学院软件研究所	14	23	3.0	4.0
3	刘西奎	山东科技大学信息科学与工程学院	24	104	7.0	9.0
4	朱梅霞	天津工业大学计算机科学与软件学院	7	6	2.0	2.0
5	韩晓琼	北京大学信息科学技术学院软件研究所	2	7	2.0	2.0