《基于verds的c语言子集的模型检测方法》由会员分享，可在线阅读，更多相关《基于verds的c语言子集的模型检测方法（8页珍藏版）》请在金锄头文库上搜索。
1、2 0 1 3 年 第 2 2卷 第1 1期 h t t p ： w ww c - S a o r g c n 计 算 机 系 统 应 用 基于 V e r d s 的 C语言子集的模型检测方法 张 兰兰 ， ( 中国科学院软件研究所 计算机科学国家重点实验室，北京 1 0 0 1 9 0 ) ( 中国科学院大学，北京 1 0 0 1 9 0 ) 摘 要： 针对现今软件使用逻辑错误的问题越来越多的出现，提出了对最流行最普遍的编程语言 语言子集 的模型检测方法的研究采用基于 V e r d s 工具的模型， 运用 C语言子集转化成 V e r d s 模型的算法，结合V e r d s 工具 和
2、 MAG I C工具实现模型检测引入反例引导的抽象精化方法使模型检测解决状态爆炸的问题 关键词：模型检测；转化； V e r d s ； C E G A R ； MAG I C M o de l Che c k i ng M e t hod o n S ubs e t o f C La ng ua g e Ba s e d o n Ve r ds ZHANG La n La n ， 。 ( S t a t e Ke y L a b o r a t o r y o f C o mp u t e r S c i e n c e ， I n s t i t u t e o f S o ff wa r
3、 e ， C h i n e s e A c a d e m y o f S c i e n c e s ， B e ij i n g 1 0 0 1 9 0 ， C h i n a ) ( C h i n e s e A c a d e my o f S c i e n c e s ， B e ij i n g 1 0 0 1 9 0 ， C h i n a ) Ab s t r a c t ： I n p r o bl e m of s o ftwa r e l o g i c e r r o r s ， n o wa d a y s i t e me r g e s mo r e a n
4、 d mo r e Th e p a p e r p r e s e n t s t h e r e s e arc h f o r mo d e l c h e c k i n g me t h o d s o f C l a n g u a g e ，t h a t i t i s t he mo s t p o p u l a r a n d g e n e r a l p r o g r a mmi n g l a n g u a g e s Th e mo d e l c h e c k i n g b a s e d o n Ve r d s t oo l s ，u s i n g
5、 C l a n g u a g e s u bs e t i nt o Ve r ds mo d e l a l g o r i t h m，c o mbi n e d wi t h t h e Ve r d s t o o l s a n d MAG I C t o o l s I n t r o d u c i n g th e c o u n t e r e x a mp l e g u i d e d a b s t r a c t i o n r e fi n e me n t ( C E G A R ) me t h o d t o s o l v e t h e p r o b
6、 l e m o f s t a t e e x p l o s i o n K e y wo r ds ： mo d e l c h e c ki n g； t r a n f o r m； Ve r d s ； CEGAR； M AGI C 随着人类对于软件的使用越来越来广泛普遍， 软件 研究越来越深入， 对其精确度的要求也越来越高程序 工作者对简单程序的逻辑可以很好做出正确的判断，但 是广泛应 用在各个领域的程序每个 都是庞大 的架构，繁 多的结构分支， 这使得程序工作人员也无法梳理好这样 程序的逻辑程序的语法错误可以在相应的平台上完成 了检测，但是并没有完成程序逻辑检测一个软件的是 否
7、完成项 目的各项要求通 过测试人 员对其 进行专业 测 试 来验证 ， 达到各项测试要求的软件可 以投入使用完 成项 目测试的软件，我们不能说它是没有错误的，更多 的应用情况在软件日复一日的使用中出现， 那些被程序 工作者忽视和没有被软件测试员测试出的问题将会凸 显出来 为了提高软件这方面的精确度，科学家着手深 入对程序准确性、稳定性和 目的可达性的研究 今天， C语言是一个开放的语言，语法形式多样， 基金项 目： 国家科技重大专( 2 0 1 2 Z X0 1 0 3 9 - 0 0 4 ) 收稿时间： 2 0 1 3 - 0 4 1 7 ； 收到修改稿时f： 2 0 1 3 0 4 2 3
8、 不同的人可以编写出实现同一功能而源代码形式多样 的程序 使用 c 能编写高性能程序，包括系统程序和 应用程序 但是 C语 言的逻辑验证 问题还没有得到到 解决，这个 问题在 软件使 用 中有潜 在 的危 险国家航 天卫星的发射，是不容失误的，不容许出现问题的， 在卫星发射的过程中，有很多涉及软件，因为小小的 逻辑 问题 的失误 未被 发现所 引发 的卫星 发射 的失败 ， 是我们已经经历过的事情 为了减少这种的事情发生， 对软件， 对 C语言逻辑问题的验证被大家提出 基于 c 语言的模型检测是解决软件逻辑问题课题研究的一 部分， 对于软件逻辑问题解决很有意义 用模型的方法来描述和验证 C程序
9、可以发现软件 应用中潜在的错误 用模型描述和验证 C 程序是对其 进行模型检测设计与实现的基础 对 c程序软件的逻 辑验证的实现的正确性和完整性有重要的影响 S p e c i I s s u e 专论 -综 述1 9 计 算 机 系 统 应 用 h t t p ： l l w ww c - S a o r g c n 2 0 1 3年 第2 2卷 第 1 1期 l 相关概念 程序模型的状态空间正比于程序的变量数 目及变 量 的定义域，即使很 小 的程序 都可 能具有 巨大 的状态 空间，甚至是无穷的， “ 状态空间爆炸” 是在大规模软件 工业 设计 中推广 使用模 型检验 的一个主要 障碍
10、通 过 研 究人员 的努力，许 多方 法被提 出来，如 符号模 型检 验 、规约技术 、抽象技 术等等其 中抽 象技术近 年来 开始得到人们关注，逐步发展成为解决此种问题的一 种 重要手 段 1 9 9 4年， C l a r k e 、 G r u mb e r g和 L o n g初步探索 了应用 抽象技术的模型检验方法，通过构造程序的抽象模型来 验 证程序 的性质 然而，该方法 并没有完全解 决“ 状态 空间爆炸” 问题抽象模型中的状态称为抽象状态 相 应地， 抽象前的系统模型称为具体模型， 具体模型中的状 态称为具体状态要求抽象模型具有强保持性非常 困难 抽象通常会引入具体模型不存在的
11、附加的行为当抽象 模型不满足性质，在程序的流程图中存在这样一条导致 性质不满足的路径， 在程序中这样的一条路径是有语句 组成的， 我们可以称语句组成的这条路径为“ 反例” ，我 们可以肯定该反例存在于抽象模型， 但反例可能只是抽 象模型中引入的一个附加行为，不一定存在于具体模型， 这样的反例称为伪反例( s p u r i o u s c o u n t e r e x a m p l e ) 为解 决这样的问题， C l ar k e等 人在之前 的研究基础上继续深 入， 提 出了“ 反例 引导的抽象精化( c o u n t e r e x a m p l e g u i d e d a
12、b s t r a c t i o n r e f in e m e n t ,C E G A R ) ” J 框架 国外 出现 了很 多对于C语言的模型检测和程序验证的研究， 如S l a mt 1 ， Bl a s t I 4 ， Co mp c e r t t 1 ，V A R V E L 6 1 等 S l a m和 B l a s t 都采用 了反例引导的抽象精化框架 2 Ve r d s 验证工 具 W e r d s 7 - 9 程序验证模型是 由中科院软件所研究员 张文辉老师提出并维护 的 V e r d s 是验证层次化离散 系 统的模型验证工具系统的性质可用时序逻辑 C T
13、 L来 描述 验证方 法有 两类， 其一是基于 C T L 限界语义 的 限界模型检测方法， 其二是基于三元布尔图的符号模 型检测方法 本论文选择V e r d s 模型的原因，这是因为 V e r d s 有足够 的优 势，主要在 以下两个方面 ： f 1 )实现在 V E R DS中的三元布尔图的模型检测 方法和著名的 N u S MV 2 5 0符号模型检测工具进行过 比较 ，对 两 种类 型 的 随机 布尔 程序 的实验 用 例， V E R DS相比较于Nu S MV有明显的优势； 对于一些协 2 O 专论 综述 S p e c i a l I s s u e 议模型，V E R D
14、 S与 Nu S MV及其他相关工具比较互有 利 弊另外，限界模型检 测和 符号模 型检 测有一 定 的 互补 关系，主要优 势在于有 些性质在 一些系 统中 能够 在较 小的局 部范围 内得 到验证或者反证 使 用 V E R DS 进行验证有 可能结合两者 的长处 ( 2 )VE R D S使用的建模语言具有层次化的结构， 便于描述过程调用等，与一般程序语言有一些共同之 处， 适用 于程序 的描述并且验证 方法能够应用“ 假设 -保证” 框架，将较大的验证 问题分解为较小的验证问 题， 便于较大程序 的验证 V e r d s 模型一般有主模块和 P r o c e d u r e模块，
15、第二 个模块和 C语 言中函数块类 似 V e r d s 模型可 以进行并 行程序的验证，这种情况会用到 Mo d u l e模块， 这个模 块可以抽象一个线程性质的描述找S P E C模块， 用抽 象树逻辑 C T L表述 C T L是一种分支 时态逻 辑 C T L公式 的时态操 作 符由路径算子和时态算子组成 路径算子有 2种： A表 示“ 适用于所有的路径” ， E表示“ 存在至少 l条以上的 路径” 时态算子由X( n e X t t i m e ) 算子、F ( F u t u r e ) 算子、 G ( G l o b a 1 ) 算 子、U ( U n t i l ) 算子组
16、成 3 C到Ve r d s 模型转化步骤和预期结果 对于所 需要验 证的 C 程序，我们假 设在语法上正 确 的， 本文提 出针对 C 语言 的模型检测方法，首先在 V e r d s 工具中对c程序的验证，减少了建立模型的工作； 其次对于简单的 C语言程序，给出将 c语言子集转化 到 V e r d s模型的算法，这样实现了对 C 语言程序在 v e r d s 工具上的自动验证：然后针对大程序存在的状态 空间爆炸 问题， 提 出结合 C E G AR减少状态 的方法：最 后，对 C E G A R t m 】 实现过程中，重要的反例生成部分， 运用 MA G I C t ” 】 工具得 到符号迁移系统 L T S判断是 否 为伪反例， 对 C E G A R的完成 具有很 好的辅助作用 本文将可支持 的 C 语言程序转
