[1]齐蕾蕾,杨庆红*,游 颖.算法的形式化推导与基于Isabelle的自动化验证[J].江西师范大学学报(自然科学版),2018,(04):379-383.[doi:10.16357/j.cnki.issn1000-5862.2018.04.10]
　QI Leilei,YANG Qinghong*,YOU Ying.The Formal Derivation of Algorithm and Automatic Verification Based on Isabelle[J].Journal of Jiangxi Normal University:Natural Science Edition,2018,(04):379-383.[doi:10.16357/j.cnki.issn1000-5862.2018.04.10]
点击复制

算法的形式化推导与基于Isabelle的自动化验证()
分享到：

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

卷:
期数:
2018年04期
页码:
379-383
栏目:
出版日期:
2018-08-20

文章信息/Info

Title:
The Formal Derivation of Algorithm and Automatic Verification Based on Isabelle
文章编号:
1000-5862(2018)04-0379-05
作者:
齐蕾蕾; 杨庆红*; 游 颖
江西师范大学计算机信息工程学院,江西 南昌 330022
Author(s):
QI Leilei; YANG Qinghong*; YOU Ying
College of Computer Information Engineering,Jiangxi Normal University,Nanchang Jiangxi 330022,China
关键词:
形式化方法;  Isabelle定理证明器;  自动化验证;  形式化推导
Keywords:
formal methods;  Isabelle theorem prover;  automatic verification;  formal derivation
分类号:
TP 311.5
DOI:
10.16357/j.cnki.issn1000-5862.2018.04.10
文献标志码:
A
摘要:
可信软件的不断发展进一步推动了形式化方法的深入研究.结合实际应用中的2个问题,采用基于递推关系的算法形式化方法,演示了算法的形式化推导过程,并运用Isabelle定理证明器结合Dijkstra最弱前置谓词方法,对得到的算法程序进行了自动化验证,避免了手工验证过程繁琐和易出错等问题.研究表明:基于递推关系的算法形式化方法不仅可以提高开发算法的效率,而且通过数学变换保证推导过程的正确性,从而有效保证了算法和程序的正确性.
Abstract:
The continuous development of trusted software has further promoted the in-depth study of formal methods.Two formal problems of practical application are introduced,and the formal deduction process of the algorithm is demonstrated by the formal method based on recursive relation.The Isabelle theorem prover is combined with the weakest predicate method of Dijkstra to validate the algorithm automatically,which avoid the problem that manual verification process is tedious and error prone.The research shows that the formal method based on recursive relation can not only improve the efficiency of the algorithm,but also ensure the correctness of the derivation process by mathematical transformation.So this process effectively guarantees the correctness of the algorithm.

参考文献/References:

[1] 彭成,王盼卿.软件形式化开发方法的选择策略研究[J].电子设计工程,2014,22(15):30-36.
[2] 游珍,薛锦云.基于Isabelle定理证明器算法程序的形式化验证[J].计算机工程与科学,2009,31(10):85-89.
[3] 包丽梅,张玉春,张世铮.关于形式化方法与软件可靠性的研究[J].内蒙古民族大学学报:自然科学版,2010,25(2):166-167.
[4] 苏竞秀,龙陈锋.Floyd算法与RAD算法性能分析[J].计算机应用与软件,2015,32(2):116-119.
[5] 雷富兴,张来顺.基于Hoare逻辑的过程调用的形式化方法[J].计算机工程与设计,2011,32(1):197-201.
[6] 杨黄磊,薛锦云.一类单元赋值语句型循环不变式的开发方法研究[J].江西师范大学学报:自然科学版,2014,38(4):378-382.
[7] 刘峰涛,贺国光.基于L_Z方法的宏观交通运输系统复杂性测度[J].哈尔滨工业大学学报,2008,40(12):2058-2061.
[8] 丁湘陵,王志刚.基于B方法的体系结构描述语言的形式化研究[J].计算机工程与科学,2013,35(1):100-106.
[9] 朱威.基于PAR方法的分形算法开发研究[D].河南:郑州大学信息工程大学,2014.
[10] 苏昭.形式化PAR方法及其算法程序规约精化机理[J].江西科技学院学报,2014,9(3):53-57.
[11] 李婉璐.软件工程中的形式化方法研究综述[J].数字技术与应用,2015(10):108-109.
[12] Lawrence C Paulson.A mechanised proof of Godel’s incompleteness theorems using nominal Isabelle[J].J Autom Reasoning,2015(55):1-37.
[13] Li Yongjian,Pang Jun.Formalizing provable anonymity in Isabelle/HOL[J].Formal Aspects of Computing,2015(27):255-282.
[14] Mike Stannett.Using Isabelle/HOL to verify first-order relativity theory[J].J Autom Reasoning,2014(52):361-378.
[15] Filip Maric’.Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL[J].Theoretical Computer Science 2010,411(50):4333-4356.

相似文献/References:

[1]熊小超,杨庆红*.2类组合数学问题的算法形式化推导[J].江西师范大学学报(自然科学版),2019,(04):402.[doi:10.16357/j.cnki.issn1000-5862.2019.04.12]
　XIONG Xiaochao,YANG Qinghong*.The Formal Derivation for Two Kinds of Combinatorial Mathematical Problems[J].Journal of Jiangxi Normal University:Natural Science Edition,2019,(04):402.[doi:10.16357/j.cnki.issn1000-5862.2019.04.12]

备注/Memo

备注/Memo:
收稿日期:2017-11-03
基金项目:国家自然科学基金(61363013)资助项目.
通信作者:杨庆红(1968-),女,江西南昌人,教授,主要从事软件形式化、智能教育软件的研究.E-mail:yangqh120@163.com
更新日期/Last Update: 2018-08-20