扩展π演算的建模、验证与测试

发布时间：2017-05-03 08:12

  本文关键词：扩展π演算的建模、验证与测试，由笔耕文化传播整理发布。

【摘要】：时间相关移动并发系统是以并发性、移动性、时间相关性和异构性等为主要特征的计算系统。对于这类系统,特别是安全攸关的时间相关移动并发系统,如移动支付系统、移动通信系统、交通控制系统等,其失误和崩溃可能会造成重大损失,因此时间相关移动并发系统的正确性、安全性等质量属性受到人们的普遍重视。对时间相关移动并发系统采用以严格数学理论为支撑的形式化方法进行建模、验证与测试是行之有效的减少系统设计错误和保证系统质量的重要途径。进程代数,作为形式化方法的代表,是一种重要的用于对并发系统进行建模和验证的技术。由于所面向的领域和应用背景的不同,涌现出很多进程代数的分支和变种,其中演算就是用于建模移动性的重要的分支。近年来,由于新型网络技术和信息技术的不断发展,使得能够建模和验证移动系统的演算得到人们的广泛关注。但是,演算在对系统建模时并未考虑到动作执行所占用的时间以及系统在某个状态所持续的时间,故而,使得它不适于对时间相关系统进行建模、验证和测试。为了对时间相关移动并发系统进行建模和验证,本文研究了添加时间相关特性的扩展的演算。在此基础上,提出采用扩展演算为时间相关移动并发系统进行建模和推演的方法。进一步地,为了对扩展演算建模的系统进行自动验证,提出将扩展演算转换为建模、仿真验证语言MSVL的方法。此外,为了对扩展演算建模的系统进行测试,文章还给出了采用扩展演算的测试用例生成方法。所取得的研究成果主要有以下几个方面。(1)建立了带区间动作前缀的扩展演算p-π,定义了p-π的语法和操作语义,给出了p-π的代数性质和时间相关性质并对其进行了证明。在此基础上给出了p-π对时间相关行为的建模。此外,还通过实例对p-π的应用效果和相应性质所起的作用进行了分析和说明。(2)提出了采用扩展演算对时间相关移动并发系统进行建模和推演的方法。采用区间动作前缀和瞬时动作前缀分别描述系统的时间相关行为和交互行为,并通过操作算子将子进程进行复合,然后利用操作规则构造出系统的时间相关标记迁移系统和可接受的执行路径,基于上述迁移系统和执行路径完成对系统性质的推演。通过移动车辆控制系统的分析表明,所提方法可对时间相关移动并发系统进行有效建模和推演,保证时间相关移动并发系统的可靠性。(3)提出了从扩展演算p-π到MSVL的转换方法。为了完成转换,先在MSVL中对通道和通信原语进行了定义。基于该定义,给出了从p-π到MSVL的结构化转换规则,并对二者采用的通信机制间存在的一致性进行了证明。为了说明转换的合理性,文章还证明在p-π进程和MSVL的格局间存在互模拟关系。这样,通过转换,就可以借助MSVL建模仿真验证工具完成对p-π进程的验证。(4)提出了基于扩展演算的测试用例生成方法。采用p-π为时间相关并发系统建模并由p-π的操作规则构造出系统模型的时间相关标记迁移系统。基于时间相关标记迁移系统和用例规约生成测试用例,测试用例的生成满足执行动作覆盖准则、路径覆盖准则和时间约束覆盖准则,并给出了测试用例的选择策略。同时通过p-π的验证方法,还保证了所产生的测试用例的正确性。
【关键词】：进程代数 π演算 规范 形式验证 基于模型的测试
【学位授予单位】：西安电子科技大学
【学位级别】：博士
【学位授予年份】：2015
【分类号】：TP301
【目录】：

