基于图转换的关联属性规约模型检测及其支撑平台研究

发布时间：2017-08-18 12:35

  本文关键词：基于图转换的关联属性规约模型检测及其支撑平台研究

  更多相关文章： 图转换 模型检测 关联属性

【摘要】：图转换系统广泛应用在软件建模和分析阶段,现有的图转换系统通常采用命题式时序逻辑(propositional temporal logic)表达待验证规约,但是该逻辑无法直接表达建模实体随时间演化的关联属性,提出一种轻量级可支持通用图转换系统中关联属性规约的验证方法,通过引入标记节点及相关属性,将包含相应关联属性的规约公式等价转换为常规命题式时序逻辑,从而可以间接支持该类型规约的验证。以流行的对象式图转换模型检测工具GROOVE为平台,结合启发案例,通过实验验证了所提出方法的可行性。由于引入标记节点及属性来完成关联属性规约的验证会带来额外的状态数,加剧状态空间爆炸问题,增加系统开销,应用对称化简以及层次化技术,优化模型结构,减少状态数,来节约系统的时间开销。结合具体实例,通过实验对比,展示出对称化简以及图形层次化技术在图转换系统的模型检测中减少状态空间的有效性。此外,为提供更好的可用性,采用图形化编辑框架GEF(Graphic Editing Framework),以及Eclipse插件式架构,开发出一个支撑平台。根据所提出方法,该平台可以展示图转换工具基本界面结构,并能够自动地引入标记节点及其相应属性来解决关联属性的验证难题,从而可支持对该类系统的验证工作。
【关键词】：图转换 模型检测 关联属性
【学位授予单位】：南京航空航天大学
【学位级别】：硕士
【学位授予年份】：2015
【分类号】：TP311.52
【目录】：

• 摘要4-5
• Abstract5-11
• 注释表11-12
• 缩略词12-13
• 第一章 绪论13-17
• 1.1 研究背景13-15
• 1.1.1 模型检测13
• 1.1.2 图转换模型检测13-15
• 1.2 研究内容15-16
• 1.3 研究组织结构16-17
• 第二章 基本概念17-24
• 2.1 图转换综述17-19
• 2.2 图转换模型检测工具GROOVE19-21
• 2.3 时序逻辑21-22
• 2.4 GEF框架综述22-24
• 第三章 包含关联属性的规约验证24-42
• 3.1 问题描述24-25
• 3.2 解决方法25-30
• 3.3 状态空间缩减方法30-35
• 3.3.1 对称化简30-32
• 3.3.2 层次式图转换32-35
• 3.4 验证结果35-42
• 3.4.1 示例 1：车站管理系统的模型检测35-39
• 3.4.2 示例 2：餐厅服务系统的模型检测39-42
• 第四章 支撑平台构建42-58
• 4.1 开发语言及平台选择42-43
• 4.2 框架的选择43
• 4.3 GEF对MVC模式的实现手段43-45
• 4.4 系统整体设计45-51
• 4.4.1 系统整体需求45-46
• 4.4.2 Model层设计46-49
• 4.4.3 Control层设计49-50
• 4.4.4 View层设计50-51
• 4.5 系统细节实现51-58
• 4.5.1 规则的实现51-52
• 4.5.2 属性栏的实现52-53
• 4.5.3 分页实现53-54
• 4.5.4 针对包含关联属性规约验证的处理方法54-56
• 4.5.5 测试56-58
• 第五章 总结58-59
• 参考文献59-63
• 致谢63-64
• 在学期间的研究成果及发表的学术论文64

【相似文献】

中国期刊全文数据库 前10条

1 戎玫;张广泉;;模型检测新技术研究[J];计算机科学;2003年05期

2 肖健宇;张德运;郑卫斌;;过程提取用于改善程序模型检测的可伸缩性[J];西安交通大学学报;2006年06期

3 袁志斌;徐正权;王能超;;软件模型检测中的抽象[J];计算机科学;2006年07期

