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

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

The Two-Level Verification Method of Shared Memory Concurrent Distributed Algorithm Based on Concurrent Apla Language

Formal verification of concurrent distributed algorithms for shared memory has become one of the most challenging problems,especially in cloud computing,multi-core,wireless sensor networks,distributed databases and blockchain environments.Based on the existing work of the research team in the formal specification language and method,derivation and validation algorithm form aspects,order to customize the generic abstract design language Apla,the concise,high abstraction for concurrent distributed computing concurrent Apla language is put forward,which supports both sequential algorithm verification and validation of concurrent distributed algorithm effectively.On the basis of rely guarantee reasoning,a novel formal verification method of two-layer concurrent distributed algorithm is proposed,in which the system layer is used for concurrency level verification and the component layer is used for sequential level verification.Finally,the validity and feasibility of the method are verified by two examples.