论文部分内容阅读
随着计算机软硬件系统日益复杂，如何保证其正确性和可靠性已经成为日益紧迫的问题。对于并发系统，由于其内在的非确定性，这个问题难度更大。在过去的几十年间，各国研究人员为解决这个问题付出了巨大的努力，取得了重要的进展。模型检测的方法就是在这种需求下产生的一种有效的解决方法。
模型检测的研究始于上世纪八十年代初，当时Clarke，Emerson等人提出了用于描述并发系统性质的CTL逻辑，设计了检测有穷状态系统是否满足给定CTL公式的算法，并实现了一个原型系统。这一工作为对并发系统的性质的自动化验证开辟了一条新的路径，成为近二十五年来计算机科学基础研究的一个热点。随后不久出现的符号模型检测技术使这一方法向实际应用性迈出了关键的一步。
模型检测已被应用于计算机硬件、通信协议、控制系统、安全认证协议等方面的分析与验证中，取得了令人瞩目的成功，并从学术界辐射到了产业界。许多公司，如Intel、HP、Phillips等成立了专门的小组负责将模型检测技术应用于生产过程中。
模型检测的基本思想是用状态转换系统M表示系统的行为，用时态逻辑公式A描述系统的性质。这样“系统是否具有所期望的性质”就转化为数学问题“状态转换系统M是否是公式φ的一个模型?”，用公式表示为M┟φ。对有穷状态系统，这个问题是可判定的，即可以用计算机程序在有限时间内自动验证。
1962年，Carl Adam Petri在他的博士论文中首次提出了Petri网的概念。简单的说，Petri网是一种能够应用于多种系统的图形化数学建模工具。对于描述和研究并发，分布式，并行，随机以及非确定性的信息处理系统而言，它是一种很有发展前景的工具。作为一个图形化的工具，Petri网类似于流程图，结构图和网络图，有利于可视化的交流协作。作为一个数学工具，它可以帮助建立状态方程，代数方程以及其他反映系统行为的数学模型。它是完全形式化的。正因如此，我们才可能对被建模过程的性质进行准确的判断。目前，针对Petri网的分析技术和工具已得到广泛发展。
工作流是为了帮助实现信息系统对复杂商务进程各个方面的控制，模拟和支持而产生的。由于Petri网的上述优点，它很快地被应用于工作流中，基于Petri网的工作流就此产生。
本文主要做了两个方面的工作：
第一，正确性是工作流进程定义中必须满足的最低要求。它与工作流的动态性质有关。现存有很多工具可以对基于Petri网的工作流进行正确性验证，如Woflan等。不过，这些工具都是基于显式的可达状态的枚举，从而很有可能在并发迁移中的互相影响而遇到状态爆炸问题。一个基于Petri网的商务进程(工作流)典型的工业应用有50-1000个库所和迁移。如果Petri网是k—有界的，那它的可达状态就有k1000个。一些现存的验证工具如Woflan等只能处理2×106个可达状态。因此，我们可以借助发展比较成熟的模型检测工具如SMV，NuSMV，Spin对工作流进行正确性验证。
首先用时态逻辑CTL表达了正确性所要求的三个性质并且进行了严格的证明，然后将CTL公式转换为符号模型检测软件可以识别的输入文件进行验证。这一类检测工具的重要特征就在于发现被检测模型不满足预先给出性质的时候会自动给出一个反例。根据这个反例，我们就能判断出问题出在模型的哪一个部分，从而对工作流进行进一步修正，最终得到一个正确的工作流。松弛正确性是工作流中另外一个应用广泛的性质，它对系统的要求稍弱，我们应用同样的方法对它进行了验证，在与验证正确性过程唯一不同的是在验证松弛正确性时我们用LTL而非CTL描述了系统需要满足的性质，但这对验证本身没有太大的影响。最后的实验表明，符号模型检测确实可以处理工作流的正确性验证问题。
第二，正确性只是一个工作流需要满足的最低要求，在实际的应用中还有许多其他性质需要得到验证。时态逻辑公式的表达能力是否能够正确的表达这些性质是一个很有趣的问题。如果时态逻辑的表达能力足够强大，那么符号模型检测就有充分的理由成为工作流验证的一个工具。
为此，本文选取了一些比较重要而常用的性质，如决定可达状态集合的可达性，保证每个传递都能最终被激活的活性，限制每个库所内的托肯数不能超过一定数量的有界性以及可逆性，原状态，可覆盖性，持续性等，用时态逻辑公式将它们一一表述并作了详细的证明。我们得到的这些结果表明时态逻辑的表达能力能够很好的处理大部分工作流的性质。应用与验证正确性和松弛正确性相同的方法，我们也可以用符号模型检测的软件读取用时态逻辑公式表达的这些性质并加以验证。
在未来的工作中，我们确定了两个方向：
首先，选取比较大型的工作流例子，尤其是那些由于状态爆炸导致Woflan无法完成的工作流，应用符号模型检测工具进行验证它们的正确性。
其次，工作流中有许多较为复杂的性质，但是在实际应用中又无法避免，我们尝试用CTL或者LTL将它们表达出来，探索时态逻辑在工作流中的表达极限。