[1]王昌晶,余小军,沈德明,等.一种基于Concurrent Apla语言的共享内存并发分布式算法2层验证方法[J].江西师范大学学报(自然科学版),2020,(03):301-306.[doi:10.16357/j.cnki.issn1000-5862.2020.03.14]
　WANG Changjing,YU Xiaojun,SHEN Deming,et al.The Two-Level Verification Method of Shared Memory Concurrent Distributed Algorithm Based on Concurrent Apla Language[J].Journal of Jiangxi Normal University:Natural Science Edition,2020,(03):301-306.[doi:10.16357/j.cnki.issn1000-5862.2020.03.14]
点击复制

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

《江西师范大学学报》（自然科学版）[ISSN:1006-6977/CN:61-1281/TN]

卷:
期数:
2020年03期
页码:
301-306
栏目:
信息科学与技术
出版日期:
2020-06-10

文章信息/Info

Title:
The Two-Level Verification Method of Shared Memory Concurrent Distributed Algorithm Based on Concurrent Apla Language
文章编号:
1000-5862(2020)03-0301-06
作者:
王昌晶1; 余小军1; 沈德明2; 罗海梅3; 4;  左正康1*
1.江西师范大学计算机信息工程学院,江西 南昌 330022; 2.江西科技师范大学通信与电子学院,江西 南昌 330013; 3.江西师范大学物理与通信电子学院, 江西 南昌 330022; 4.江西师范大学江西省光电子与通信重点实验室,江西 南昌 330022
Author(s):
WANG Changjing1; YU Xiaojun1; SHEN Deming2; LUO Haimei3; 4; ZUO Zhengkang1*
1.College of Computer Information Engineering,Jiangxi Normal University,Nanchang Jiangxi 330022,China; 2.School of Communication and Electronics,Jiangxi Science and Technology Normal University,Nanchang Jiangxi 330013,China; 3.College of Physics and Communication Electronics,Jiangxi Normal University,Nanchang Jiangxi 330022,China; 4.Key Laboratory of Photoelectronics and Tel-ecommunication of Jiangxi Province,Jiangxi Normal University,Nanchang Jiangxi 330022,China
关键词:
并发分布式计算;  依赖-卫式推理;  Concurrent Apla;  形式化验证
Keywords:
concurrent distributed computing;  rely guarantee reasoning;  concurrent Apla;  formal verification
分类号:
TP 311
DOI:
10.16357/j.cnki.issn1000-5862.2020.03.14
文献标志码:
A
摘要:
形式化验证共享内存并发分布式算法已成为当前极具挑战性的问题之一,尤其是在云计算、多核、无线传感器网络、分布式数据库、区块链环境下.该文基于研究团队在形式化规约语言和方法、算法形式推导和验证方面的已有工作,以自定义泛型抽象顺序设计语言Apla为基础,进一步研究并提出简明、高抽象用于并发分布式计算的Concurrent Apla语言,使其既支持顺序算法的验证又能有效地验证并发分布式算法.在依赖-卫式推理的基础上,提出一种新颖的2层并发分布式算法形式化验证方法,其中系统层用于处理并发级验证,而组件层用于处理顺序级验证.最后,通过2个实例验证了该方法的有效性和可行性.
Abstract:
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.

参考文献/References:

[1] 王戟,詹乃军,冯新宇,等.形式化方法概貌[J].软件学报,2019,30(1):33-61.
[2] 贺飞,张立军.软件形式化验证专题前言[J].软件学报,2019,30(7):1901-1902.
[3] 刘震伟,薛锦云,夏鲸,等.PAR平台中并发分布式事务处理机制及其应用研究[J].江西师范大学学报:自然科学版,2019,43(6):649-654.
[4] 王捍贫,张磊.形式化方法在云计算中的应用现状[J].广州大学学报:自然科学版,2019,18(4):69-74.
[5] 马凯旋.基于云计算平台的形式化技术相关并行查询与检测算法的研究[D].南京:南京邮电大学,2018.
[6] 许明,开金宇,肖蕾.反应式软件形式化系统研究系统分析[J].哈尔滨商业大学学报:自然科学版,2014,30(4):477-481.
[7] Burrows M,Abadi M,Needham R M.A logic of authentication[J].Mathematical and Physical Sciences,1989,426(1871): 233-271.
[8] Clarke E M J,Grumberg O,Peled D A.Model checking[M].San Mateo:MIT Press,1999.
[9] 薛锦云.PAR方法抽象程序设计语言Apla技术报告[R].江西师范大学省高性能计算技术重点实验室,2010.
[10] Jones C B.Tentative steps toward a development method for interfering programs[J].ACM Transactions on Programming Languages and Systems(TOPLAS),1983,5(4):596-619.
[11] Armstrong A,Gomes V B F,Struth G.Algebraic principles for rely-guarantee style concurrency verification tools[EB/OL][2019-10-16].https://ui.adsabs.harvard.edu/abs/2013arXiv1312.1225A/.
[12] Liang Hongjin,Feng Xinyu,Fu Ming.Rely-guarantee-based simulation for compositional verification of concurrent program transformations[J].ACM Transactions on Programming Languages and Systems(TOPLAS),2014,36(1):3.
[13] Gavran I,Niksic F,Kanade A,et al.Rely/guarantee reasoning for asynchronous programs[EB/OL][2019-10-16].https://drops.dagstuhl.de/opus/volltexte/2015/5390/.
[14] Fedorchenko I M,Markovskii E A,Tikhonovich V I,et al.Verification of parallel shared-memory programs,Owicki-Gries method of axiomatic[EB/OL][2019-10-16].https://link.springer.com/referenceworkentry/10.1007/978-0-387-09766-4_2090.
[15] Lengauer C.Owicki-Gries method of axiomatic verification[EB/OL][2019-10-16].http://dx.doi.org/10.1007/978-0-387-09766-4_182.
[16] Kojima K,Igarashi A.A hoare logic for SIMT programs[EB/OL][2019-10-16].http://www.fos.kuis.kyoto-u.ac.jp/～kozima/hl-simt-full.pdf.
[17] Norbert S.Verification of sequential imperative programs in Isabelle-HOL[EB/OL][2019-10-16].http://www-wjp.cs.uni-sb.de/leute/private_homepages/nschirmer/pub/schirmer_phd.pdf.
[18] Nipkow T,Nieto L P.Owicki/Gries in Isabelle/HOL[EB/OL][2019-10-16].https://dl.acm.org/doi/10.5555/645367.650813.
[19] Nieto L P.The rely-guarantee method in Isabelle/HOL[EB/OL][2019-10-16].https://dl.acm.org/doi/10.5555/645367.650813.

备注/Memo

备注/Memo:
收稿日期:2020-03-19
基金项目:国家自然科学基金(61762049,11804133,61862033,61662035,61902162),国家留学基金(202008360094),江西省科技厅课题(20181BAB206034)和江西省研究生创新基金(YC2019-S161)资助项目.
作者简介:王昌晶(1977-),男,江西南昌人,教授,博士,博士生导师,主要从事可信软件、智能化软件与智能化教育的研究.E-mail:wcj771006@163.com
通信作者:左正康(1980-),男,江西抚州人,教授,博士,主要从事泛型程序设计和可信软件的研究.E-mail:kerrykaren@126.com
更新日期/Last Update: 2020-06-10