进程互模拟验证算法的研究与实现(毕业论文12600字)
【摘要】伴随着计算机网络的诞生，分布式计算应用日益广泛。远程过程调用、网格、web服务、移动Agent等分布计算技术已经不再是陌生的术语，它们得到了越来越广泛的应用。这些新的分布式计算技术给我们带来了更强大的计算能力，更高的灵活性和方便，但随之而来的是一系列的程序验证问题。由于并发分布式系统本身非常复杂，因此其开发过程不仅难度大、效率低、周期长，而且很难避免和发现其中隐含的错误和缺陷。对于安全攸关系统(safety critical systems)，其失误和崩溃可能会造成生命和财产的重大损失，甚至导致灾难。形式化方法被公认为是一种行之有效的减少设计错误、提高系统可靠性的重要途径。对此，学者们采用了形式化的方法为系统建模，描述规范及验证系统是否满足规范。其中，进程代数是一中常用的有效工具，它可用于建模及描述规范。本文将给出算法，验证两个进程是否互模拟，从而验证系统是否满足规范。
【关键字】进程代数、进程等价性、互模拟
Process bisimulation verification algorithm
Abstract: Along with the birth of computer networks, distributed computing applications are increasingly widespread. Remote procedure calls, grid, web services, mobile agent and distributed computing technology is no longer a strange term, they have been more widely used.These new distributed computing technology has brought us a more powerful computing capability, greater flexibility and convenience, but followed by a series of program verification. Concurrent distributed system itself is very complex, so the development process is not only difficult, low efficiency, long life cycle, and it is difficult to avoid and which implied errors and defects. For safety critical systems (safety critical systems), its failures and the collapse may cause significant loss of life and property, and even lead to disaster. Formal methods is recognized as an effective reduction of design errors, an important way to improve system reliability. In this regard, scholars using formal methods for system modeling, describe the specification and verification system meets the specification. Among them, the process algebra is the one commonly used and effective tool, it can be used for the modeling and description of the specification. This article will give the algorithm to verify whether the two processes are bisimulation to verify the system meets the specification.
Key word:Process algebra, process equivalence, bisimulation
目 录
摘要 I
Abstract: II
引言 1
1 基本概念 3
1.1 进程代数 3
1.2 CSP的基本概念 3
1.2.1 CSP的归约语义 4
1.2.2 CSP的LTS语义及其性质 4
1.3 行为等价性 6
1.4 互模拟的概念 7
2 进程树生成算法 7
2.1 进程状态迁移的基本规则 8
2.2 生成进程树的基本规则 8
2.3 进程树生成算法的思想 9
2.4进程树生成算法的程序实现 12
3 互模拟验证算法 12
3.1 互模拟验证的基本规则 12
3.2 互模拟验证算法的基本思想 13
3.3 互模拟验证算法的程序实现 15
4、系统实现及实验介绍 16
4.1 实验平台构架 16
4.1.1 开发环境介绍 16
4.1.2 开发语言介绍 16
4.2系统的构成 17
4.3数据类型以及存放方式 18
4.4 各个模块的主要函数的描述及算法 19
4.4.1 对CSP语言描述的进程代数进行最小拆分的函数 19
4.4.2节点表生成的函数 20
4.4.3 显示进程树的函数 20
4.4.4 验证互模拟的函数 21
4.5 界面设计 21
4.6 算法测试 22
4.6.1 测试目的 22
4.6.2 测试方法 23
4.6.3 测试实施 24
4.6.4测试结果分析 29
5 结束语 29
参考文献 31
致谢 32
引言
伴随着计算机网络的诞生，新的计算环境和计算模型产生了——分布式计算环境与分布式的计算模型。远程过程调用、网格、web服务、移动Agent等分布计算技术已经不再是陌生的术语，而是得到了越来越广泛的应用。这些新的分布式计算技术给我们带来了更强大的计算能力，更高的灵活性和方便，但随之而来的是一系列的程序验证问题。由于并发分布式系统本身非常复杂，因此其开发过程不仅难度大、效率低、周期长，而且很难避免和发现其中隐含的错误和缺陷。对于安全攸关系统(safety critical systems)，其失误和崩溃可能会造成生命和财产的重大损失，甚至导致灾难。
软件开发包括需求、设计、编码和测试等阶段，有时也包括维护阶段。传统的软件开发方法由于大量的使用自然语言和多种图形符号，结果是尽管经历了仔细的复审，最后的系统规约说明中仍然包歧义的、含糊的、矛盾的、不完整的需求描述及混乱的抽象层次。在传统的软件开发过程中，前期各阶段的工作成果都是自然语言描述的“文档”，只有最后开发阶段的成果是形式化的程序。非形式的前期工作成果（文档）只能由人阅读、理解和讨论，无法严格的分析和推理（这方面情况也正在变化）。由于程序的复杂性，对其进行分析和推理非常困难。
形式化方法被公认为是一种行之有效的减少设计错误、提高系统可靠性的重要途径。软件形式化方法最早可追溯到20世纪50年代后期对于程序设计语言编译技术的研究，即J.Backus提出BNF描述Algol60语言的语法，出现了各种语法分析程序自动生成器以及语法制导的编译方法，使得编译系统的开发从“手工艺制作方式”发展成具有牢固理论基础的系统方法。形式化方法的研究高潮始于 20世纪60年代后期，针对当时所谓“软件危机”,人们提出种种解决方法,归纳起来有两类：一是采用工程方法来组织、管理软件的开发过程；二是深入探讨程序和程序开发过程的规律，建立严密的理论，以其用来指导软件开发实践。前者导致“软件工程”的出现和发展，后者则推动了形式化方法的深入研究。经过30多 年的研究和应用，如今人们在形式化方法这一领域取得了大量、重要的成果，从早期最简单的形式化方法——一阶谓词演算方法到现在的应用于不同领域、不同阶段的基于逻辑、状态机、网络、进程代数、代数等众多形式化方法。形式化方法的发展趋势逐渐融入软件开发过程的各个阶段，从需求分析、功能描述(规约)、(体系结构/算法)设计、编程、测试直至维护。
用于开发计算机系统的形式化方法是描述系统性质的基于数学的技术，这样的形式化方法提供了一个框架，可以在框架中以系统的而不是特别的方式刻划、开发和验证系统。 如果一个方法有良好的数学基础，那么它就是形式化的。这个基础提供一系列精确定义的概念，如：一致性和完整性，以及定义规范的实现和正确性。形式化方法的本质是基于数学的方法来描述目标软件系统属性的一种技术。不同的形式化方法的数学基础是不同的，有的以集合论和一阶谓词演算为基础（如Z和 VDM），有的则以时态逻辑为基础。形式化方法需要形式化规约说明语言的支持。形式化方法研究涉及如下几个重要方面：
建模（Modeling）：为系统建立形式化模型，使用模型检测工具能够接受的形式语言来刻画系统。在形式化过程中应该对系统进行一定程度的抽象，去除不必要的信息。
描述（Specification）：阐明所要验证的性质。注意到模型检测只能够检查模型（系统）是否满足给定的公式，因而所提供的公式能否完全正确地刻画所关心的性质是得到正确检测结果的必要前提。
验证（Verification）：狭义的验证过程是指状态空间的搜索过程。这部分工作是可以完全自动完成的。广义的验证包括搜索（及报错），修改系统，再搜索，再修改……的过程，其中对于错误信息的分析和对系统的修改和重新建模的工作是需要用户参与的。
上述几点之间存在着紧密的联系。例如在进行建模时，系统的形式化抽象既需要考虑到验证时的效率和时空限制，从而尽可能地忽略冗余信息，又应该突出与待验证性质相关的特征。从某种意义上说，当验证过程给出反例时可以确信模型与性质不符，因此“证否”的工作是又验证步骤来完成的；但是肯定的验证结果是否能够“证实”，还取决于系统建模和性质描述两步。
在形式化验证过程中，验证用于描述系统的模型与描述性质的模型是否等价是一个重要问题，本文将就此展开研究。
1 基本概念
1.1 进程代数
在计算机理论的早期研究中，一般将具有输入/输出的函数作为程序的数学模型。随着计算机的发展，尤其是分布式系统与网络的出现，并发现象和交互反应的存在已不容忽视。传统的输入/输出函数模型无法胜任对这些计算现象的刻画。因此，如何描述并行的、交互反应使分布式的系统从上世纪60年代起成为了一个研究的热点，并逐步形成了所谓并发理论的研究领域，它已成为计算机科学的主流研究方向之一。
最早的并发模型是Petri与1962年在其博士论文中提出的。他给出了一种网状结构信息流模型——Petri网。Petri网既可以作为一种图形工具来模拟系统的动态行为和并发活动，又可以作为数学工具来建立状态方程、代数方程以及系统行为的其他代数模型，是一种应用广泛的理论工具。
除Petri网理论外，最著名、研究的最广泛的并发模型就是进程代数。进程代数中并发系统的行为往往被描述为状态转换图加以考察，其中最简单的描述形式之一是带标记的转换系统（LTS，labeled transition system）。当不需要考察进程代数中的独立性、协调性等特殊性质的时候，LTS可以展现进程代数的一般性质。当考察进程代数的特殊性质时，一些更为复杂的模型被给出。
1.2 CSP的基本概念
CSP是最早被提出的进程代数系统之一。它引入了复合（parallel composition）、和（sum）、以及约束（restriction）等算子下面我们先介绍一些基本概念和符号。
CSP中的进程可由如下的BNF范式定义：
，（其中 ）。
所有进程构成的集合记为Proc，一般用P, Q…表示进程。0表示不能执行任何动作的进程。带前缀（prefix）的进程 有唯一的由前缀 所表达的能力，只有当 执行过之后 才能进行演化，例如： .P表示该进程可以执行一个外界不可观测的动作，然后再执行P。和 表示不确定的选择， 的能力包含了 和 两部分的能力，当它执行了其中的一部分的能力后，另一个部分就被会抛弃。复合进程 表示 和 并发执行， 、 既可以分别与外界交互也可以两者之间进行交互。
1.2.1 CSP的归约语义
归约语义描述了一个系统内部进化的最小的一步，它不考虑系统与环境之间的交互。下面，我们首先介绍一个辅助概念——结构化同余（structural congruence），进而给出进程上归约（reduction）关系的定义。
定义: 进程上下文（context）C是指一个带空位（[-]）的进程表达式，定义如下：
(SC Sum Assoc)
(SC Sum Comm)
(SC Sum Inact)
(SC Comp Assoc)
(SC Comp Comm)
(SC Comp Inact)
表1-1
1.2.2 CSP的LTS语义及其性质
我们知道归约关系仅仅描述了系统内部不同部分的交互，并不关心系统与外部环境的交互。而带标记的转换系统LTS（Labeled Transition System）不但可以刻画系统的内部演化，而且可以描述系统与环境的交互。在进程代数中，LTS通常是由一组SOS（Structural Operational Semantics）规则加以规范的。
定义: 带标记的转换系统是一个三元组 ，其中S为状态集，T为转换标记集，对任意的 ，转换关系 称为标记为t的转换。
直观上， 表示状态s经过一个标记为t的转换到达状态s’。在进程代数中，一般用进程表示状态，动作表示转换标记。
定义: 为一个带标记的转换系统，其中Proc表示进程的集合，Act表示动作集，转换关系 由表2.3中的SOS规则所规范。
(Act)
(Sum-L)
(Sum-R)
(Par-L)
(Par-R)
(Comm)
表1-3
规则（Act）表明带前缀的进程可以进行一个前缀所标记的转换，消耗掉前缀后到达新的状态。规则（Sum-L）和（Sum-R）表明如果和的某一部分可以经过一个动作，到达某个新状态，则和也可以执行该动作并到达同样的状态。规则（Par-L）和（Par-R）表明转换动作可以发生在复合进程中的某一部分。规则（Comm）表达的是：两个动作名完全相同并且互补的动作可以形成内动作，即复合的进程内部形成通信。规则（Res）表明约束进程只能做约束名以外的动作。规则（Rel）中的f为换名函数，该规则表明换名对转换关系的影响。一般可以将规则（Act）看作公理，其他的规则视为推导规则。
如果 ，我们称（a，P’）为P的直接后继，有时也简称P’为P的直接后继。如果 ，我们称 为P的一个后继，或P’为P的后继。
一个转换 在CCS中的证明可以被看作是一棵证明树，例如： 的证明可以形成如下一棵树。
（Act）
（Sum-L） （Act）
（Comm）
图1.4 证明树示例图
上图中每个转换右侧所列的规则表示此转换所使用的转换规则，其中根节点为图中最下面的 ，最上面的叶子节点 和 是由公理直接得到的，其余的每一个节点都是由它上一层的节点通过某个推导规则得到的。
1.3 行为等价性
对于顺序执行的程序而言，其可观测的属性无非是输入与输出，这是输入/输出函数模型合理性的基础。相应地，两个顺序执行的程序之间的行为等价自然地被刻画成输入-输出关系是一样的。但对于并发系统而言，可观测的属性是多样的，从而带来了各种各样的系统行为等价性定义方式。例如，在进程代数理论发展初期提出的刻画系统行为等价的概念包括：迹等价（trace equivalence）、失败等价（failures equivalence）、互模拟(bisimulation)、实验等价（experimental equivalence）以及准备模拟（readysimulation）等。目前，互模拟已经成为学术界公认的刻画进程以及并发系统等价的基本概念，在进程代数理论中扮演着重要角色。Minler在1991年图灵奖获奖演讲中曾将其作为进程代数的核心概念之一特别加以强调。
以互模拟概念为基础的行为等价理论在形式化规范、设计和验证中扮演着重要角色。例如，当利用进程或LTS描述系统与其规范时，互模拟概念可以用于刻画系统关于其规范的正确性。一般而言，若一个系统与其规范互模拟，则认为该系统满足规范，即，该系统是此规范的一个正确实现。
1.4 互模拟的概念
互模拟是连接模态逻辑、计算机科学和集合论领域中许多重要理论的桥梁和纽带。可在扩展模态逻辑中证明一些结果，然后通过互模拟运用到过程理论中去；可以使用扩展模态公式描述不同的非良基集合的域；可以运用非良基集合来研究模态逻辑的可导出性。今天，互模拟因为各种目的广泛地应用在并行系统中；并行理论不仅仅与计算机科学有关，而且用在许多自然现象的模型化中；随着互模拟应用范围的扩大，如何把一个模型的随机部分反映到互模拟概念中去成了互模拟的一个研究方向；概率模型通常在几个应用领域被分析和定义；定义新颖的构造性的状态空间归约技术会大大提高概率模型检测效率，扩展概率模型检测范围。
互模拟是刻画进程等价的重要概念，下面我们回顾进程代数中的互模拟概念：强互模拟
定义： 关系 是一个强互模拟关系，当且仅当对任意的 及任意的 ，下列条件成立：
（1）如果 ，则存在 使得 且 ；
（2）如果 ，则存在 使得 且 。
所有强互模拟关系的并，称为强互模拟，记作 。如果 ，则称P和Q是强互模拟的。
2 进程树生成算法
用CSP语言建立模型，其最后的输出是一个受CSP规约的进程代数。由进程代数可以确定该进程的生成树，并且该进程树是唯一的。进程树可用于对进程模型的验证以及互模拟验证。
该进程树生成算法根据用户输入的进程代数（受CSP语言规约的），经过分析生成该进程的进程树，并将进程树以图形的方式呈现给用户。
2.1 进程状态迁移的基本规则
定义进程代数 。 为进程；a为进程P可以做的动作;“+”代表 是选择关系,假设 都可以做a动作 。在同一时间 中只能有一个进程做出a动作，即它们之间为选择关系，表示为 ;“|”代表 是并发关系。
的状态迁移有以下三种类型：
1、 可以做a动作， 不能做a动作 则 的状态迁移为 ；
2、 不能做a动作， 可以做a动作 则 的状态迁移为 ；
3、 可以做a动作， 可以做a动作 ，则 的状态迁移为 ；
2.2 生成进程树的基本规则
定义进程代数 。其中 为进程；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, a.b.0+a.c.0 , e.f.0, |，未遍历>
<a.b.0+a.c.0, a.b.0, a.c.0,+，未遍历>
遍历进程代数的最小分割项，求出它的子节点。节点表的数据格式：<父节点，子节点，动作>。
<a.b.0, b.0, a>
<b.0, b , 0>
<a.c.0, a , c.0>
<c.0, c , 0>
<e.f..0, e , f.0>
<f.0, f, 0>
遍历分割表，完成节点表
在分割表中找出第一行，<（a.b.0+a.c.0)|e.f.0, a.b.0+a.c.0 , e.f.0, |，未遍历>，发现它的子分割项的a.b.0+a.c.0在节点表中的父节点字段不存在，转而遍历第2行<a.b.0+a.c.0, a.b.0, a.c.0,+，未遍历>，它的子分割项在节点表中的父节点字段都存在，所以按照进程状态迁移的基本规则，在节点表中生成它的子节点：
<a.b.0+a.c.0,b.0,a>
<a.b.0+a.c.0,c.0,a>
修改分割表中本行的是否遍历字段为已遍历，然后遍历分割表中的是否遍历字段为未遍历的行，即：<（a.b.0+a.c.0)|e.f.0, a.b.0+a.c.0 , e.f.0, |，未遍历>在节点表中可以找到它的所有分割项，所以在节点表中生成它的子节点：
<（a.b.0+a.c.0)|e.f.0,（a.b.0+a.c.0)|f.0,e>
<（a.b.0+a.c.0)|e.f.0,b.0|e.f.0,a>
<（a.b.0+a.c.0)|e.f.0,c.0|e.f.0,a>
修改分割表中本行的是否遍历字段为已遍历，至此节点表已经完成。
④根据节点表画出进程树。由根节点开始，在节点表中寻找父节点为(a.b.0+a.c.0)|e.f.0的项。结果为：
<（a.b.0+a.c.0)|e.f.0,（a.b.0+a.c.0)|f.0,e>
<（a.b.0+a.c.0)|e.f.0,b.0|e.f.0,a>
<（a.b.0+a.c.0)|e.f.0,c.0|e.f.0,a>
据此画出进程树的根节点
图2-2
然后跟据根节点的子节点按照上述步骤一步步画出该进程代数的进程树如下：
图2-3
以上介绍了进程代数生成进程树的基本思想，下一节将给出具体算法。
2.4进程树生成算法的程序实现
图2-4 程序流程图
算法的具体实现与测试参见本文第四部分“系统实现及实验介绍”。
3 互模拟验证算法
互模拟验证算法的作用：由用户用CSP为两个进程建模，输入进程代数。本算法验证根据这两个进程代数验证这两个进程是否互模拟。
3.1 互模拟验证的基本规则
两个互相模拟的进程其进程树的深度肯定相同，并且其进程树自下而上保存互模拟的关系，如果有某一层不互相模拟，找不到互模拟的关系，则它们不是互模拟的。
验证两个进程是否互模拟，首先需要获得这两个进程的进程树。如果这两个进程的进程树的深度不同，则可以直接判断出他们不互模拟。接着对其进程树自下而上遍历，在每一层寻找互模拟关系，如果有哪层没有互模拟关系就可以直接判断它们不互模拟。如果每一层都互模拟，最终可以判断这两个进程是互模拟的。
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)。
若 不为空,则i+1是P和Q的深度，则P~Q,返回true；
否则，若 为空，则P和Q不互模拟，返回false；
否则，若 不为空，且对于任意深度为i+1的点s，均存在一点t满足 ,则i=i+1，继续循环。
例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直接不存在互模拟关系。
例2，对于进程代数P=(a.0+b.0)|c.0 Q=b.0|c.0
P和Q的进程树如下图所示：
图3-3 进程代数P的生成树
图3-4 进程代数Q的生成树
接下来开始验证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是互模拟的。
3.3 互模拟验证算法的程序实现
图3-5 程序流程图
算法的具体实现与测试参见本文第四部分“系统实现及实验介绍”。
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平台下应用程序开发的主要工具，以其简单友好的操作界面、方便快捷的编码方式、完整的调试环境等优势，为应用程序开发人员带来很多的帮助。
4.1.2 开发语言介绍
C#是一种安全的、稳定的、简单的、优雅的，由C和C++衍生出来的面向对象的编程语言。它在继承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运用进程树生成算法，对输入的进程代数进行分析、运算，最终在数据库中产生个节点表，其中存有该进程树的每个节点的信息。
模块5运用进程互模拟验证算法，根据模块4输出的节点表来验证这两个进程是否互模拟。
模块6根据模块4输出的节点表，画出这两个进程的进程树，并且显示出来。
模块7和模块8用来输出互模拟验证的结果。
说明：对于模块1，目前主要采用手工方法来实现，并且其输出一般都比较简单。
4.3数据类型以及存放方式
模块4的进程树生成算法以及模块5的互模拟验证算法，其中用到了最小分割表和节点表。这两个表建立在SQl2005数据库。其格式如下：
最小分割表：
<1>字段名以及数据类型
图4-2 最小分割表定义
<2>程序运行过程中产生的部分数据
图4-3 最小分割表部分数据
由于最小分割表与模块5的互模拟验证无关，所以进程1和进程2可以共用同一个最小分割表。
进程1的节点表：
<1>字段名以及数据类型
图4-4 节点表1定义
<2>程序运行过程中产生的部分数据
图4-5 节点表1部分数据
进程2的节点表：
<1>字段名以及数据类型
图4-6 节点表2定义
<2>程序运行过程中产生的部分数据
图4.7 节点表2部分数据
4.4 各个模块的主要函数的描述及算法
4.4.1 对CSP语言描述的进程代数进行最小拆分的函数
函数功能：对进程代数进行最小拆分
输入：符合CSP规约的进程代数表达式
输出：在数据库的最小分割表中存入其分割项
算法思想：对于输入的进程代数，按照选择“+”和并发“|”进行分割，接着对于它的子分割项同样按照选择“+”和并发“|”进行分割。对最小分割表进行循环遍历，每一行的子分割项都不能再进行最小分割。这样该进程代数的最小分割表也就完成了。
4.4.2节点表生成的函数
函数功能：根据最小分割表完成生成树的节点表
输入： 用CSP语言描述的进程代数的最小分割表
输出：在数据库的节点表中存入进程树的节点信息
算法思想：遍历进程代数的最小分割表的每一行，如果该行的的子分割项字段在节点表中都存在，则根据进程代数的SOS规约生成该项的节点信息，将其存入节点表中，同时在最小分割表中删除该行。循环遍历直至分割表的行数为0。至此，节点表也就完成了。
4.4.3 显示进程树的函数
函数功能：在屏幕上显示出该进程代数生成的进程树
输入：进程树的节点信息（存储于数据库的节点表中)
输出：该进程树的树状图
我们定义如下函数：
public void huashu(Graphics g, int a, int b, int kuan, string father)
{
string sss = "select * from donzuo1 where father='" + father + "'";
g.DrawString(father, this.Font, new SolidBrush(Color.Black), a, b);
DataSet myds = Sql.getds(sss);
for (int i = 0; i < myds.Tables[0].Rows.Count; i++)
{
g.DrawLine(System.Drawing.Pens.Black, a, b, a - kuan / 2 + (i + 1) * (kuan / (myds.Tables[0].Rows.Count + 1)), b + 80);
g.DrawString(myds.Tables[0].Rows[i]["donzuo"].ToString(),this.Font,
new SolidBrush(Color.Black), (a + a - kuan / 2 + (i + 1) * (kuan / (myds.Tables[0].Rows.Count + 1))) / 2, b + 40);
huashu1(g, a - kuan / 2 + (i + 1) * (kuan / (myds.Tables[0].Rows.Count + 1)), b + 80, kuan / (myds.Tables[0].Rows.Count + 1), myds.Tables[0].Rows[i]["son"].ToString());
}
}
其中Graphics g是定义的画布，a、b是该进程树的起始坐标,father是该进程树的根节点。该函数运用了递归的思想，最后将该进程树的节点一层层的画在画布上，最后用一个picturebox控件呈现给用户。
4.4.4 验证互模拟的函数
函数功能：验证两个用CSP语言描述的进程是否互模拟
输入：进程树的节点表
输出：告知用户这两个进程互模拟验证的结果
算法思想：<1>、判断P和Q生成的进程树的深度。如果进程树的深度不同，则返回false。表示这两个进程不互模拟。
<2>、从进程树深度为0的节点开始，构造二元关系<s,t>，s为进程P生成的进程树的节点所能做的动作，t为进程Q生成的进程树的节点所能做的动作。遍历此二元关系，找出其中存在互模拟关系的。若存在互模拟关系的<s,t>的集合为空，则返回false，表示这两个进程不互模拟；若集合不为空，则深度加1，继续遍历两个进程树。
当遍历至进程树的最顶层时，集合<s,t>不为空时，返回true，表示这两个进程互模拟。
4.5 界面设计
本文主要针对算法研究，在界面设计方面主要实现算法的测试功能，故看起来比较简单。
该界面运用TabControl容器，设置TabPage1和TabPage2分别为进程1和进程2的显示界面，进程1界面实现为进程代数1生成进程树，进程2界面实现为进程代数2生成进程树，对于验证两个进程代数是否互模拟，将在界面1内验证实现。具体界面图如下：
进程1界面：
图4-8 进程1界面
进程2界面：
图4-9 进程2界面
4.6 算法测试
4.6.1 测试目的
人们对于软件测试的目的往往存在着这样的错误认识：测试是为了表明程序是正确的。实际上恰恰相反，测试是为了证明程序中是存在错误的。因为程序在实际运行中会遇到各种各样的问题，而这些问题可能是我们在设计时没有考虑到的，所以在设计测试方案时，就应该尽量让它能发现程序中的错误，从而在软件投入运行之前就将这些错误改正，最终把一个高质量的软件系统交给用户使用。对于测试的目的，Grenford J.Myers曾提出过以下观点：
（1）测试是为了发现程序中的错误而执行程序的过程
好的测试方案是极可能发现迄今为止尚未发现的错误的测试方案
成功的测试是发现了至今为止尚未发现的错误测试。
从上述规格可以看出，测试的定义是“为了发现程序中的错误而执行程序的过程”。具体地说，软件测试是根据软件开发各阶段的规格说明和程序的内部结构而精心设计出一批测试用例，并利用测试用例来运行程序，以发现程序错误的过程。正确认识测试的目的是十分重要的，只有这样，才能设计出最能暴露错误的测试方案。
此外，我们应该意识到，测试只能证明程序中错误的存在，但不能证明程序中没有错误。因为即使经过了最严格的测试之后，仍然可能还没有被发现的错误存在于程序中，所以说测试只能查出程序中的错误，但不能证明程序没有错误。
4.6.2 测试方法
测试方法主要有两种，黑盒测试和白盒测试。一般情况采用两种测试方法同时进行。黑盒和白盒的主要区别在于测试是针对系统的内部结构还是具体实现的算法。下面简要介绍这两种测试方法：
黑盒测试：
黑盒测试也称功能测试或数据驱动测试，它是在已知产品所应具有的功能，通过测试来检测每个功能是否都能正常使用。在完全不考虑程序内部程序和内部特性的情况下，测试者在程序接口进行测试，它只检查程序功能是否按照需求规格说明书的规定正常使用，程序是否能够适当地接收输入数据而产生正确的输出信息，并且保持外部信息（如数据库或文件）的完整性。黑盒测试方法主要有等价类划分、边值分析、因果图、错误推测等，在本系统中主要用于软件确认测试。
白盒测试：
白盒测试也称结构测试或逻辑驱动测试，可通过测试来检测产品内部动作是否按照规格说明书的规定正常进行，按照程序内部的结构测试程序，检验程序中的每条通路是否都有能按预定要求正确工作。白盒测试的主要方法有逻辑驱动、基路测试等，在本系统中主要用于软件验证。
4.6.3 测试实施
在测试过程中，需首先验证对于不能分割的进程代数的进程树生成算法的正确性。
其次，对于由选择符“+”分割的进程代数，验证进程树生成算法的正确性。
同样，对于由并发运算符“|”分割的进程代数，验证进程树生成算法的正确性。
然后，输入比较复杂的进程代数，其中包含括号、选择符、并发运算符，验证进程树生成算法的正确性。
接下来，分别输入两组进程代数，其中一组是互模拟的，另一组中的进程代数没有互模拟关系，验证互模拟验证算法的正确性。
最后，通过观察以上几步的测试结果，验证结果的正确性，进一步证明算法的正确性以及可行性。
1、生成树算法测试
（1）a.P
a.P表示执行完a动作后到达P状态。
列举用例: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动作终止。
生成树如图所示：
图4-12 测试结果
2 互模拟算法测试
模拟用例：① a.b.c.0
② b.c.0+a.c.d.0
③ a.c.0|b.c.0
④ b.c.d.0
⑤ a.0|b.c.0+a.c.d.0
进行测试，验证进程①与进程②③④⑤是否互模拟。
从理论基础上分析，我们知道进程①与进程③⑤互模拟，因为都存在这样的分支：执行a动作→执行b动作→执行c动作→进程终止。同理，进程①与进程②④不能互模拟。互模拟验证如下：
（1）①与②进行验证
图4-13 测试结果
（2）①与③进行验证
图4-14 测试结果
（3）①与④进行验证
图4-16 测试结果
通过验证，我们发现①与进程③⑤互模拟，与②④不互模拟，由于互模拟存在传递性，我们知道③⑤之间存在互模拟，而③、⑤与②、④均不互模拟。
4.6.4测试结果分析
在进程树生成算法测试中，我们使用了三种不同类型的进程代数，然后将其分别输入到系统中。观察程序生成的进程树并将其与我们预先的分析结果比较后，验证了进程树生成算法的正确性。
对于互模拟验证算法，在测试时考虑到互模拟验证算法的交互性，共采用了6组测试数据。每组按照进程代数的类型划分，然后根据他们之间是否互模拟的关系再进一步划分。最后将测试数据输入系统进行测试。通过观察测试结果，证明了互模拟验证算法的正确性。
通过观察测试的结果，验证了进程树显示函数的正确性以及可行性。
5 结束语
本文基于CSP语言描述的进程模型提出算法验证两个进程是否互模拟，同时由进程代数生成进程树，并将进程树以树状图的方式呈现给用户。
目前该系统经过测试，能够实现根据受CSP规约的进程代数生成进程树，并能够将进程树以图形的方式呈现给用户，本系统的互模拟验证功能是本课题研究的重点。
今天，互模拟因为各种目的被广泛地用在并发系统中，最大互模拟一般被看作是施加于系统上的最精致的行为等价性。互模拟证明方法被用来证明过程之间的等价性，甚至当人们不选择最大互模拟作为过程之间的行为等价性时，情况也一样。例如，我们也许对路径等价性感兴趣，并且也使用互模拟证明方法，因为最大互模拟蕴涵路径等价性。利用最大互模拟检测算法的效力和最大互模拟合成性特征使进程的状态空间最小化。最大互模拟和它的变体（如最大模拟）被用来对某些有意思的系统进行抽象化。总之，在互模拟验证方面现在还有很大的研究空间。
参考文献
[1 ]Gamma E ,Helm R ,Johnson R ,Vlisides J . 李英军等译. 设计模式:可复用面向对象软件的基础[M] . 北京:机械工业出版社,2002；
[2 ]王咏武,王咏刚. 道法自然———面向对象实践指南[M] . 北京: 电子工业出版社,2004；
[3 ]Fowler M. 侯捷等译. 重构:改善既有代码的设计[M] . 北京: 中国电力出版社,2003；
[4 ]Booch G,Rumbaugh J ,Jacobson I.邵维忠等译. UML 用户指南[M] .北京:机械工业出版社,2001；
[5 ] 钱锋,雷航.面向对象嵌入式GUI 研究和模式应用[J ] .计算机应用,2004 , (4)；
[6]蒋屹新，林闯，曲扬,尹浩.基于Pe城网的模型检测研究，软件学报,v01．15 No.9
Septernber 2004：1265一1276；
[7]陆汝钤．计算机语言的形式语义．科学出版社，1992；
[8]左孝凌等．离散数学，上海科学技术文献出版社，1982；
[9]J．E HopcrofI，J．D u11IIlⅫ，徐美瑞译．自动机理论、语言和计算导引，科学出版社，1986；
[10]蒋凡,宁华中.基于标号变迁系统的测试集自动生成，计算机研究与发展，v01．38No，12 2001：1435．1446；
[11]汤子赢，哲风屏，汤小丹．计算机操作系统，西安电子科技大学出版社，1996；
[12]易锦，张文辉．从基于迁移的扩展Bnchi自动机到Bnchi自动机，Journal ofsoRware，Vbl．17 No．4April 2006：720-728
|
