论文部分内容阅读
随着软件复杂度的不断增加、应用领域的不断扩大,人们对软件可靠性的需求日益迫切,如何保证软件的可靠性成为软件工程领域的一个焦点问题。传统的软件测试只能发现错误,不能保证程序正确。形式化方法被认为是解决软件可靠性的一个有效途径,但形式化语言较难掌握,一般开发人员直接书写比较困难。基于此,本文提出了一种基于规约模式的、用于描述C程序性质的半形式化语言C-PDL,研究了从C-PDL到模型检测工具SPIN输入语言的转换过程,最后采用SPIN验证C程序是否满足C-PDL描述的性质。规约模式是根据常用时序逻辑公式抽象而成的一种半形式化表达模式,用其描述的性质有对应的LTL表达式。现有规约模式的语义较含糊,导致用其描述的性质可以对应不同的LTL表达式,目前有SPS和Prospec两种版本。本文以SPS为标准,基于SPIN工具验证LTL表达式,并根据验证结果纠正了规约模式的语义,保证了它们的一致。C程序描述的是一系列状态转换的过程,可以引入规约模式描述程序性质。为了能更直观地表达程序性质以及准确地找到错误路径,本文对传统的状态进行扩展,使其不仅包含变量的取值,还包含位置信息,通过位置信息可以定位到具体的代码行。本文提出的C-PDL是描述C程序性质的半形式化语言,以规约模式为基础、以扩展后的状态为组成元素,并增加了描述断言的表达模式,能够描述顺序程序和并发程序的动态性质及程序的不变量。由于SPIN不能直接验证C-PDL描述的性质,本文研究了从C-PDL到SPIN输入语言的转换过程。在以上工作的基础上,本文以alternating-bit和producer-consumer为例,使用C-PDL描述程序性质,并根据性质省略掉无关代码,基于SPIN验证C程序是否满足这些性质。通过这个过程证明了C-PDL的表达能力以及从C-PDL到SPIN输入语言的转换过程的正确性,同时可以看出,此方法不仅能保证程序对于某些性质是正确的,还能方便地寻找错误路径。