论文部分内容阅读
在科技高速发展的今天,C语言由于其自身的优势已经成为最主流的程序设计语言之一,被广泛应用于各个领域的软件实现中。然而C语言中的数组越界问题和除数为零问题屡见不鲜,这些问题往往会造成程序出错,甚至可能导致系统崩溃,因此保障C程序的正确性有着重要意义。形式化方法作为对系统正确性进行验证的一种重要方法,它通过使用相关的数学理论来验证系统是否满足相应的规范,从而从根本上保障了系统的正确性。而区间时序逻辑语言(Modeling,Simulation and Verification Language,MSVL)就是形式化验证中常用的一种建模、仿真和验证语言,已广泛应用于实时系统的验证中。本文主要研究了C程序到MSVL程序的自动转换,取得了以下研究成果:1.研究了现有的多种C程序模型检测工具的工作原理,指出了它们存在的一些不足,如难以保障所提取模型与程序的一致性。给出了一种对C程序正确性进行验证的方法。首先将C程序直接转换为MSVL程序,并以生成的MSVL程序作为模型,将对C程序正确性的验证转换为对MSVL程序正确性的验证,然后使用命题投影时序逻辑(Propositional Projection Temporal Logic,PPTL)公式描述待验证系统的性质,最后通过MSV解释器对MSVL程序进行验证。2.分别对C语言以及MSVL语言进行了研究,并从词法、语法等方面细致地分析了C语言和MSVL语言之间的异同,设计并给出了C程序到MSVL程序的转换规则。3.研究了编译器及自动转换系统的工作原理,给出了C-to-MSVL程序转换系统的基本框架,并依据功能将系统划分为五大功能模块,同时给出了各个模块的实现方案,最终使用Visual C++&Lex&Yacc实现了C-to-MSVL程序转换系统。4.通过“狼羊菜”问题和“二十四组合数”问题展示了C-to-MSVL程序转换系统的可用性与实用性。通过“狼羊菜”问题展示了本转换系统的转换过程以及MSV解释器的仿真和验证过程,说明了本转换系统的可用性。通过对“二十四组合数”问题的源码进行转换并对生成的MSVL程序进行仿真,发现了源C代码中存在的除数为零和数组越界错误,说明了本转换系统的实用性。