并发进程系统正确性的验证图式

并发进程系统正确性的验证,比之顺序进程正确性的验证有其特殊意义。并发系统的运行,在执行序列这一级上是非决定的,通常的调试手段,很难暴露系统中依赖于执行序列的那类错误。因此并发系统正确性的验证,在三种不同水平上都是有价值的:完全形式化的形式演绎系统;半形式化的数学证明;或者有效的检查调试方法。 并发系统运行的非决定性,也极大地增加了验证的复杂性。在证明系统具有某个性质时,粗略地说,就是要证明这个系统的所有执行序列都具有这种性质。一个顺序进程,从给定的初始状态出发,只有一个可能的执行序列;但是多个并发进程的可能执行序列则往往是无穷多个。由于这种复杂性禁锢了人们的智力活动,使得一些简单的事实,人们也很难将其严格证明。系统中存在的问题,事后看来即使是一些很明显的问题,也会被这种复杂性掩盖起来,长时间不被发现。