[1]王昌晶,贺江飞,罗海梅,等.模型驱动的Dafny程序形式化生成与自动验证[J].江西师范大学学报(自然科学版),2020,(04):378-384.[doi:10.16357/j.cnki.issn1000-5862.2020.04.09]
　WANG Changjing,HE Jiangfei,LUO Haimei,et al.The Model-Driven Dafny Program Generation and Automatic Verification[J].Journal of Jiangxi Normal University:Natural Science Edition,2020,(04):378-384.[doi:10.16357/j.cnki.issn1000-5862.2020.04.09]
点击复制

模型驱动的Dafny程序形式化生成与自动验证()
分享到：

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

卷:
期数:
2020年04期
页码:
378-384
栏目:
信息科学与技术
出版日期:
2020-08-10

文章信息/Info

Title:
The Model-Driven Dafny Program Generation and Automatic Verification
文章编号:
1000-5862(2020)04-0378-07
作者:
王昌晶1; 贺江飞1; 罗海梅2; 3; 左正康1*; 许 帆</sup>1
1.江西师范大学计算机信息工程学院,江西 南昌 330022; 2.江西师范大学物理与通信电子学院,江西 南昌 330022; 3.江西师范大学江西省光电子与通信重点实验室,江西 南昌 330022
Author(s):
WANG Changjing1; HE Jiangfei1; LUO Haimei2; 3; ZUO Zhengkang1*; XU Fan1
1.College of Computer Information Engineering,Jiangxi Normal University,Nanchang Jiangxi 330022,China; 2.College of Physics and Communication Electronics,Jiangxi Normal University,Nanchang Jiangxi 330022,China; 3.Key Laboratory of Photoelectronics and Telecommunication of Jiangxi Province,Jiangxi Normal University,Nanchang Jiangxi 330022,China
关键词:
模型驱动;  Dafny程序;  循环不变式;  形式化生成;  自动验证
Keywords:
model driven;  Dafny program;  loop invariant;  formal generation;  automatic verification
分类号:
TP 311
DOI:
10.16357/j.cnki.issn1000-5862.2020.04.09
文献标志码:
A
摘要:
Dafny是一种内置规范结构的编程语言和静态程序证明器,它能验证程序的功能正确性以及将证明过程自动化,这既提高了软件开发的效率,又极大增强了软件开发的可靠性.该文探索了一种模型驱动的Dafny程序形式化生成的方法.首先,从问题的Radl规约出发,根据规约变换技术得到其Radl算法; 然后,根据PAR方法中循环不变式开发新策略得到问题的循环不变式; 最后,在Radl算法和循环不变式基础上利用模型等价转换规则生成Dafny程序,并由Dafny证明器自动验证其功能正确性.用该方法解决了2个典型问题的算法程序开发与验证,证实了该方法能够有效地提高Dafny程序的生成效率和可靠性.
Abstract:
Dafny is a programming language with built-in specification structure and a static program prover.It can verify the program's functional correctness and automate the certification process.This not only improves the efficiency of software development,but also greatly enhances the reliability of software development.A model-driven method for the formal generation of Dafny programs is explored in the paper.Firstly,the Radl algorithm is derived from the Radl specification of the problem according to the protocol transformation technology.Then,a new strategy is developed based on the loop invariant of the PAR method to obtain the loop invariance of the problem.Finally,based on Radl algorithm and loop invariant,Dafny program is generated using model equivalent transformation rules,and its functional correctness is automatically verified by Dafny prover.The method proposed in this paper solves two typical problems of algorithm program development and verification,and it is proved that this method can effectively improve the generation efficiency and reliability of Dafny programs.

参考文献/References:

[1] 王戟,詹乃军,冯新宇,等.形式化方法概貌[J].软件学报,2019,30(1):33-61.
[2] Rustan K,Leino M.Accessible software verification with Dafny[J].IEEE Software,2017,34(6):94-97.
[3] Xue Jinyun,Zheng Yujun,Hu Qimin,et al.PAR:a practicable formal method and its supporting platform[EB/OL].[2019-06-16].https://link.springer.com/chapter/10.1007/978-3-030-02450-5_5.
[4] Ke Wei,Li Xiaoshan,Liu Zhiming,et al.rCOS:a formal model-driven engineering method for,component-based software[J].The frontier of Chinese Computer Science:English Version,2012,6(1):17-39.
[5] 胡启敏,薛锦云,游珍,等.PAR平台中若干软件构件形式化验证技术研究[J].计算机工程与科学,2018,40(2):268-274.
[6] 杨黄磊,薛锦云.一类单元赋值语句型循环不变式的开发方法研究[J].江西师范大学学报:自然科学版,2014,38(4):378-382.
[7] 万松松,薛锦云,谢武平.循环不变式开发技术研究[J].计算机工程与科学,2010,32(9):84-88.
[8] 游珍.Isabelle定理证明器的剖析及其在PAR方法/PAR平台中的应用[D].南昌:江西师范大学,2009.
[9] Leino K R M.Dafny:an automatic program verifier for functional correctness[EB/OL].[2019-06-16].https://dl.acm.org/doi/10.5555/1939141.1939161.
[10] Barnett M,Chang B Y E,Deline R,et al.Boogie:a modular reusable verifier for object-oriented programs[EB/OL].[2019-06-16].https://link.springer.com/chapter/10.1007%2F11804192_17.
[11] Moura L D,Nikolaj Bjørner.Z3:an efficient SMT solver[J].Tools and Algorithms for the Construction and Analysis of Systems,14th International Conference,2008,4963:337-340.
[12] 冉小晓.Radl→Apla自动程序转换系统研究与实现[D].南昌:江西师范大学,2005.
[13] 杨晨.基于PAR平台的最弱前置谓词生成器的设计与实现[D].南昌:江西师范大学,2010.
[14] Jean-Christophe Filliâtre,Paskevich A.Why3:where programs meet provers[J].Lecture Notes in Computer Science,2013,7792:125-128.
[15] 游珍,薛锦云.基于Isabelle定理证明器算法程序的形式化验证[J].计算机工程与科学,2009,31(10):85-89.
[16] 李智,庞柳,刘国源,等.一种模型驱动的软件需求分析方法及技术支持[J].广西师范大学学报:自然科学版,2013(2):22-29.
[17] Saleh I,Kulczycki G,Blake M B.Formal specification and verification of data-centric service composition[C].Miami,Florida:IEEE,2010:131-138.
[18] Iman Saleh.Formalizing data-gentric web services[M].New York:Springer,2015:1-126.

备注/Memo

备注/Memo:
收稿日期:2019-10-17
基金项目:国家自然科学基金(61762049,11804133,61862033)和江西省科技厅课题(2020BABL202025,2020BABL202026,2018BAB206034)资助项目.
作者简介:王昌晶(1977-),男,江西南昌人,教授,博士,博士生导师,主要从事泛型程序设计和可信软件的研究.E-mail:wcj771006@163.com
通信作者:左正康(1980-),男,江西抚州人,教授,博士,主要从事泛型程序设计和可信软件的
更新日期/Last Update: 2020-08-10