摘要: 并发程序的复杂性导致传统的软件测试方法难于发现其中的某些缺陷。使用形式化方法对并发程序进行建模和验证可以和软件测试形成互补。Chu空间是一种从范畴论领域发展起来的具有多种良好性质的并发行为的形式化模型。Chu空间支持真并发语义并且具有良好的代数特性。Chu空间为众多的数学结构提供了统一的表达方式。这些结构包括：集合、偏序集合、所有的小范畴、群、环、格、向量空间、布尔代数、拓扑空间等。另外，Chu空间还是对不确定性进行研究的工具，可以对随机性和模糊性等问题进行统一的表达和运算。
本文给出使用有限Chu空间作为形式化模型对并发程序进行建模和验证的方法。从实际建模的角度出发，本文给出了一个扩展的有限Chu空间的进程代数，包括5个算子：或算子、非确定选择算子、扩展的顺序合成算子、扩展的并发合成算子和触发合成算子。该进程代数可以直接描述典型的并发行为、基于语句块的异常处理机制以及并发进程间的同步机制。本文定义了一种假想的并发程序设计语言（ICL），该语言可以看作是实际并发语言的一种抽象。本文使用有限Chu空间及其扩展的进程代数给出了ICL的指称语义。由于该扩展的Chu空间进程代数经过了仔细地设计，所以该指称语义的语义函数非常直观。
建模之后就是验证阶段。本文给出了有限Chu空间的验证算法。扩展的有限Chu空间进程代数被同时用作Chu空间的规范语言。使用该语言所定义的进程代数类型的性质。例如：1. 事件a与b互斥；2. 事件a与b先后执行；3. 事件a与b并发执行。其中事件a,b可以是进程A,B。定义的性质分为2类：可允许的性质和必须具有的性质。本文给出对这2类性质的多项式时间的验证算法。
Chu空间进程代数具有可扩展性，即：根据不同的目标语言，可以对原有的算子进行修改，也可以提出新的算子。在实际应用中，需要进行验证的程序可能由各种程序设计语言写成。不同的语言具有不同的特性。例如：并发进程间的同步方式可能有共享变量、同步信号和消息传递等。对于这些不同的特性需要不同的处理，这就需要对本文给出的Chu空间进程代数进行修改或扩展。
Chu空间的相似性度量是另一个需要研究的问题。传统的软件模型检验方法通常给出一个或0或1的返回值，表示被检验的程序是否满足某一性质。在很多情况下，可能需要一个0,1之间的数值（即：相似性度量），用来表示程序与性质之间的距离。例如：在一个构件库中，需要根据某一性质挑选一个构件，如果库中所有构件都不能满足该性质，那么与该性质距离最近的构件就可以成为备选。由于Chu空间具有二维矩阵的表示方法，可以预见，Chu空间的相似性度量可能具有较好的计算复杂度。