分布式环境下的在线等价性检查优化

"这篇论文探讨了分布式动态等价性检查，一种提高基于需求的等价性检查效率的方法，尤其适用于大型系统。该方法利用布尔方程系统（BESs）来处理分布式环境中的等价性检查，以实现在线验证的性能提升。作者提出了一种新的分布式算法——奥尔夫警长，用于解决BESs，以此优化BISIMULATOR验证引擎，后者是在CADp验证工具箱中基于OpEN/Cimsimulator环境开发的。实验结果显示，分布式版本的BISIMULATOR展现出准线性加速比和良好的可扩展性，与顺序版本相比有显著优势。等价性检查在验证领域至关重要，特别是在协议和服务的比较中，以及安全性分析等方面。" 这篇论文关注的是在理论计算机科学领域中，如何高效地进行分布式动态等价性检查。等价性检查是验证系统是否符合预期行为的关键技术，通常涉及将系统描述（如协议）与期望行为（如服务）进行比较。对于大规模系统，传统的全局等价性检查方法可能因系统太大无法完全构建而变得不切实际。因此，基于需求的等价性检查应运而生，它能以需求驱动的方式逐步探索两个标注转换系统（LTSs）的等价关系，即使在系统无法加载进内存的情况下也能检测出错误。 文章介绍了一个新算法——奥尔夫警长，用于分布式解决布尔方程系统，这是等价性检查中的一个重要组成部分。BESs被用来表示和分析LTSs之间的关系。通过DSOLVE，一个分布式版本的BIMSIMULATOR验证引擎，可以在线执行这些检查。实验数据证明，这种方法提供了准线性加速比，并且在可扩展性方面表现出色，相对于单机版本的BISIMULATOR有显著改进。 等价性检查不仅应用于一致性验证，还涉及到安全性属性的评估。论文引用了多种相关研究，强调了在标记转换系统框架下进行等价性检查的重要性。通过分布式计算技术，等价性检查的有效性和效率得到了提升，这对于处理日益复杂和庞大的系统验证问题来说，是一个重要的进展。