基本信息来源于合作网站,原文需代理用户跳转至来源网站获取       
摘要:
UML 动态子图主要包括序列图和状态图等,它们在描述系统的行为方面应用广泛,但是半形式化的语义使它们不能直接进行形式化验证。Coq 是目前主流的交互式定理证明器,用形式化的 Coq 规范来描述 UML 动态子图模型,可以在此基础上进行对模型的属性进行验证等工作。基于现有工作,提出将 UML 动态子图模型转换为 Coq 形式规范的框架,在元模型层次给出状态图和序列图的转换规则,介绍算法和原型工具实现。这种元模型层次的转换方法,保证了转换前后的语法正确性,为进一步分析验证提供了基础。
推荐文章
UML状态机到B形式化规约的转换
UML状态机
形式化方法
B方法
高可信软件工程
基于ATL引擎的UML到Simulink模型转换方法研究
模型驱动开发
模型转换
ATL
UML
Simulink
UML状态图到B形式化规范的转换实现
UML状态图
B方法
转换工具
UML2 B
从UML状态图到PVS规范的自动转换、验证
UML状态图
PVS
层次自动机模型
模型验证
内容分析
关键词云
关键词热度
相关文献总数  
(/次)
(/年)
文献信息
篇名 元模型层次的 UML 动态子图到 Coq 形式规范的转换
来源期刊 计算机应用与软件 学科 工学
关键词 UML 动态子图 模型转换 元模型 Coq Kermeta
年,卷(期) 2016,(8) 所属期刊栏目 软件技术与研究
研究方向 页码范围 7-11,66
页数 6页 分类号 TP311
字数 4564字 语种 中文
DOI 10.3969/j.issn.1000-386x.2016.08.002
五维指标
作者信息
序号 姓名 单位 发文数 被引次数 H指数 G指数
1 李超 华东师范大学计算机科学技术系 15 35 4.0 5.0
2 杨宗源 华东师范大学计算机科学技术系 32 326 9.0 17.0
3 窦亮 华东师范大学计算机科学技术系 10 73 5.0 8.0
4 尹敏 华东师范大学计算机科学技术系 3 18 2.0 3.0
传播情况
(/次)
(/年)
引文网络
引文网络
二级参考文献  (5)
共引文献  (5)
参考文献  (5)
节点文献
引证文献  (2)
同被引文献  (0)
二级引证文献  (0)
2005(1)
  • 参考文献(0)
  • 二级参考文献(1)
2006(2)
  • 参考文献(1)
  • 二级参考文献(1)
2007(1)
  • 参考文献(0)
  • 二级参考文献(1)
2008(1)
  • 参考文献(0)
  • 二级参考文献(1)
2009(2)
  • 参考文献(1)
  • 二级参考文献(1)
2010(1)
  • 参考文献(1)
  • 二级参考文献(0)
2011(2)
  • 参考文献(2)
  • 二级参考文献(0)
2016(1)
  • 参考文献(0)
  • 二级参考文献(0)
  • 引证文献(1)
  • 二级引证文献(0)
2016(1)
  • 引证文献(1)
  • 二级引证文献(0)
2017(1)
  • 引证文献(1)
  • 二级引证文献(0)
研究主题发展历程
节点文献
UML 动态子图
模型转换
元模型
Coq Kermeta
研究起点
研究来源
研究分支
研究去脉
引文网络交叉学科
相关学者/机构
期刊影响力
计算机应用与软件
月刊
1000-386X
31-1260/TP
大16开
上海市愚园路546号
4-379
1984
chi
出版文献量(篇)
16532
总下载数(次)
47
  • 期刊分类
  • 期刊(年)
  • 期刊(期)
  • 期刊推荐
论文1v1指导