论文题目: 基于接口自动机的组合验证方法研究
论文类型: 博士论文
论文专业: 计算机科学与技术
作者: 文艳军
导师: 齐治昌
关键词: 形式验证,组合验证,模型检验,精化检验,接口自动机,体系结构描述语言
文献来源: 国防科学技术大学
发表年度: 2005
论文摘要: 形式验证是提高软件可靠性的有效手段。为了控制形式验证特别是模型检验和精化检验的复杂性,研究人员提出了组合方法,其基水思想是“分而治之”,即把大的、系统整体的验证任务分解为一组小的、系统局部的子任务,再逐个解决。组合方法的一个关键问题是如何处理构件之间的相互依赖关系给任务分解带来的困难。因为传统的模型不能在构件的行为描述中显式地表达构件对环境的假设,因此在组合验证时往往需要单独构造环境模块,这较大程度地增加了组合验证的复杂性。本文研究基于一种新的形式模型——接口自动机来进行软件设计的组合验证、特别是组合精化检验的方法。这种新的形式模型支持在构件的建模中显式地表达它的环境假设信息,因而更有利于组合验证方法的使用。 本文对接口自动机模型的组合验证开展了三个方面的研究。首先,为了揭示这种新的形式模型的本质,本文研究了它与传统的I/O自动机模型之间的关系。然后在此基础上对接口自动机理论进行了完善,并研究了该理论在软件体系结构的组合分析与验证中的应用。最后,提出了接口自动机上的一种新的组合精化检验方法。 论文的主要贡献概括如下: 1.建立了接口自动机上的精化关系与I/O自动机上的前向模拟之间的等价关系。接口自动机的精化关系是以一种交替的(Alternating)方式来定义的,它与I/O自动机的前向模拟之间差别很大,以至于有的学者认为接口自动机和I/O自动机分别属于两类不同的模型(还有部分原因出自并发组合上的差异):接口模型和构件模型。上述等价关系的建立揭示了这两类模型之间存在的本质联系,从理论上确立了基于接口自动机的构件设计与基于I/O自动机的构件验证的集成基础,并使得利用I/O自动机的理论和工具来解决接口自动机的问题成为可能。 2.完善了接口自动机理论。这主要体现在三个方面。其一,发现并修正了原理论中的一个错误;其二,受进程代数CCS中的“2/3模拟”概念的启发,本文引入了接口自动机上的“2/3交替模拟”概念,这使得接口自动机的精化关系具备了保持“无死锁”性质的能力,从而增强了接口自动机的应用价值;其三,引入了广义精化的概念,来描述构件的接口与构件的实现之间的精化关系,并建立了相应的组合精化检验规则。 3.基于完善以后的接口自动机理论重新定义了软件体系结构描述语言WRIGHT的语义,新的语义解释更加简洁、更加自然。WRIGHT是一种著名的体系结构描述语言,它原来的测试规则(用于保证系统的协调性)比较复杂,这主要是因为在这些规则中必须
论文目录:
摘要
Abstract
第一章 绪论
§1．1 研究背景
§1．2 研究现状及存在的问题
1．2．1 研究现状
1．2．2 存在的问题
§1．3 课题的研究思路和内容
§1．4 本文的主要贡献与创新
§1．5 论文结构
第二章 并发反应式系统的组合验证
§2．1 引言
§2．2 基本概念
§2．3 组合精化检验
2．3．1 分枝精化
2．3．2 线性精化
2．3．3 计算复杂性
§2．4 组合模型检验
2．4．1 (?)CTL~*和(?)VCTL性质
2．4．2 LTL性质
2．4．3 计算复杂性
§2．5 比较和讨论
§2．6 结论与展望
第三章 接口自动机与I／O自动机的集成
§3．1 引言
3．1．1 背景介绍
3．1．2 相关工作
3．1．3 本章的组织结构
§3．2 接口自动机
3．2．1 简介
3．2．2 定义
3．2．3 并发组合与相容性
3．2．4 精化关系
§3．3 异常自动机
§3．4 并发组合与相容性上的联系
§3．5 精化关系上的联系
§3．6 本章小结
第四章 对接口自动机理论的完善
§4．1 背景介绍
§4．2 接口自动机理论中的一个错误及其修正
4．2．1 错误
4．2．2 修正
§4．3 基本精化
4．3．1 闭接口自动机
§4．4 广义精化
§4．5 本章小结
第五章 WRIGHT的基于接口自动机的语义解释
§5．1 引言
§5．2 WRIGHT概况
§5．3 WRIGHT的基于接口白动机的语义解释
5．3．1 连接子的语义
5．3．2 联接(Attachments)的语义
5．3．3 相关的测试规则
5．3．4 性质
§5．4 与原语义解释的比较
§5．5 一种Web Services组合的解决办法
5．5．1 BPEL4WS协议
5．5．2 案例分析：网上超市
§5．6 本章小结
第六章 一种接口自动机的组合精化检验方法
§6．1 引言
§6．2 基本知识
§6．3 一种新的组合精化检验方法
§6．4 案例分析
§6．5 相对不可达迁移的计算
6．5．1 从接口自动机到标记迁移系统
6．5．2 迁移状态化
§6．6 本章小结
第七章 基于逆观察等价的组合可达性分析
§7．1 引言
§7．2 基本知识
§7．3 接口自动机的相对不可达迁移的计算(续)
§7．4 逆观察等价
§7．5 基于逆观察等价的组合可达性分析
§7．6 案例分析
7．6．1 简单令牌传递系统
7．6．2 令牌环互斥系统
§7．7 本章小结
第八章 结束语
§8．1 工作总结
§8．2 研究展望
论文发表情况
致谢
参考文献表
发布时间: 2005-11-07
参考文献
- [1].加权自动机的拓扑和代数特征研究[D]. 王拥兵.陕西师范大学2017
- [2].格值交替自动机的若干问题研究[D]. 魏秀娟.陕西师范大学2018
- [3].自动机和链编码的理论研究与应用[D]. 张薇.华东师范大学2006
- [4].基于动态系统计算的数字图像处理[D]. 巨志勇.同济大学2007
- [5].形式语言与自动机理论若干问题研究[D]. 陈文宇.电子科技大学2009
- [6].On-the-Fly和动态的软件模型检测方法研究[D]. 赵璐.哈尔滨工程大学2014
相关论文
- [1].面向UML的模型检验研究[D]. 董威.中国人民解放军国防科学技术大学2002
- [2].基于形式语义的构件组装与演化研究[D]. 龚洪泉.复旦大学2005
- [3].基于形式规格说明的统一软件建模系统的研究[D]. 刘静.上海大学2005
- [4].面向构件的复杂软件系统中动态配置技术的研究[D]. 窦蕾.国防科学技术大学2005
- [5].模型检验的反例解释[D]. 沈胜宇.国防科学技术大学2005
- [6].安全协议形式化验证技术的研究与实现[D]. 李梦君.国防科学技术大学2005
- [7].程序正确性验证的几个问题[D]. 范年柏.湖南大学2005
- [8].基于体系结构的软件动态演化研究[D]. 李长云.浙江大学2005
- [9].构件化嵌入式软件设计的分析与验证[D]. 胡军.南京大学2005
- [10].基于自动机的时间系统形式验证技术[D]. 许庆国.上海大学2007