带参并发系统的模型检测

带参并发系统 实际包含一族并发系统实例，其中以一个（或多个）参数表示每个系统实例的规模，比如实例系统中 并发执行的进程个数或数据域的大小。带参模型检测的任务是验证 对任意的参数数值，所有的系统实例都满足所期望的性质。本文研究带参并发系统的模型检测方法和技术。 一般来说， 带参系统的参数不仅代表进程个数，也可以是通信缓冲区容量、数据域大小、数据通路宽度等。然而迄今为止，该领域的绝大多数研究都 针对前者类型的参数，而往往忽视数据方面的参数。本文中，我们提出基于带符号迁移图的复合型带参网络协议建模框架。 系统表示为顺序结构的“结点进程”的并发复合，彼此通过“信道进程”进行通讯；性质以一种嵌套谓词等式系形式的一阶$\mu$ 演算表达；进而相应扩展由实验室自主开发的传值进程模型检测工具，对于数据带参的并发系统给出有效的验证方法， 并且对于一些典型的带参系统作出实例研究。 出乎意料的是，在GERMAN2004 协议的缓存一致性已经被其他研究者证明正确的情况下，我们却发现了它在于数据一致性方面的一个严重错误，并予以更正。 进一步，应用我们检测工具中所实现的“数据无关”技术，我们有效推广了研究结论，证明了对于任意大小的数据域， 修改后的GERMAN协议仍然保证满足数据一致性要求。 环境抽象的方法将计数抽象的思想借鉴到谓词抽象的技术中，对于控制带参的并发系统给出一般性验证框架。然而该方法具有相当 高的复杂度；对于很多实际应用的系统而言，所构造的抽象系统规模仍然超出常用模型检测工具所能处理的范围。为了克服这个困难， 我们提出了{\em 状态聚类}方法，在 局部可达性分析的基础上，通过对系统表达式的分析把全部可达的局部状态分组成为少数几个状态簇。在进行 状态聚类的启发式算法中，我们采用了先分裂后聚合的策略，即在识别出不同类的具有代表性的状态配置后，再将类似的状态尽可能 合并到同一个状态簇。这样局部状态被相应划分成为若干等价类，每个类以一个单元状态为代表。然后我们在系统描述的层次上， 通过程序重写的方式直接构造生成对应的抽象系统。 实例研究显示，状态聚类方法通常能够将抽象节点的大小缩减约3个数量级。 参数抽象作为带参系统的安全性性质验证的另外一个有效方法，其最困难之处在于找到合适的辅助不变量，用以进行卫加强 以精化抽象模型。针对这个问题，我们提出一种启发式的方法，通过在参考模型中计算自动产生辅助不变量。 利用这一技术，我们将参数截断的思想应用于 处理环境抽象中依赖于参数类型的复杂变量，使得环境抽象在状态聚类后得到进一步优化。我们有效结合了参数抽象与环境抽象技术， 显著降低了抽象系统状态空间规模，从而极大节省了模型检测的内存开销；并且由于抽象中的每个 步骤都以现行的模型检测工具辅助计算，整个验证过程可以机械化完成，不需要过多的人工介入。作为示范，对于 工业应用的复杂的缓存一致性协议FLASH，我们在保留了其中最为著名的“三跳”事务处理的情况下，验证了缓存一致性和数据一致性。 据我们所知，这是首次这样工业实用的复杂协议能够同时在控制方面和数据方面在如此的精度上得到成功验证。