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

发布时间：2021-07-22 15:54

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

【文章来源】：江西师范大学学报(自然科学版). 2020,44(03)北大核心

【文章页数】：6 页

【文章目录】：
0 引言
1 基于共享内存的并发分布式计算的Concurrent Apla语言
    1.1 Concurrency Apla语法
    1.2 Concurrency Apla结构化操作语义
2 基于Concurrent Apla语言的共享内存并发分布式算法2层验证方法
    2.1 依赖-卫式规约
    2.2 2层共享内存并发算法验证方法
3 案例研究
    3.1 并发执行x:=x+1
    3.2 并发求M,N最大公约数
4 结束语



本文编号：3297445