计算机工程 ›› 2019, Vol. 45 ›› Issue (10): 64-69,77.doi: 10.19678/j.issn.1000-3428.0053152

• 体系结构与软件技术 • 上一篇    下一篇

汇编级顺序语句块的自动形式化规约及其验证

祁龙云1, 吕小亮1, 路红2, 黄皓2   

  1. 1. 南京南瑞信息通信科技有限公司, 南京 210003;
    2. 南京大学 计算机软件新技术国家重点实验室, 南京 210023
  • 收稿日期:2018-11-16 修回日期:2019-01-21 出版日期:2019-10-15 发布日期:2019-01-29
  • 作者简介:祁龙云(1979-),男,工程师,主研方向为形式化验证、可信计算;吕小亮,工程师;路红,讲师、博士研究生;黄皓,教授、博士。
  • 基金项目:
    国家电网公司2018年总部科技项目"可信嵌入式操作系统关键技术研究"(SGJSNT00FZJS1800129)。

Automatic Formal Specification and Its Verification of Assembly-Level Sequential Statement Blocks

QI Longyun1, Lü Xiaoliang1, LU Hong2, HUANG Hao2   

  1. 1. NARI Information and Communication Technology Co., Ltd., Nanjing 210003, China;
    2. State Key Laboratory for Novel Software Technology at Nanjing University, Nanjing 210023, China
  • Received:2018-11-16 Revised:2019-01-21 Online:2019-10-15 Published:2019-01-29

摘要: 软件的形式化验证是保障软件可证明性、可靠性和安全性的重要手段,但传统形式化验证脚本的生成过程复杂且需要形式化验证专家的大量手工验证。为提高证明效率,构建一种自动证明模型,并在此基础上提出语义自动规约算法以及对所规约的语义自动生成证明脚本的算法。利用C++和Python并通过交互式定理证明器Isabelle 2017在基准数据中随机选择10个程序进行测试,结果表明,与完全人工操作相比,该算法具有较高的验证效率,可实现顺序语句块的自动化规约与验证。

关键词: 自动形式化规约, 自动化验证, 定理证明器, 交互式定理, 形式化验证

Abstract: Formal verification of software is an important means to guarantee the provability,reliability and security of software, but the generation process of traditional formal verification script is complex and requires a lot of manual verification of formal verification experts.In order to improve the efficiency of proof,this paper constructs an automatic proof model,and on this basis,proposes a semantic automatic specification algorithm and its automatic generation algorithm for generating proof scripts.Using C++ and Python and randomly selecting 10 programs in the benchmark data by the interactive theorem prover Isabelle 2017 to run the test,results show that compared with the fully manual operation,the algorithm has higher verification efficiency,and can implement automatic specification and verification of sequential statement.

Key words: automatic formal specification, automatic verification, theorem prover, interactive theorem, formal verification

中图分类号: