發(fā)布時(shí)間：2021-07-22 15:54

　　形式化驗(yàn)證共享內(nèi)存并發(fā)分布式算法已成為當(dāng)前極具挑戰(zhàn)性的問題之一,尤其是在云計(jì)算、多核、無(wú)線傳感器網(wǎng)絡(luò)、分布式數(shù)據(jù)庫(kù)、區(qū)塊鏈環(huán)境下.該文基于研究團(tuán)隊(duì)在形式化規(guī)約語(yǔ)言和方法、算法形式推導(dǎo)和驗(yàn)證方面的已有工作,以自定義泛型抽象順序設(shè)計(jì)語(yǔ)言Apla為基礎(chǔ),進(jìn)一步研究并提出簡(jiǎn)明、高抽象用于并發(fā)分布式計(jì)算的Concurrent Apla語(yǔ)言,使其既支持順序算法的驗(yàn)證又能有效地驗(yàn)證并發(fā)分布式算法.在依賴-衛(wèi)式推理的基礎(chǔ)上,提出一種新穎的2層并發(fā)分布式算法形式化驗(yàn)證方法,其中系統(tǒng)層用于處理并發(fā)級(jí)驗(yàn)證,而組件層用于處理順序級(jí)驗(yàn)證.最后,通過2個(gè)實(shí)例驗(yàn)證了該方法的有效性和可行性. 

【文章來(lái)源】：江西師范大學(xué)學(xué)報(bào)(自然科學(xué)版). 2020,44(03)北大核心

【文章頁(yè)數(shù)】：6 頁(yè)

【文章目錄】：
0 引言
1 基于共享內(nèi)存的并發(fā)分布式計(jì)算的Concurrent Apla語(yǔ)言
    1.1 Concurrency Apla語(yǔ)法
    1.2 Concurrency Apla結(jié)構(gòu)化操作語(yǔ)義
2 基于Concurrent Apla語(yǔ)言的共享內(nèi)存并發(fā)分布式算法2層驗(yàn)證方法
    2.1 依賴-衛(wèi)式規(guī)約
    2.2 2層共享內(nèi)存并發(fā)算法驗(yàn)證方法
3 案例研究
    3.1 并發(fā)執(zhí)行x:=x+1
    3.2 并發(fā)求M,N最大公約數(shù)
4 結(jié)束語(yǔ)



本文編號(hào)：3297445