理论计算机科学电子笔记128(2005)161-177www.elsevier.com/locate/entcs用静态通道图分析法阿拉斯泰尔F. Donaldson,Alice Miller,Mu Zhao Calder苏格兰格拉斯哥大学计算机科学系{ally,alice,muffy}@ dcs.gla.ac.uk摘要在过去的十年里,人们对利用对称性来对抗模型检验中的状态爆炸问题产生了很大的兴趣。 虽然模型中的对称性通常是由于被建模系统的拓扑结构中的对称性而产生的,但大多数利用结构对称性的模型检查器仅限于表现出完全对称性的拓扑结构,例如星形和集团。我们定义了一个并发的,消息传递程序的静态通道图,并表明,在一定的限制下,有一个程序的静态通道图的对称性和与程序相关联的Kripke结构的对称性之间的对应关系。这使得检测,并潜在的开发,在系统中的结构对称性与任意拓扑结构。我们的对称检测方法可以处理移动系统中的信道参考通过信道,从而在一个动态的通信结构。我们用Promela建模语言举例说明了我们的结果。关键词:模型检测,对称,并发,分布式系统,形式验证,Promela/SPIN。1介绍模型检查是一种用于并发系统验证的自动化技术[4]。 为了检查一个系统是否满足一组属性,系统的一个抽象的、有限的状态模型是用一种特定的语言写的,属性是用时态逻辑公式表示的。然后,一个叫做模型检查器的软件工具搜索模型的状态空间如果发现违反属性,模型检查器将返回一个通过模型的反示例路径,该路径将导致错误。如果状态空间被彻底搜索并且没有发现违规,那么模型满足属性。只要1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi:10.1016/j.entcs.2005.04.010162A.F. Donaldson等人理论计算机科学电子笔记128(2005)161由于该模型准确地说明了系统与属性相关的行为,因此可以得出结论,该系统满足属性。模型检查对于发现具有罕见发生概率(因此难以检测)和潜在灾难性后果的错误非常有用 作为 因此,模型检查特别适合于关键系统的验证。模型检验受到状态爆炸问题的阻碍。这就是当模型中的组件数量增加时,模型的状态空间支持组合增长,很快变得太大而无法进行可行的检查。模型检测中的许多研究集中在解决状态爆炸问题的方法上。这些方法包括状态的符号表示、抽象、偏序约简和归纳(例如,参见[4])。另一种方法利用系统中固有的对称性[1,2,5,6,11]。并发系统通常包含许多复制的组件,因此,模型检查可能涉及在状态空间的等价区域上进行冗余搜索对称约简技术涉及将搜索限制为等价类代表,并且通常会显著节省内存和验证时间[1,5,6]。然而,大多数利用结构对称性的模型检查器在两个方面受到限制。首先,它们仅限于表现出完全对称性的拓扑结构,如星和团。第二,它们依赖于用户来指定模型中关于对称性的信息。这可能容易出错,并损害了模型检查的自动化,这是其作为验证技术的主要优势之一。我们提出了一种方法来检测任意通信结构的消息传递系统的模型中的结构对称性我们的方法包括分析被建模的系统的静态通道图。使用这种方法的对称性检测可以完全自动化,并且不需要用户提供额外的信息-唯一的要求是模型满足某些限制,这些限制可以自动检查。未来的工作将是使用这些结构对称性来实现对称性约简。1.1结果概述我们定义了并发程序的静态通道图,并表明,在一定的限制下,程序的静态通道图的自同构和与程序相关联的Kripke结构的自同构之间存在对应关系。因此,一个难以处理的大Kripke结构的自同构可以从程序的静态通道图中获得,这通常是一个小图。静态通道图可以是A.F. Donaldson等人理论计算机科学电子笔记128(2005)161163自动确定的复杂性线性的大小的程序。因此,算法的复杂度为O(k)(|X|+N)),其中N是程序的大小,X是程序中变量的集合,k是静态通道图的自同构群的生成器的数量。我们的方法可以处理程序中的通道引用通过通道,导致一个动态的通信结构。2并发程序在整个论文中,我们使用':='表示赋值运算符,'='表示测试相等性的布尔运算符。设D是一个有限数据域,并设D ∈D表示一个未定义值。定义2.1一个并发程序P包括:• 一组同时执行的进程{p,|1 ≤ i ≤ m}对于某个m ≥ 1,• 一组通信信道{c,|m