模型检测是保证程序正确性的一条重要途径,它最大的优点就是验证过程完全自动化。然而,模型检测在规模大、复杂度高的系统的应用中却碰到了所谓状态空间爆炸问题——对很多系统来说,其运行过程中所产生的系统状态数目往往随着系统规模的扩大和及其子模块数目的增加而呈现指数增长。这直接导致很多系统的规模超出了当前验证工具的能力范围。 SPIN是贝尔实验室开发的面向分布式软件系统的模型检测器。SPIN在应用过程中同样面临状态空间爆炸问题,它采用偏序归约策略来减少状态空间中需要遍历及存储的状态数目。还有另一种完全不同的策略是减少每个系统状态所需的存储空间,这属于内存压缩技术的范畴。 本文提出了一种基于SPIN的无损压缩技术——基于属性的状态向量优化(SOBP),它利用系统属性的特点,以一个变量替换多个变量的方式对状态向量进行优化,从而实现状态压缩。而且,当该算法与collapse compression结合使用时,将使collapse compression更加强大,从而进一步减少状态存储空间。与SPIN中其它无损压缩算法一样,该压缩算法在实现状态压缩的同时,也是以增加运行时间作为代价的。