【作者】 刘自恒；

【导师】 曾庆凯；

【作者基本信息】 南京大学 ， 计算机软件与理论， 2012， 硕士

【摘要】 软件作为信息系统的实现载体,广泛应用在各个领域,软件中的任何安全漏洞或错误的实现都可能导致非常严重的后果。通过大量的测试可以提高软件的可靠性,但成本较高,也不能完全保证软件的可靠。形式化证明方法基于严密的数学和逻辑基础,经过正确性证明的程序可以保证软件符合指定的程序规范,从而大大提高软件可靠性。程序正确性证明的一个关键问题是发现充分的循环不变式信息来辅助、支撑证明过程的完成。由人工寻找循环不变式工作繁琐,容易出错。因此,研究如何自动地有效分析和生成循环不变式,使得软件证明过程顺利完成,成为形式化方法研究领域的一个重要研究课题。本文主要针对软件验证技术中的循环不变式生成技术进行研究和实现：(1)对形式化程序分析方法主要理论进行总结。本文根据形式化分析中用到的主要理论的不同对形式化分析技术进行总结。对各自的理论核心、主要解决的问题、典型工具进行了阐述。在此基础上,指出形式化证明过程的难点,并总结了当前克服这些难点所采用的方法。(2)介绍和总结了目前求解循环不变式的主要研究状况和现有方法。根据他们主要理论和适用范围的不同进行阐述,指出了目前工作存在的不足。(3)本文提出了一种基于条件赋值转换和自适应模板技术的循环不变式生成方法。根据程序控制流结构、依赖分析结果和值分析结果,生成可能的循环不变式,然后由定理证明器求解。该方法可以自动地运行,并将结果以ACSL注释的形式添加到程序中,辅助完成程序属性的证明过程。(4)基于上述方法,在Frama-C平台和APRON库的基础上,实现了一个分析插件loopInv。选取了一些程序作为分析对象,与其他方法作了比较,结果表明可以发现更多的不变式,使一些程序规范顺利得到证明。更多还原

【Abstract】 Software has been used widely in various areas as the carrier of information systems. Any vulnerability or incorrect development in software will cause highly serious failures. It can increase the confidence with enough testing which will be very expensive. Unfortunately, it still cannot guarantee that the software to be tested is fully reliability even with lots of testing. Formal methods are based on strict mathematically and logically basis. It can ensure that the software meets its given specifications through proving of correctness, which greatly improves the reliability of software.A key issue in program proving is finding sufficient loop invariants to assist the automatic process. However, writing loop invariants manually is boring and error-prone. Thus, the research on how to analysis and generate loop invariants automatically becomes an important issue in the area of formal methods. This dissertation focused on the generation of loop invariants and mainly covers the subjects of theory of formal methods and generation technologies for invariants.(1)We summarized the main theories of formal methods to analysis programs. It is focused on the core theory, the main problem to resolve and classical tools. Then we point out the difficulty of formal proof.(2) We summarized recent research and common technologies for generating loop invariants. They are described and compared from many aspects, including the kinds of programs to be analyzed, the way how they work and their shortcomings.(3) Based on conditional assignment and adaptive template an approach to generate invariants is proposed in this dissertation. Many semantic factors are considiered here, not only loop itself but also specifications, asserts etc.. It infers potential loop invariants according to CFG, PDG and value analysis which are then resolved by theory prover. It can run automatically and insert invariants as ACSL comments into C codes as output.(4)Based on the method above, a plugin named looplnv is designed and implemented with the platform Frama-C and APRON. According to the experiments on some selected programs, it can generate more invariants comparing with other tools and most of the programs can be proved successfully.更多还原