.Ijb133 { display:none; } 进程互模拟验证算法的研究与实现( 毕业论文 12600字) 【摘要】伴随着计算机网络的诞生，分布式计算应用日益广泛
远程过程调用、网格、web服务、移动Agent等分布计算技术已经不再是陌生的术语，它们得到了越来越广泛的应用
这些新的分布式计算技术给我们带来了更强大的计算能力，更高的灵活性和方便，但随之而来的是一系列的程序验证问题
由于并发分布式系统本身非常复杂，因此其开发过程不仅难度大、效率低、周期长，而且很难避免和发现其中隐含的错误和缺陷
对于安全攸关系统(safety critical systems)，其失误和崩溃可能会造成生命和财产的重大损失，甚至导致灾难
形式化方法被公认为是一种行之有效的减少设计错误、提高系统可靠性的重要途径
对此，学者们采用了形式化的方法为系统建模，描述规范及验证系统是否满足规范
其中，进程代数是一中常用的有效工具，它可用于建模及描述规范
本文将给出算法，验证两个进程是否互模拟，从而验证系统是否满足规范
远程过程调用、网格、web服务、移动Agent等分布计算技术已经不再是陌生的术语，而是得到了越来越广泛的应用
这些新的分布式计算技术给我们带来了更强大的计算能力，更高的灵活性和方便，但随之而来的是一系列的程序验证问题
由于并发分布式系统本身非常复杂，因此其开发过程不仅难度大、效率低、周期长，而且很难避免和发现其中隐含的错误和缺陷
对于安全攸关系统(safety critical systems)，其失误和崩溃可能会造成生命和财产的重大损失，甚至导致灾难
软件开发包括需求、设计、编码和测试等阶段，有时也包括维护阶段
传统的软件开发方法由于大量的使用自然语言和多种图形符号，结果是尽管经历了仔细的复审，最后的系统规约说明中仍然包歧义的、含糊的、矛盾的、不完整的需求描述及混乱的抽象层次
在传统的软件开发过程中，前期各阶段的工作成果都是自然语言描述的“文档”，只有最后开发阶段的成果是形式化的程序
非形式的前期工作成果（文档）只能由人阅读、理解和讨论，无法严格的分析和推理（这方面情况也正在变化）
由于程序的复杂性，对其进行分析和推理非常困难
软件形式化方法最早可追溯到20世纪50年代后期对于程序设计语言编译技术的研究，即J.Backus提出BNF描述Algol60语言的语法，出现了各种语法分析程序自动生成器以及语法制导的编译方法，使得编译系统的开发从“手工艺制作方式”发展成具有牢固理论基础的系统方法
形式化方法的研究高潮始于 20世纪60年代后期，针对当时所谓“软件危机”,人们提出种种解决方法,归纳起来有两类：一是采用工程方法来组织、管理软件的开发过程；二是深入探讨程序和程序开发过程的规律，建立严密的理论，以其用来指导软件开发实践
前者导致“软件工程”的出现和发展，后者则推动了形式化方法的深入研究
经过30多 年的研究和应用，如今人们在形式化方法这一领域取得了大量、重要的成果，从早期最简单的形式化方法——一阶谓词演算方法到现在的应用于不同领域、不同阶段的基于逻辑、状态机、网络、进程代数、代数等众多形式化方法
形式化方法的发展趋势逐渐融入软件开发过程的各个阶段，从需求分析、功能描述(规约)、(体系结构/算法)设计、编程、测试直至维护
用于开发计算机系统的形式化方法是描述系统性质的基于数学的技术，这样的形式化方法提供了一个框架，可以在框架中以系统的而不是特别的方式刻划、开发和验证系统
如果一个方法有良好的数学基础，那么它就是形式化的
这个基础提供一系列精确定义的概念，如：一致性和完整性，以及定义规范的实现和正确性
形式化方法的本质是基于数学的方法来描述目标软件系统属性的一种技术
不同的形式化方法的数学基础是不同的，有的以集合论和一阶谓词演算为基础（如Z和 VDM），有的则以时态逻辑为基础
形式化方法需要形式化规约说明语言的支持
在形式化过程中应该对系统进行一定程度的抽象，去除不必要的信息
描述（Specification）：阐明所要验证的性质
注意到模型检测只能够检查模型（系统）是否满足给定的公式，因而所提供的公式能否完全正确地刻画所关心的性质是得到正确检测结果的必要前提
验证（Verification）：狭义的验证过程是指状态空间的搜索过程
这部分工作是可以完全自动完成的
广义的验证包括搜索（及报错），修改系统，再搜索，再修改……的过程，其中对于错误信息的分析和对系统的修改和重新建模的工作是需要用户参与的
上述几点之间存在着紧密的联系
例如在进行建模时，系统的形式化抽象既需要考虑到验证时的效率和时空限制，从而尽可能地忽略冗余信息，又应该突出与待验证性质相关的特征
从某种意义上说，当验证过程给出反例时可以确信模型与性质不符，因此“证否”的工作是又验证步骤来完成的；但是肯定的验证结果是否能够“证实”，还取决于系统建模和性质描述两步
在形式化验证过程中，验证用于描述系统的模型与描述性质的模型是否等价是一个重要问题，本文将就此展开研究
随着计算机的发展，尤其是分布式系统与网络的出现，并发现象和交互反应的存在已不容忽视
传统的输入/输出函数模型无法胜任对这些计算现象的刻画
因此，如何描述并行的、交互反应使分布式的系统从上世纪60年代起成为了一个研究的热点，并逐步形成了所谓并发理论的研究领域，它已成为计算机科学的主流研究方向之一
最早的并发模型是Petri与1962年在其博士论文中提出的
他给出了一种网状结构信息流模型——Petri网
Petri网既可以作为一种图形工具来模拟系统的动态行为和并发活动，又可以作为数学工具来建立状态方程、代数方程以及系统行为的其他代数模型，是一种应用广泛的理论工具
除Petri网理论外，最著名、研究的最广泛的并发模型就是进程代数
进程代数中并发系统的行为往往被描述为状态转换图加以考察，其中最简单的描述形式之一是带标记的转换系统（LTS，labeled transition system）
当不需要考察进程代数中的独立性、协调性等特殊性质的时候，LTS可以展现进程代数的一般性质
当考察进程代数的特殊性质时，一些更为复杂的模型被给出
它引入了复合（parallel composition）、和（sum）、以及约束（restriction）等算子下面我们先介绍一些基本概念和符号
CSP中的进程可由如下的BNF范式定义： ，（其中 ）
所有进程构成的集合记为Proc，一般用P, Q…表示进程
0表示不能执行任何动作的进程
带前缀（prefix）的进程 有唯一的由前缀 所表达的能力，只有当 执行过之后 才能进行演化，例如： .P表示该进程可以执行一个外界不可观测的动作，然后再执行P
和 表示不确定的选择， 的能力包含了 和 两部分的能力，当它执行了其中的一部分的能力后，另一个部分就被会抛弃
复合进程 表示 和 并发执行， 、 既可以分别与外界交互也可以两者之间进行交互
1.2.1 CSP的归约语义 归约语义描述了一个系统内部进化的最小的一步，它不考虑系统与环境之间的交互
下面，我们首先介绍一个辅助概念——结构化同余（structural congruence），进而给出进程上归约（reduction）关系的定义
而带标记的转换系统LTS（Labeled Transition System）不但可以刻画系统的内部演化，而且可以描述系统与环境的交互
在进程代数中，LTS通常是由一组SOS（Structural Operational Semantics）规则加以规范的
定义: 带标记的转换系统是一个三元组 ，其中S为状态集，T为转换标记集，对任意的 ，转换关系 称为标记为t的转换
直观上， 表示状态s经过一个标记为t的转换到达状态s’
在进程代数中，一般用进程表示状态，动作表示转换标记
定义: 为一个带标记的转换系统，其中Proc表示进程的集合，Act表示动作集，转换关系 由表2.3中的SOS规则所规范
规则（Sum-L）和（Sum-R）表明如果和的某一部分可以经过一个动作，到达某个新状态，则和也可以执行该动作并到达同样的状态
规则（Par-L）和（Par-R）表明转换动作可以发生在复合进程中的某一部分
规则（Comm）表达的是：两个动作名完全相同并且互补的动作可以形成内动作，即复合的进程内部形成通信
规则（Res）表明约束进程只能做约束名以外的动作
规则（Rel）中的f为换名函数，该规则表明换名对转换关系的影响
一般可以将规则（Act）看作公理，其他的规则视为推导规则
如果 ，我们称（a，P’）为P的直接后继，有时也简称P’为P的直接后继
如果 ，我们称 为P的一个后继，或P’为P的后继
（Act） （Sum-L） （Act） （Comm） 图1.4 证明树示例图 上图中每个转换右侧所列的规则表示此转换所使用的转换规则，其中根节点为图中最下面的 ，最上面的叶子节点 和 是由公理直接得到的，其余的每一个节点都是由它上一层的节点通过某个推导规则得到的
1.3 行为等价性 对于顺序执行的程序而言，其可观测的属性无非是输入与输出，这是输入/输出函数模型合理性的基础
相应地，两个顺序执行的程序之间的行为等价自然地被刻画成输入-输出关系是一样的
但对于并发系统而言，可观测的属性是多样的，从而带来了各种各样的系统行为等价性定义方式
例如，在进程代数理论发展初期提出的刻画系统行为等价的概念包括：迹等价（trace equivalence）、失败等价（failures equivalence）、互模拟(bisimulation)、实验等价（experimental equivalence）以及准备模拟（readysimulation）等
目前，互模拟已经成为学术界公认的刻画进程以及并发系统等价的基本概念，在进程代数理论中扮演着重要角色
Minler在1991年图灵奖获奖演讲中曾将其作为进程代数的核心概念之一特别加以强调
例如，当利用进程或LTS描述系统与其规范时，互模拟概念可以用于刻画系统关于其规范的正确性
一般而言，若一个系统与其规范互模拟，则认为该系统满足规范，即，该系统是此规范的一个正确实现
1.4 互模拟的概念 互模拟是连接模态逻辑、计算机科学和集合论领域中许多重要理论的桥梁和纽带
可在扩展模态逻辑中证明一些结果，然后通过互模拟运用到过程理论中去；可以使用扩展模态公式描述不同的非良基集合的域；可以运用非良基集合来研究模态逻辑的可导出性
今天，互模拟因为各种目的广泛地应用在并行系统中；并行理论不仅仅与计算机科学有关，而且用在许多自然现象的模型化中；随着互模拟应用范围的扩大，如何把一个模型的随机部分反映到互模拟概念中去成了互模拟的一个研究方向；概率模型通常在几个应用领域被分析和定义；定义新颖的构造性的状态空间归约技术会大大提高概率模型检测效率，扩展概率模型检测范围
所有强互模拟关系的并，称为强互模拟，记作
如果 ，则称P和Q是强互模拟的
2 进程树生成算法 用CSP语言建立模型，其最后的输出是一个受CSP规约的进程代数
由进程代数可以确定该进程的生成树，并且该进程树是唯一的
进程树可用于对进程模型的验证以及互模拟验证
该进程树生成算法根据用户输入的进程代数（受CSP语言规约的），经过分析生成该进程的进程树，并将进程树以图形的方式呈现给用户
2.1 进程状态迁移的基本规则 定义进程代数
为进程；a为进程P可以做的动作;“+”代表 是选择关系,假设 都可以做a动作
在同一时间 中只能有一个进程做出a动作，即它们之间为选择关系，表示为 ;“|”代表 是并发关系
其中 为进程；a为进程P可以做的动作； ， ， ，
进程P的进程树生成规则可由下表定义： 图2-1 2.3 进程树生成算法的思想 本进程树生成算法采用了最小分割的思想
对于一个由进程代数表示的进程，首先将其按照选择关系、并发关系、优先级等进行最小分割得出一个分割表；遍历它的最小分割项，求出它的子节点；接着遍历分割表，得出每个节点的直接父节点，生成一个父节点表；最后由父节点表画出进程树
例如：对于进程代数P=(a.b.0+a.c.0)|e.f.0 将其按照选择关系、并发关系、优先级进行最小分割，得出分割表
分割表的数据格式：<父分割项，子分割项1，子分割项2，分隔符，是否遍历>
节点表的数据格式：<父节点，子节点，动作>
④根据节点表画出进程树
由根节点开始，在节点表中寻找父节点为(a.b.0+a.c.0)|e.f.0的项
2.4进程树生成算法的程序实现 图2-4 程序流程图 算法的具体实现与测试参见本文第四部分“系统实现及实验介绍”
3 互模拟验证算法 互模拟验证算法的作用：由用户用CSP为两个进程建模，输入进程代数
本算法验证根据这两个进程代数验证这两个进程是否互模拟
验证两个进程是否互模拟，首先需要获得这两个进程的进程树
如果这两个进程的进程树的深度不同，则可以直接判断出他们不互模拟
接着对其进程树自下而上遍历，在每一层寻找互模拟关系，如果有哪层没有互模拟关系就可以直接判断它们不互模拟
如果每一层都互模拟，最终可以判断这两个进程是互模拟的
3.2 互模拟验证算法的基本思想 进程的互模拟验证要用到在上一节涉及到的进程树生成算法
由用户用CCS对进程P和Q建模，用进程树生成算法导出该进程的进程树
验证互模拟： 用如下伪代码来表述互模拟验证的过程
如果进程P和Q生成的进程树的深度不同，则P和Q不互模拟，程序终止 从P和Q进程树的深度为0的节点起，构造关系
令S[0]={（s,t):s,t深度均为0} 若S[i]不为空，令S[i+1]={(s,t):s,t深度均为i+1} 依次检验S[i+1]中的序偶对，若存在 或者 ，则从 中删去(s,t)
例1，对于进程代数P=a.0+b.0 和进程代数Q=a.c.0+e.f.o+k.i.0 使用上节介绍的进程树生成算法生成这两个进程代数的的进程树，如下图所示
图3-1 进程P的进程树 图3-2 进程Q的进程树 接下来开始验证P和Q之间是否存在互模拟关系
首先，分析进程P和Q的生成树的深度，发现进程P的生成树的深度为2，进程Q的生成树的深度为3，根据进程互模拟验证的基本规则可以直接判定进程P和Q直接不存在互模拟关系
首先，分析进程代数P和Q的生成树，得知进程P的进程树的深度为2，进程Q的进程树的深度为2
然后在深度为0的节点，构造二元关系S={<(a.0+b.0)|c.0,b.0|c.0>},，根据互模拟验证基本规则，发现<(a.0+b.0)|c.0,b.0|c.0>为互模拟关系
接下来在深度为1的节点构造二元关系S，发现其中也存在互模拟的关系
继续遍历深度为2的节点，同样构造二元关系S，在区中发现了互模拟的关系
当继续遍历的时候发现已到达了树的顶部，这时可以说明进程P和Q是互模拟的
4、系统实现及实验介绍 4.1 实验平台构架 4.1.1 开发环境介绍 本系统运行于Window XP操作系统环境下，采用SQL Server 2005数据库进行数据构建，运用C#语言与SOL语句在Visual Studio 2008开发环境下进行系统实现
SQL Server 2005是一个全面的数据库平台，其数据引擎是企业数据管理解决方案的核心
集成的商业智能（BI）工具、分析、报表、集成和通知功能为用户提供了企业级的数据管理
SQL Server 2005数据库引擎为关系型数据和结构化数据提供了更安全可靠的存储功能，可以构建和管理用于业务的高可用和高性能的数据应用程序
SQL Server 2005可以为开发人员、数据库管理员、信息工作者以及决策者提供创新的解决方案，帮助用户从数据中获得更多的收益
Visual Studio是Windows平台应用程序开发环境，可用来创建Windows平台下Windows应用程序和网络应用程序，也可用来创建网络服务、智能设备应用程序和Office插件
而Visual Studio 2008版本引入了250多个新特性，整合了对象、关系型数据、XML的访问方式，语言更加简洁
同时支持项目模板、调试器和部署程序
Visual Studio 2008可以高效开发Web应用，集成了AJAX 1.0，包含AJAX项目模板，它还可以高效开发Office应用和Mobile应用
随着.NET平台和C#语言的不断发展，Visual Studio 2008作为.NET平台下应用程序开发的主要工具，以其简单友好的操作界面、方便快捷的编码方式、完整的调试环境等优势，为应用程序开发人员带来很多的帮助
它在继承C和C++强大功能的同时去掉了一些它们的复杂特性（例如没有宏和模版，不允许多重继承）
C#综合了VB简单的可视化操作和C++的高运行效率，以其强大的操作能力、优雅的语法风格、创新的语言特性和便捷的面向组件编程的支持成为.NET开发的首选语言
并且C#成为ECMA与ISO标准规范
C#看似基于C++写成，但又融入其它语言如Pascal、Java、VB等
4.2系统的构成 本节，我们将给出我们的进程互模拟验证系统的模块构成，以及各个模块的功能
图4-1 系统模块构成 模块1将待验证的协议用CSP建模，导出进程代数，此过程是手工完成的
模块2将模块1导出的两个进程代数输入程序
模块3对模块 2的输入的两个进程代数进行分析，识别出各个单词，关键词，动作，变量之类的
模块4运用进程树生成算法，对输入的进程代数进行分析、运算，最终在数据库中产生个节点表，其中存有该进程树的每个节点的信息
模块6根据模块4输出的节点表，画出这两个进程的进程树，并且显示出来
模块7和模块8用来输出互模拟验证的结果
说明：对于模块1，目前主要采用手工方法来实现，并且其输出一般都比较简单
4.3数据类型以及存放方式 模块4的进程树生成算法以及模块5的互模拟验证算法，其中用到了最小分割表和节点表
这两个表建立在SQl2005数据库
其格式如下： 最小分割表： <1>字段名以及数据类型 图4-2 最小分割表定义 <2>程序运行过程中产生的部分数据 图4-3 最小分割表部分数据 由于最小分割表与模块5的互模拟验证无关，所以进程1和进程2可以共用同一个最小分割表
对最小分割表进行循环遍历，每一行的子分割项都不能再进行最小分割
这样该进程代数的最小分割表也就完成了
4.4.2节点表生成的函数 函数功能：根据最小分割表完成生成树的节点表 输入： 用CSP语言描述的进程代数的最小分割表 输出：在数据库的节点表中存入进程树的节点信息 算法思想：遍历进程代数的最小分割表的每一行，如果该行的的子分割项字段在节点表中都存在，则根据进程代数的SOS规约生成该项的节点信息，将其存入节点表中，同时在最小分割表中删除该行
循环遍历直至分割表的行数为0
至此，节点表也就完成了
该函数运用了递归的思想，最后将该进程树的节点一层层的画在画布上，最后用一个picturebox控件呈现给用户
如果进程树的深度不同，则返回false
表示这两个进程不互模拟
<2>、从进程树深度为0的节点开始，构造二元关系
遍历此二元关系，找出其中存在互模拟关系的
若存在互模拟关系的
当遍历至进程树的最顶层时，集合
4.5 界面设计 本文主要针对算法研究，在界面设计方面主要实现算法的测试功能，故看起来比较简单
该界面运用TabControl容器，设置TabPage1和TabPage2分别为进程1和进程2的显示界面，进程1界面实现为进程代数1生成进程树，进程2界面实现为进程代数2生成进程树，对于验证两个进程代数是否互模拟，将在界面1内验证实现
实际上恰恰相反，测试是为了证明程序中是存在错误的
因为程序在实际运行中会遇到各种各样的问题，而这些问题可能是我们在设计时没有考虑到的，所以在设计测试方案时，就应该尽量让它能发现程序中的错误，从而在软件投入运行之前就将这些错误改正，最终把一个高质量的软件系统交给用户使用
对于测试的目的，Grenford J.Myers曾提出过以下观点： （1）测试是为了发现程序中的错误而执行程序的过程 好的测试方案是极可能发现迄今为止尚未发现的错误的测试方案 成功的测试是发现了至今为止尚未发现的错误测试
具体地说，软件测试是根据软件开发各阶段的规格说明和程序的内部结构而精心设计出一批测试用例，并利用测试用例来运行程序，以发现程序错误的过程
正确认识测试的目的是十分重要的，只有这样，才能设计出最能暴露错误的测试方案
此外，我们应该意识到，测试只能证明程序中错误的存在，但不能证明程序中没有错误
因为即使经过了最严格的测试之后，仍然可能还没有被发现的错误存在于程序中，所以说测试只能查出程序中的错误，但不能证明程序没有错误
4.6.2 测试方法 测试方法主要有两种，黑盒测试和白盒测试
一般情况采用两种测试方法同时进行
黑盒和白盒的主要区别在于测试是针对系统的内部结构还是具体实现的算法
下面简要介绍这两种测试方法： 黑盒测试： 黑盒测试也称功能测试或数据驱动测试，它是在已知产品所应具有的功能，通过测试来检测每个功能是否都能正常使用
在完全不考虑程序内部程序和内部特性的情况下，测试者在程序接口进行测试，它只检查程序功能是否按照需求规格说明书的规定正常使用，程序是否能够适当地接收输入数据而产生正确的输出信息，并且保持外部信息（如数据库或文件）的完整性
黑盒测试方法主要有等价类划分、边值分析、因果图、错误推测等，在本系统中主要用于软件确认测试
白盒测试的主要方法有逻辑驱动、基路测试等，在本系统中主要用于软件验证
4.6.3 测试实施 在测试过程中，需首先验证对于不能分割的进程代数的进程树生成算法的正确性
其次，对于由选择符“+”分割的进程代数，验证进程树生成算法的正确性
同样，对于由并发运算符“|”分割的进程代数，验证进程树生成算法的正确性
然后，输入比较复杂的进程代数，其中包含括号、选择符、并发运算符，验证进程树生成算法的正确性
接下来，分别输入两组进程代数，其中一组是互模拟的，另一组中的进程代数没有互模拟关系，验证互模拟验证算法的正确性
最后，通过观察以上几步的测试结果，验证结果的正确性，进一步证明算法的正确性以及可行性
列举用例:a.b.0 描述：执行a动作后到达b.0状态，再执行b动作，到达0状态，即终止
生成树如图所示： 图4-10 测试结果 （2） + + 表示执行 进程同时舍弃 进程或执行 进程同时舍弃 进程
列举用例：a.b.0+a.c.0 描述：执行a.b.0进程或者执行a.c.0进程，二者只能选其一，对于动作分解同（1）描述
生成树如图所示：注意每个图都要有标号和名字 图4-11 测试结果 （3） | | 表示 和 并发执行， 、 既可以分别与外界交互也可以两者之间进行交互
列举用例：a.b.0|c.d.0 描述：a.b.0与c.d.0两个进程并发执行，第一个动作可以执行a或c，若执行a，a动作后可执行b或c，以次类推，同理若执行c动作，c动作后可执行a或d动作，以此类推，直至执行0动作终止
从理论基础上分析，我们知道进程①与进程③⑤互模拟，因为都存在这样的分支：执行a动作→执行b动作→执行c动作→进程终止
同理，进程①与进程②④不能互模拟
4.6.4测试结果分析 在进程树生成算法测试中，我们使用了三种不同类型的进程代数，然后将其分别输入到系统中
观察程序生成的进程树并将其与我们预先的分析结果比较后，验证了进程树生成算法的正确性
对于互模拟验证算法，在测试时考虑到互模拟验证算法的交互性，共采用了6组测试数据
每组按照进程代数的类型划分，然后根据他们之间是否互模拟的关系再进一步划分
最后将测试数据输入系统进行测试
通过观察测试结果，证明了互模拟验证算法的正确性
通过观察测试的结果，验证了进程树显示函数的正确性以及可行性
5 结束语 本文基于CSP语言描述的进程模型提出算法验证两个进程是否互模拟，同时由进程代数生成进程树，并将进程树以树状图的方式呈现给用户
今天，互模拟因为各种目的被广泛地用在并发系统中，最大互模拟一般被看作是施加于系统上的最精致的行为等价性
互模拟证明方法被用来证明过程之间的等价性，甚至当人们不选择最大互模拟作为过程之间的行为等价性时，情况也一样
例如，我们也许对路径等价性感兴趣，并且也使用互模拟证明方法，因为最大互模拟蕴涵路径等价性
利用最大互模拟检测算法的效力和最大互模拟合成性特征使进程的状态空间最小化
最大互模拟和它的变体（如最大模拟）被用来对某些有意思的系统进行抽象化
总之，在互模拟验证方面现在还有很大的研究空间