• 摘要5-7
• ABSTRACT7-11
• 缩略词对照表11-17
• 第一章 绪论17-31
• 1.1 研究背景与意义17-18
• 1.2 形式化模型18-21
• 1.2.1 基于图形化的模型18-19
• 1.2.2 基于文本的模型19-21
• 1.3 形式化验证21-23
• 1.3.1 模型检测21-22
• 1.3.2 定理证明22-23
• 1.4 基于模型的测试23-25
• 1.4.1 基于非形式化模型的测试24
• 1.4.2 基于形式化模型的测试24-25
• 1.5 相关研究工作与本文研究目的25-28
• 1.5.1 相关研究工作25-28
• 1.5.2 本文研究目的28
• 1.6 论文的主要工作与组织结构28-31
• 第二章 π演算与MSVL31-45
• 2.1 π演算31-35
• 2.1.1 π演算的语法和语义31-33
• 2.1.2 π演算的移动性33-34
• 2.1.3 π演算的研究进展34-35
• 2.2 建模、仿真与验证语言MSVL35-44
• 2.2.1 投影时序逻辑PTL35-38
• 2.2.2 MSVL38-44
• 2.3 本章小结44-45
• 第三章 扩展π演算 p-π45-65
• 3.1 p-π的语法45-46
• 3.2 p-π的语义46-50
• 3.2.1 结构等价46-47
• 3.2.2 操作规则47-50
• 3.3 p-π的性质50-56
• 3.3.1 代数性质50-55
• 3.3.2 时间相关性质55-56
• 3.4 时间相关行为的建模56-58
• 3.4.1 时间延迟56-57
• 3.4.2 超时处理57
• 3.4.3 中断处理57-58
• 3.5 实例58-63
• 3.6 本章小结63-65
• 第四章 时间相关移动并发系统的建模与推演65-75
• 4.1 系统描述65-67
• 4.2 系统建模67-71
• 4.3 系统推演71-73
• 4.3.1 基于操作规则的系统迁移71-72
• 4.3.2 基于系统迁移的系统推演72-73
• 4.4 本章小结73-75
• 第五章 从p-π到MSVL的结构化转换方法75-95
• 5.1 MSVL的通道和通信原语76-77
• 5.2 从p-π到MSVL的转换77-87
• 5.2.1 名字和原子命题的转换78
• 5.2.2 进程的转换78-84
• 5.2.3 Interleaving和True Concurrency间的一致性84-86
• 5.2.4 注意86-87
• 5.3 转换的合理性87-90
• 5.4 应用实例90-94
• 5.4.1 系统建模90-91
• 5.4.2 转换91-92
• 5.4.3 验证92-94
• 5.5 本章小结94-95
• 第六章 采用扩展π演算的测试用例生成方法95-109
• 6.1 时间相关标记迁移系统96-97
• 6.2 测试用例生成97-103
• 6.2.1 执行路径97-99
• 6.2.2 可观察动作与不可观察动作99
• 6.2.3 覆盖准则99
• 6.2.4 互模拟进程替换99-100
• 6.2.5 基于对象约束语言的用例规约100
• 6.2.6 测试用例生成算法100-101
• 6.2.7 测试用例选择策略101-103
• 6.3 应用实例103-107
• 6.3.1 OBS的p-π系统进程103-104
• 6.3.2 系统的TDLTS104-105
• 6.3.3 测试用例生成105-107
• 6.4 相关方法比较107
• 6.5 本章小结107-109
• 第七章 总结与展望109-113
• 7.1 全文总结109-110
• 7.2 未来的研究工作110-113
• 附录A113-115
• 参考文献115-125
• 致谢125-127
• 作者简介127-128
• 1. 基本情况127
• 2. 教育背景127
• 3. 攻读博士学位期间的研究成果127-128

【相似文献】

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

1 路晓丽;葛玮;陈新丽;郝克刚;;支持共享和复用的测试用例库系统的设计[J];计算机科学;2006年05期

2 胡珊;杨丰玉;张晔;刘琳岚;;基于测试项抽取的测试用例复用方法[J];微电子学与计算机;2010年01期

3 张德平;查日军;;划分测试用例选择的风险决策方法[J];计算机应用研究;2010年12期

4 杨翊;陈挺;许峥;;证券软件的测试用例设计充分性实践[J];中国证券期货;2012年07期

5 张智轶;陈振宇;徐宝文;杨瑞;;测试用例演化研究进展[J];软件学报;2013年04期

6 杨悦;秦湘河;杨永安;郭荣;;航天测控软件测试用例标准及应用研究[J];无线电工程;2013年09期

7 王侃,卢庆龄,彭艳丽;测试用例自动生成的链方法研究与实现[J];装甲兵工程学院学报;2001年03期

8 李顺华;测试用例管理方法探讨[J];飞航导弹;2001年05期

9 徐仁佐,陈斌,陈波,吴闽泉,熊忠伟;构造面向对象软件可复用测试用例的模式研究[J];武汉大学学报(理学版);2003年05期

10 陈绍英;金成姬;;性能测试用例[J];程序员;2004年11期

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