4 刘吉锋;孙吉贵;;基于抽象-验证-细化范例的软件模型检测[J];计算机科学;2006年12期

5 化志章;吴传孙;揭安全;薛锦云;;软件模型检测新技术研究[J];微计算机信息;2007年36期

6 王飞明;胡元闯;董荣胜;;模型检测研究进展[J];广西科学院学报;2008年04期

7 邝宏斌;罗贵明;;并行软件模型检测[J];计算机工程;2008年19期

8 何恺铎;顾明;宋晓宇;李力;李江;;面向源代码的软件模型检测及其实现[J];计算机科学;2009年01期

9 林璇;;模型检测方法在入侵检测中的应用研究[J];现代计算机(专业版);2009年02期

10 顾滨兵;;一种软件模型检测方法及其原型系统[J];微计算机应用;2010年11期

中国重要会议论文全文数据库 前5条

1 高静;曹子宁;;基于空间逻辑和计算树逻辑的模型检测[A];2009年中国高校通信类院系学术研讨会论文集[C];2009年

2 许梅;曹子宁;;基于谓词μ演算和空间逻辑的模型检测算法研究[A];2009年中国高校通信类院系学术研讨会论文集[C];2009年

3 何青;骆翔宇;苏开乐;;对弈必胜策略的符号化模型检测[A];2006年全国理论计算机科学学术年会论文集[C];2006年

4 王飞明;胡元闯;董荣胜;;模型检测中状态爆炸及其优化策略研究[A];广西计算机学会2008年年会论文集[C];2008年

5 陈道喜;张广泉;陈冬火;;NSPK协议的Spin模型检测[A];2008年全国开放式分布与并行计算机学术会议论文集(下册)[C];2008年

中国博士学位论文全文数据库 前10条

1 江华;界程演算模型检测[D];贵州大学;2008年

2 林荣德;移动界程演算及模型检测应用的关键问题研究[D];华南理工大学;2010年

3 刘剑;传值进程与移动进程的模型检测方法[D];中国科学院研究生院（软件研究所）;2005年

4 刘志锋;模型检测中关键技术的研究及其应用[D];南京大学;2011年

5 朱维军;时间区间时序逻辑模型检测：理论、算法及应用[D];西安电子科技大学;2011年

6 尹良泽;基于SAT的组合迁移系统模型检测技术研究[D];清华大学;2014年

7 陈冬火;超协调时序逻辑及其模型检测方法[D];中国科学院研究生院（成都计算机应用研究所）;2006年

8 田聪;命题投影时序逻辑的判定性、复杂性、表达性及模型检测[D];西安电子科技大学;2010年

9 黄宏涛;基于懒惰切片的模型检测技术研究[D];哈尔滨工程大学;2012年

10 刘金卓;基于符号化模型检测的软件演化过程模型验证[D];云南大学;2013年

中国硕士学位论文全文数据库 前10条

1 李永亮;基于DNA计算的CTL模型检测方法研究[D];郑州大学;2015年

2 杨树峰;基于统计模型检测的无线传感器网络协议建模与分析[D];郑州大学;2015年

3 张兴兴;基于广义可能性测度的互模拟及CTL不动点语义[D];陕西师范大学;2015年

4 王彬;基于多值模型检测的SaaS应用测试及其自动化研究[D];陕西师范大学;2015年

5 王凯;基于模型检测多反例对软件进行调试[D];电子科技大学;2015年

6 邓楠轶;基于广义可能性测度的模型检测器GPoCheck的设计与实现[D];陕西师范大学;2015年

7 张恒;多值模型检测器的研究与实现[D];陕西师范大学;2015年

8 高毅;不同模型检测下信号并串转换模块功能建模的研究[D];电子科技大学;2014年

9 崔晓爽;基于GSTE模型检测的信号并串转换模块功能验证的研究[D];电子科技大学;2014年

10 许落汀;基于BDDs的离散实时时态逻辑RTCTL*的符号化模型检测及证据生成[D];华侨大学;2015年

，

本文编号：694606