模型精化过程中模型间一致性检测研究

发布时间：2017-09-19 00:03

  本文关键词：模型精化过程中模型间一致性检测研究

  更多相关文章： 模型精化 模型检测 一致性检测 属性抽取 线性时序逻辑

【摘要】：模型精化是软件工程中基于模型驱动开发的关键问题之一,被广泛应用于基于模型驱动开发方法中。若在初始模型中引入过多细节会使得开发和测试不易管理,因此对于那些大型复杂系统的建模很难做到一步到位,在实际的开发建模过程中往往采用模型精化的技术。所谓模型精化即在原模型的基础上添加更多的细节,逐步细化,模型从刚开始的比较抽象变得逐渐具体化。如何保证模型精化过程中模型间的一致性,一直是工业界和学术界高度关注的问题之一。模型精化过程中模型间的一致性是正确建模的必要前提,为了保证精化后的模型和精化前是一致的,需要对精化前后的模型进行一致性检验。由于模型具有复杂性和抽象性,包含不一致信息的模型将导致开发后期阶段编码的矛盾和错误,一致性检验的重要意义就在于可以在软件设计的早期阶段发现不一致问题,减少生成代码后出错所产生的代价。传统的模型精化过程中模型间一致性检测方法只关注于模型自身的语法、语义、结构方面的正确性,死锁(Deadlock)检测,不变式(Invariants)保持性检测等,而不关注于模型间行为方面的一致性检测。然而,系统模型间的不一致往往存在于系统行为的各个方面,使用传统的一致性检测方法很难一一找出这些不一致。为此,本文提出利用系统行为属性来刻画系统行为状态的改变,并结合模型检测的方法来检测模型间的行为一致性。我们假设精化前的模型能够忠实地反映用户需求,但是在模型精化过程中有时会发生精化后的模型丢失或违反精化前模型中的相关行为。为此,我们首先对精化前模型分析生成抽象测试用例,并从中抽取出能够表达系统行为变迁的系统行为并表示为系统行为属性,然后根据精化后的模型抽取模型精化关系并进一步更新系统属性,最后使用这些系统行为属性来验证精化后的模型是否依然满足其代表的系统行为,如果不满足则说明模型间存在不一致行为,可以通过生成的反例路径找出不一致的位置,修改不一致后,再迭代进行验证,直到精化后的模型能够满足这些系统属性为止。最后,为了分析本文方法的有效性,选取了三个常用系统(Celebrity、Kettle、 VOBC)进行一致性检测,为了模拟出现的不一致情况,人为注入不一致,再利用本文所提出的方法进行一致性检测,实验结果表明使用本文方法可以有效找出模型精化前后的大多数不一致行为,从而实现了使用系统行为属性的方法来检测模型间的一致性,提高了模型间一致性检测的有效性。
【关键词】：模型精化 模型检测 一致性检测 属性抽取 线性时序逻辑
【学位授予单位】：华东师范大学
【学位级别】：硕士
【学位授予年份】：2016
【分类号】：TP311.52
【目录】：

• 摘要6-8
• ABSTRACT8-12
• 第一章 引言12-18
• 1.1 研究背景和意义12-13
• 1.2 国内外研究现状13-14
• 1.3 关键问题与技术路线14-15
• 1.4 主要工作与特色之处15-16
• 1.5 本文的组织结构16-18
• 第二章 相关概念介绍18-21
• 2.1 模型检测18
• 2.2 模型精化18-19
• 2.3 EVENT-B模型19-20
• 2.4 线性时序逻辑(LINEAR TEMPORAL LOGIC,LTL)20
• 2.5 本章小结20-21
• 第三章 模型系统实例21-28
• 3.1 模型系统概述21-22
• 3.2 电烧水壶模型系统22-26
• 3.3 可能出现的不一致26-27
• 3.4 本章小结27-28
• 第四章 模型间一致性检测方法28-45
• 4.1 基本流程28-29
• 4.2 抽象测试用例生成29-32
• 4.3 系统行为属性抽取32-37
• 4.4 精化关系抽取37-42
• 4.5 系统行为属性验证42-43
• 4.6 本章小结43-45
• 第五章 实验分析45-49
• 5.1 实验内容45
• 5.2 实验数据与实验环境45-47
• 5.3 实验结果分析47-48
• 5.4 本章小结48-49
• 第六章 总结与展望49-52
• 6.1 本文总结49-50
• 6.2 未来工作展望50-52
• 附录1 攻读学位期间发表的学术论文目录52-53
• 附录2 生成的部分线性时序逻辑(LTL)示例53-56
• 参考文献56-60
• 致谢60-61