1 王道堂;林春哲;张凯;;软件测试用例构造方法与手段[A];计算机技术在工程建设中的应用——第十二届全国工程建设计算机应用学术会议论文集[C];2004年

2 李磊;曹先彬;;基于进化的软件测试用例生成方法[A];2005年“数字安徽”博士科技论坛论文集[C];2005年

3 徐李勤;王洁宁;;基于层次有色Petri网的软件测试用例选取研究[A];全国第二届信号处理与应用学术会议专刊[C];2008年

4 林春哲;张凯;王道堂;;软件测试用例设计分析[A];计算机技术在工程建设中的应用——第十二届全国工程建设计算机应用学术会议论文集[C];2004年

5 张侠影;李志蜀;;一种优化的测试用例约简方法[A];2008'中国信息技术与应用学术论坛论文集（一）[C];2008年

6 张德平;聂长海;徐宝文;;划分测试用例选择策略研究[A];第五届中国测试学术会议论文集[C];2008年

7 郭从颖;;场景驱动测试用例设计及其测试自动化技术研究[A];中国计量协会冶金分会2008年会论文集[C];2008年

8 郭从颖;;场景驱动测试用例设计及其测试自动化技术研究[A];2008全国第十三届自动化应用技术学术交流会论文集[C];2008年

9 周晓燕;李兵;潘伟丰;覃叶宜;;基于错误传播概率网络的软件回归测试用例选择[A];第五届全国复杂网络学术会议论文（摘要）汇集[C];2009年

10 万琳;张威;马雪雁;陈曼青;;基于路径的测试用例自动生成技术[A];第十届全国容错计算学术会议论文集[C];2003年

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

1 深圳市信息无障碍研究会 戴杰;“听”软件的IT工程师[N];人民政协报;2014年

2 谢敏 沈雪芳 戴金龙;解决软件测试的近忧和远虑[N];计算机世界;2005年

3 计算机世界实验室 韩勖;拨云见日[N];计算机世界;2008年

4 《网络世界》记者 郑楠;ONF测试步伐有条不紊[N];网络世界;2014年

5 ;找错[N];计算机世界;2002年

6 信息产业部软件与集成电路促进中心 于明邋唐仕武;驶入测试“快车道”[N];计算机世界;2007年

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

1 罗玲;扩展π演算的建模、验证与测试[D];西安电子科技大学;2015年

2 李丽;航天相机主控软件测试用例自动生成技术的研究[D];中国科学院研究生院（长春光学精密机械与物理研究所）;2010年

3 黄如兵;组合测试用例的自适应随机生成与优先级排序方法研究[D];华中科技大学;2013年

4 张娟;软件测试中测试用例复用的研究[D];上海大学;2012年

5 游亮;回归测试用例选择技术研究[D];华中科技大学;2012年

6 谢晓东;基于模型比较的软件测试用例生成方法研究[D];华中科技大学;2007年

7 李根;基于动态测试用例生成的二进制软件缺陷自动发掘技术研究[D];国防科学技术大学;2010年

8 邢颖;测试用例自动生成的分支限界算法及实验研究[D];北京邮电大学;2014年

9 钱思佑;图形用户界面测试中相关问题研究[D];中国科学技术大学;2010年

10 李军义;软件测试用例自动生成技术研究[D];湖南大学;2008年

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

1 田春艳;基于灰色关联逼近理想解方法的测试用例评价模型研究[D];昆明理工大学;2009年

2 唐海鹏;基于Additional策略回归测试用例优先级排序优化研究[D];西南大学;2015年

3 陈梦云;基于圈复杂度和调用次数的测试用例排序方法[D];上海师范大学;2015年

4 姚瑞超;广东电网测试用例自动生成工具的研究与设计[D];华南理工大学;2015年

5 张泽林;基于数据挖掘的软件多故障定位与分析技术[D];南京理工大学;2015年

6 邹炳松;嵌入式软件的图形化测试用例生成系统设计与实现[D];哈尔滨工业大学;2015年

7 李锦程;基于微信平台的医疗就诊系统设计与实现[D];哈尔滨工业大学;2015年

8 赵群;软件错误定位中的巧合正确性问题研究[D];哈尔滨工业大学;2015年

9 常龙辉;Web应用的测试用例优化生成与优先级技术[D];上海大学;2015年

10 王令赛;基于粒子群优化算法的测试用例生成技术研究[D];中国矿业大学;2015年

  本文关键词：扩展π演算的建模、验证与测试，，由笔耕文化传播整理发布。

本文编号：342669