一种基于Concurrent Apla语言的共享内存并发分布式算法两层验证方法

 

(1.江西师范大学计算机信息工程学院，江西 南昌 330022;2.江西师范大学物理与通信电子学院, 江西 南昌 330022;3.江西师范大学江西省光电子与通信重点实验室，江西 南昌 330022）

摘要：形式化验证共享内存并发分布式算法已成为当前极具挑战性的问题之一，尤其是在云计算、多核、无线传感器网络、分布式数据库、区块链环境下。本文基于研究团队在形式化规约语言和方法、算法形式推导和验证方面的已有工作，以自定义泛型抽象顺序设计语言Apla为基础，进一步研究并提出简明、高抽象用于并发分布式计算的Concurrent Apla语言，使其既支持顺序算法的验证又能有效地验证并发分布式算法。在依赖-卫式推理的基础上，提出一种新颖的两层并发分布式算法形式化验证方法，其中系统层用于处理并行并发级验证，而组件层用于处理顺序级验证。最后，通过两个实例验证了方法的有效性和可行性。

关键词：并发分布式算法；共享内存；Rely-Guarantee推理；Concurrent Apla；形式化验证