【相似文献】

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

1 祁方民;;Petri网结点精化及其应用[J];计算机与现代化;2014年07期

2 王云峰 ,庞军 ,查鸣 ,杨朝晖 ,郑国梁;精化演算支撑工具的分析[J];计算机应用与软件;2002年02期

3 刘瑜,张世琨,邬伦,叶燕林;地理信息系统中的设计模式——以过滤和精化为例[J];北京大学学报(自然科学版);2001年06期

4 熊建;陈晓克;;基于Wiki技术可持续精化精品课教学平台[J];福建电脑;2010年12期

5 杨朝晖;王云峰;郑国梁;;精化演算支撑工具PRT的研究[J];计算机科学;2000年03期

6 ;[J];;年期

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

1 周鑫;;面对新形势、树立新观念、迎接新挑战——谈企业职工面对“精化分立、分业经营”新形势的感想[A];陕西省体制改革研究会2006-2007优秀论文集[C];2007年

2 高阳;王敏中;;拉伸矩形梁的精化理论[A];北京力学会第11届学术年会论文摘要集[C];2005年

3 高阳;王敏中;;横观各项同性压电矩形直梁的精化理论[A];中国力学学会学术大会'2005论文摘要集（下）[C];2005年

4 赵红丽;范景辉;郭小方;刘广;陈建平;;CR辅助的基线参数精化方法研究[A];第十七届中国遥感大会摘要集[C];2010年

5 江东;王庆宾;王凯;;重力场精化的空间插值方法研究[A];中国测绘学会2010年学术年会论文集[C];2010年

中国重要报纸全文数据库 前10条

1 罗平华;彩虹精化气雾漆龙头今日挂牌[N];证券时报;2008年

2 证券时报记者 罗平华;彩虹精化出口收入逆势增长三成[N];证券时报;2009年

3 证券时报记者 向南;彩虹精化 涉足室内环保业务[N];证券时报;2010年

4 记者 翟敏;彩虹精化上半年业绩平平 管理层就“巨额订单”事件致歉[N];上海证券报;2011年

5 记者 王健杰;彩虹精化营收内降外增[N];北京商报;2009年

6 中国空空导弹研究院 综合管理处;精化军品能力 优化民品结构[N];中国航空报;2004年

7 本报通讯员 周善良 记者 李雨农;精化分立 一所多制[N];中国航空报;2002年

8 武连寅邋蔡军;淮化精化再次入选国家高新企业[N];中国化工报;2007年

9 记者 孙燕飚　刘琼;万润精化再上会 日德企业“锁喉”难改观[N];第一财经日报;2011年

10 记者 况玉清;彩虹精化虚假陈述案下月开庭[N];北京商报;2012年

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

1 陈桂芝;解大规模非对称矩阵特征问题的一些精化算法[D];大连理工大学;2000年

2 梁红瑾;并发程序精化验证及其应用[D];中国科学技术大学;2014年

3 牛大田;计算大规模矩阵部分奇异值分解的精化Lanczos型算法[D];大连理工大学;2003年

4 梁坤;高灵敏度GPS接收技术中几个关键问题的研究[D];中国科学院研究生院（国家天文台）;2008年

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

1 钱洁;轨旁系统的形式化建模精化与验证[D];华东师范大学;2015年

2 刘婷婷;双层梁的精化理论[D];辽宁科技大学;2015年

3 王玲;模型精化过程中模型间一致性检测研究[D];华东师范大学;2016年

4 刘稳;隐式重启和精化的全局Lanczos方法与块Lanczos方法[D];南京航空航天大学;2014年

5 付亚军;面向多主体的基于政策的运行机制研究[D];湖南大学;2009年

6 吴钢;解大规模非对称矩阵特征问题Lanczos方法的两种精化版本[D];大连理工大学;2001年

，

本文编号：878298