（计算机科学与技术专业论文）面向自动化模型检测的模型提取工具的设计与实现.pdf

硕l ：学位论文 摘要 随着计算机软件日益复杂，如何保证其正确性和可靠性成为十分紧迫的问题。 模型检测是一种验证有限状态系统的时序逻辑属性的形式化方法，已经在硬件电 路、驱动程序和安全协议等领域获得了巨大的成功。 应用模型检测技术到高级程序设计语言实现的系统的难点是提取抽象模型， 通常的办法是手工构造。然而这个方法存在一些不足，如成本过高，易引入建模 错误等，因此从源代码中直接提取验证模型存在强烈的实际需求。贝尔实验室开 发的s p i n 是优秀的模型检测工具，其建模语言是p r o m e l a ，而c 语言是应用 最广泛的程序设计语言之一，因此本文的主要研究内容定位于a n s i c 程序的模 型提取技术，从而达到使用s p i n 自动化模型检测c 程序的目的。 本文设计了一套对a n s i c 程序进行模型提取的方法，较好地处理了c 的大 部分语言特性，特别是几种复杂的结构，比如递归函数、枚举类型和指针等。并 开发了一个模型提取工具c 2 s p i n 。从功能上来说，c 2 s p i n 分为前端和后端。前 端是一个分析器，具有对c 源代码进行词法分析和语法分析的功能。后端则是一 个转换器，实现了从c 代码到p r o m e l a 代码的系统转换。而且，为了减小模型 的规模，加快模型提取的速度或者提高模型的执行效率，c 2 s p i n 中使用了一些简 单的抽象机制和优化技术。 c 2 s p i n 显著降低了建模的开销。结合c 2 s p i n ，s p i n 能够自动地检测使用c 语言编写的应用程序中的多种错误，比如死锁等性质。作者使用c 2 s p i n 进行了 一定数量的测试。在实验中，依靠c 2 s p i n 生成的模型，我们发现了s p i n 4 3 0 的 一个语义错误，以及h o l z m a n n 对两个经典互斥算法的实现中的活锁错误。因此 我们认为c 2 s p i n 在检测a n s i c 程序方面具有一定的实用价值。 关键词：形式化方法；模型检测；模型提取；a n s i c ；s p i n ；p r o m e l a i i a bs t r a c t w i t ht h ei n c r e a s i n gc o m p l e x i t yo fc o m p u t e rs o f t w a r e s ，i ti sn e c e s s a r ya n du r g e n tt o e n s u r et h ec o r r e c t n e s sa n dr e l i a b i l i t yo ft h e s es y s t e m s m o d e lc h e c k i n gi saf o r m a l m e t h o df o rv e r i f y i n gt h et e m p o r a ll o g i cp r o p e r t i e so ff i n i t e s t a t es y s t e m s ，a n dh a s g o t t e nh u g es u c c e s si na r e a ss u c ha sh a r d w a r ec i r c u i t s ，d e v i c ed r i v e r sa n ds e c u r i t y p r o t o c o l s t h ed i f f i c u l t yo fa p p l y i n gm o d e lc h e c k i n gt e c h n i q u et ot h es y s t e m si m p l e m e n t e di n h i g h 1 e v e lp r o g r a m m i n gl a n g u a g ei se x t r a c t i n ga n a b s t r a c tm o d e lw h i c hi su s u a l l y d o n eb yh a n d b u tt h i sa p p r o a c hh a ss o m ew e a k n e s s e s ，f o ri n s t a n c e ，t h ec o s t o f m o d e l i n gi sf a i r l yh i g ha n dt h ea r t i f i c i a l m o d e l sa r ee r r o r 。p r o n e ，t h e r e f o r et h e r ea r e s t r o n gp r a c t i c a lr e q u i r e m e n t sf o re x t r a c t i n gv e r i f i c a t i o nm o d e lf r o mt h es o u r c ec o d e d i r e c t l y s p i ni so n eo ft h em o s te x c e l l e n tm o d e lc h e c k e r sw h o s em o d e l i n gl a n g u a g e i sp r o m e l a ，w h i l et h ecp r o g r a m m i n gl a n g u a g ei s o n eo ft h em o s tp o p u l a r l a n g u a g e s ，s ot h em a i nc o n t e n to ft h et h e s i s f o c u s e so nt h et e c h n i q u eo fm o d e l e x t r a c t i o nf o rcp r o g r a m si no r d e rt oa c h i e v et h eg o a lo f m o d e lc h e c k i n gcp r o g r a m s w i t hs p i na u t o m a t i c a l l y i nt h i st h e s i s ，w ed e s i g nas e to fm e t h o d sf o re x t r a c t i n gv e r i f i c a t i o nm o d e l sf r o m t h ea n s i cp r o g r a m sw h i c hh a n d l em o s tl a n g u a g ef e a t u r e si ncp r o p e r l y , e s p e c i a l l ya f e wt o u g hs t r u c t u r e s ，s u c ha sr e c u r s i v ef u n c t i o n ，e n u m e r a t i o nt y p ea n dp o i n t e r a n d t h e nw ed e v e l o pam o d e le x t r a c t o rn a m e dc 2s p i n c 2 s p i ni sd i v i d e di n t ot w op a r t si n t e m so ff u n c t i o n a l i t y , t h ef r o n t e n da n dt h eb a c k - e n d t h ef r o n t e n d i sa na n a l y z e r t h a te x e c u t e sl e x i c a la n ds y n t a c t i ca n a l y s i so v e rt h ec s o u r c ec o d e t h eb a c k - e n di sa t r a n s l a t o rt h a tp e r f o r m ss y s t e m a t i ct r a n s l a t i o nf r o mcp r o g r a m si n t o p r o m e l a d e s c r i p t i o n s m o r e o v e r , ac o u p l e o fa b s t r a c t i o na n do p t i m i z a t i o nt e c h n i q u e sw e r e d e p l o y e di nc 2 s p i ns oa st o r e d u c et h es i z eo ft h em o d e l ，s p e e du pt h ep r o c e s so f m o d e le x t r a c t i o no ri m p r o v et h ee f f i c i e n c yo ft h ee x e c u t i o n c 2 s p i nr e d u c e st h ee x p e n s eo fm o d e l i n gs i g n i f i c a n t l y s p i nc a nd e t e c t v a r i o u s e r r o r si na p p l i c a t i o n si m p l e m e n t e di ncm e c h a n i c a l l yc o m b i n i n g w i t hc 2 s p i n ，s u c ha s d e a d l o c k w er a naq u a n t i t yo ft e s t i n gu s i n gc 2 s p i n i nt h ee x p e r i m e n t s ，d e p e n d i n g u p o nt h em o d e l sg e n e r a t e db yc 2 s p i n ，w ef o u n das e m a n t i cb u g i ns p i n 4 3 0a n d s i m i l a rl i v e l o c k si nt h ei m p l e m e n t a t i o no ft w oc l a s s i cm u t u a le x c l u s i o na l g o r i t h m s w r i t t e nb vh o l z m a n n t h u sw ec o n c l u d et h a tc 2 s p i ni s u s e f u li nt e s t i n ga n s i - c p r o g r a m s 1 1 i 硕l j 学位论文 k e yw o r d s ：f o r m a lm e t h o d s ；m o d e lc h e c k i n g ；m o d e le x t r a c t i o n ；a n s i c ；s p i n ； p r o m e l a i v 面向自动化模型柃测的模型提取丁只的设汁j 实现 暑- - ! 鼍毫詈皇暑詈皇皇曼鼍鼍! 曼! 鼍詈鼍 一一一一i i 鼍! 皇蔓! 鼍皇曼曼鼍鼍皇暑詈皇鼍皇鼍 插图索引 2 1x s p i n 的验证过程1 2 2 2 深度优先搜索算法1 5 2 3 有限状态自动机t 1 和t 2 1 6 2 4t l 和t 2 的扩展异步积1 6 2 5 应用偏序归约技术的效果1 8 3 1c 2 s p i n 的基本结构2 4 3 2c 2 s p i n 的类图切片2 5 3 3 分析器c 9 9 p a r s e r 的基本流程2 6 3 4 分析器的记号表片段2 6 3 5x + y 的a s t 2 7 3 6 根结点n o d e 2 7 3 7 函数定义结点2 8 3 8 基本变量符号表2 8 3 9 结构体符号表2 8 3 1 0 函数符号表2 9 3 1 1c 2 s p i n 的命令行界面3 0 3 1 2 计算a + b 的c 代码3 0 3 1 3c 2 s p i n 提取模型的过程3 1 3 1 4 计算a + b 的p r o m e l a 代码3 l 3 1 5c 2 s p i n 发现语法错误3 2 3 1 6s p i n 的模拟执行3 2 3 1 7s p i n 的验证执行3 2 4 1p r o m e l a 中的t y p e d e f 3 5 4 2p r o m e l a 中的进程3 5 4 3p r o m e l a 中的选择语句3 6 4 4p r o m e l a 中的循环语句3 6 4 5p r o m e l a 中的跳转语句3 7 4 6p r o m e l a 中的锁机制一3 7 4 7 变量作用域管理机制3 9 4 8 不致的t y p e d e f 4 0 4 9 枚举类型模型4 0 4 10 指针模型4 2 v i i 图图图图图图图图图图图图图图图图图图图图图图图图图图图图图图图图 硕j 学使论文 4 1 l 基本的i f 语句模型4 2 4 1 2 基本的w h i l e 语句模型4 3 4 13c 2 s p i n 提取的循环模型4 4 4 1 4 函数a 调用b 的关系图4 5 4 1 5 函数a ，b ，c 互相调用关系图4 5 4 1 6 判断间接递归函数的算法4 6 4 17 函数的内联模型4 7 4 1 8 函数的异步通信模型一4 7 4 1 9 函数的同步通信模型4 7 4 2 0 递归函数模型4 8 4 21 模型优化4 9 5 1d e k k e r 算法伪代码5 1 5 2p e t e r s o n 算法伪代码5 2 5 3d e k k e r 算法的活锁错误示意图5 3 5 4d e k k e r 算法的活锁错误原因5 3 5 5p e t e r s o n 算法的活锁错误示意图5 4 5 6p e t e r s o n 算法的活锁错误原因5 4 5 7s p i n 4 3 0 的一个b u g 5 5 v i i i 图图图图图图图图图图图图图图图图图图 面向自动化模犁榆测的模型提取下具的设计与实现 sn 一n n i 曼i 曼! 罡鼍鼍曼曼詈! 曼! ! 詈曼曼鼍皇! 苎曼詈 附表索引 表2 1l t l 公式( 事件发生) 2 0 表2 2l t l 公式( 事件关联) 一2 0 表2 3l t l 公式( 其它情况) 一2 0 表4 1p r o m e l a 的基本数据类型3 4 表4 2c 2 s p i n 的基本类型映射表3 8 表5 1d e k k e r 算法的死锁检测结果5 1 表5 2p e t e r s o n 算法的死锁检测结果5 2 表5 3d e k k e r 算法的活锁检测结果5 3 表5 4p e t e r s o n 算法的活锁检测结果5 4 湖南大学 学位论文原创性声明 本人郑重声明：所呈交的论文是本人在导师的指导下独立进行研究所取得 的研究成果。除了文中特别加以标注引用的内容外，本论文不包含任何其他个 人或集体已经发表或撰写的成果作品。对本文的研究做出重要贡献的个人和集 体，均已在文中以明确方式标明。本人完全意识到本声明的法律后果由本人承 担。 作者签名：上火i 衫 l嘿砂户，月f 日 学位论文版权使用授权书 本学位论文作者完全了解学校有关保留、使用学位论文的规定，同意学校 保留并向国家有关部门或机构送交论文的复印件和电子版，允许论文被查阅和 借阅。本人授权湖南大学可以将本学位论文的全部或部分内容编入有关数据库 进行检索，可以采用影印、缩印或扫描等复制手段保存和汇编本学位论文。 本学位论文属于 1 、保密口，在年解密后适用本授权书。 2 、不保密团。 ( 请在以上相应方框内打“”) 作者虢王大伸弋日期 刷帷轹几 辞嬲 硕i j 学位论文 第1 章绪论 1 1 课题背景及意义 1 1 1 研究背景 随着应用领域的扩展和深入，计算机软硬件系统日益复杂，如何保证其正确 性和可靠性等成为十分重要的问题。近年来，由于软件错误而导致严重后果的报 道屡见不鲜。1 9 9 4 年，奔腾处理器被发现在执行某个特定的浮点运算时出现错误， 这种错误2 7 0 0 0 年才可能出现一次。i n t e l 为此花费了4 7 5 亿美元回收有缺陷的产 品。1 9 9 6 年6 月4 日，耗资8 0 亿美元的欧洲航天局阿丽亚娜( a r i a n e ) 5 0 1 火箭 在升空3 7 秒后爆炸，原因是控制系统的设计错误。这两起灾难事件的共同教训 就是，软硬件系统的可靠性已经成为关系到国计民生的重大因素之一。 幸运的是，系统可靠性问题已经引起了高度重视。美国国防高等研究规划局 ( d a r p a ) 提出了“f o r m a lm e t h o d s ”计划，重点支持对高可信软件系统的原理 和相应支撑工具的研究；美国国家自然科学基金会( n s f ) 在2 0 0 0 年启动了规模 宏大的研究计划“i n f o r m a t i o nt e c h n o l o g yr e s e a r c h ”，强调利用形式化方法来保证 系统行为的可靠性【l 】。中国在这一研究领域的投入也日益加强。“十一五”期间， 依据国家中长期科学和技术发展规划纲要( 2 0 0 6 2 0 2 0 年) 、国家“十一五 科学技术发展规划和国家高技术研究发展计划( 8 6 3 计划) “十一五”发展纲 要，8 6 3 计划信息技术领域围绕国家重大工程、重大行业应用和经济发展的迫切 需求，设立了“新一代高可信网络 重大项目。 在软件开发生命周期中，作为衡量质量的必要手段，测试始终是重要的一环。 传统的质量保证方法包括模拟和测试，分别在系统模型或者实际系统上进行。一 般的方法是给系统提供一组输入数据，观察相应的输出数据，然后判断这些输出 结果是否符合预期。然而这种基于有限测试用例集驱动的测试技术有着不可避免 的局限性。首先，它虽然能够测试软件的部分属性，但是由于缺乏严格的属性描 述方法，因此难以适用于复杂属性的测试；其次，传统测试方法严重依赖于测试 人员的领域经验和测试用例的覆盖范围，对于并发程序中的由于线程、进程间或 者与环境交互造成的错误而言，它们难以重现。因此，单纯依靠有限的测试用例 是远远不够的。 当今工业上控制软件质量所采用的主要方法，比如代码检查，同行评审，内 部测试等，能够较好地适用于单机的、串行的应用程序，因为这类程序的行为是 确定的。然而它们并不适用于行为不确定的分布式软件系统。 面向自动化模掣榆测的模掣提取t 只的设计与实现 2 0 世纪6 0 年代，f l o y d 和h o a r e 等人开创了形式化验证( f o r m a lv e r i f i c a t i o n ) 的新领域【2 3 】，主要思想是对原系统的抽象模型进行严格的形式化证明。具体过程 包含两点：一是描述系统行为，称作建模( m o d e l i n g ) 。模型的表示方式包括有限 状态自动机、p e t r i 网、进程代数等；二是刻画系统属性，称作规格( s p e c i f i c a t i o n ) ， 诸如安全性、活性、公平性等。属性的表示方式包括命题逻辑、时序逻辑、兀 演算、u 演算等。 作为一种主要的形式化验证方法，模型检测( m o d e lc h e c k i n g ) 由c l a r k e 和 e m e r s o n 于1 9 8 1 年提出【4 】。其基本思想是采用有限状态自动机( f i n i t es t a t e a u t o m a t o n ，下文简称f s a ) 描述系统行为( s ) ，常用的是一类扩展的f s a b u c h i 自动机或者一种带标签的状态迁移系统一k r i p k e 结构，并采用时序逻辑描述 系统属性( p ) ，比如线性时序逻辑l t l ( l i n e a rt e m p o r a ll o g i c ) 5 】或计算树逻辑 c t l ( c o m p u t a t i o nt r e el o g i c ) 6 1 ，通过穷举搜索系统空间的所有状态和迁移来验证 该系统是否满足某属性，即s 卜p ，如果不满足，将给出一个反例。模型检测技 术尤其擅长处理并发系统和实时系统，目前已经应用于状态数目达1 0 12 0 的复杂 系统，在硬件、驱动程序及安全认证协议等领域都获得了巨大的成功。 模型检测的一个严重缺陷是“状态爆炸”问题，即随着待测系统的规模增大， 算法所需的时间和空间开销往往呈指数增长。目前解决此问题的策略主要有三类： 一是结合模型检测与定理证明( t h e o r e mp r o v i n g ) 的优势。模型检验具有自动性， 但有状态爆炸问题。相对而言，定理证明的处理能力受状态数目的影响不大，但 需要人工引导。比如斯坦福大学的s t e p ( s t a n f o r dt e m p o r a lp r o v e r ) 1 7 】就是用模型检 测器处理子系统的验证问题，然后用定理证明器将结果汇总并处理，从而完成整 个系统的验证。二是符号模型检测，该方法由b u r c h 和c l a r k e 等人在1 9 9 0 年提 出【8 】，用有序二叉判定图o b d d s ( o r d e r e db i n a r yd e c i s i o nd i a g r a m s ) 9 】描述状态迁 移图，用布尔逻辑公式描述系统属性，不仅大大压缩了状态表示的空间，而且可 以充分利用已有的大量有效的图算法来提高验证的速度，因而取得了重大的突破， 在当年就已经用于状态数目超过1 0 2 0 的硬件电路的验证【l 们。但符号模型检测的最 大瓶颈仍然是状态图规模的指数级增长会导致内存不足。三是定界模型检测技术 ( b o u n d e dm o d e lc h e c k i n g ) ，这是继符号模型检测之后的又一重要进展。这个方 法由b i e r e 等人在19 9 9 年提出【】，依赖于布尔可满足性问题( b o o l e a ns a t i s f i a b i l i t y p r o b l e m ，简称s a t ) 的求解器，主要思想是：在一个限定的步数k 内，确定系统是 否满足性质。若不能确定，则增加k 值，重新进行验证。在每一个检验周期内， 定界模型检测问题被转化成s a t 问题求解。虽然s a t 问题是n p 完全 ( n p c o m p l e t e ) 问题，在实际应用中却存在不少高效的近似算法。i n t e l 的研究报 告显示：在对p e n t i u m 4 芯片中抽取的典型设计进行的验证中，定界模型检测在 验证能力和效率上都比符号模型检测有优势。 2 硕l ：学位论文 应对“状态爆炸 问题曾经是一个研究热点，其它重要方法有：o n t h e f l y 1 2 】， 谓词抽象【1 3 , 1 4 】，偏序归约1 5 】等。 迄今为止，学术界和工业界已经开发了多种模型检测工具，并得到了广泛的 应用，如s p i n ( s i m p l ep r o m e l ai n t e r p r e t e r ) 16 1 ，s m v ( s y m b o l i cm o d e lc h e c k i n g ) 1 7 1 ， j p f ( j a v ap a t h f i n d e r ) 1 8 , 1 9 ，b a n d e r a 2 们，b l a s t ( b e r k e l e yl a z ya b s t r a c t i o ns o f t w a r e v e r i f i c a t i o nt 0 0 1 ) 2 1 1 ，s l a m t 2 2 】等。 s p i n 是由贝尔实验室的h o l z m a n n 开发的著名的验证并发系统逻辑属性的工 具，以p r o m e l a ( p r o c e s sm e t al a n g u a g e ) 作为建模语言。对于给定的p r o m e l a 模型，s p i n 可以对其进行仿真，也可以生成一个c 语言描述的验证程序，然后 对系统的属性进行检验。 p r o m e l a 的语法十分简单，支持基本的数据类型，比如i n t ，b o o l 等，以及 一些特有的类型，比如c h a n ( 管道) ，但是没有c 语言中函数和指针等高级概念。 因为它能够方便地创建同步或异步执行的并发进程，所以适合描述并发程序。一 个p r o m e l a 模型通常由进程、消息管道、变量和全局对象组成。 1 1 2 研究意义 由于模型检测基于穷举搜索算法的特性以及具备丰富的支持工具，因此许多 著名的i t 公司，如i n t e l 、m i c r o s o f t 、i b m 都已经在其产品开发过程中广泛使用 模型检测技术来提高软硬件系统的质量。而国内的相关研究由于起步较晚，基础 比较薄弱，因此许多工作尚未开展。 为软件系统建造可靠的验证系统一直是一个艰巨的目标。众所周知，即使一 些很简单的属性，比如程序的死锁或者可终止性，都是不可判定的【2 3 1 。因此，一 般的自动验证系统都是着眼于小心翼翼地定义程序设计语言的真子集，比如可以 通过在通用程序设计语言上施加某些语法限制来获得这类真子集。然而这些限制 的技巧一般只有那些富有经验的程序员才具备。如果能够设计一套方法，利用它 可以自动地获得一个抽象系统，即从通用编程语言编写的源程序中自动生成可验 证的模型，是十分有价值的。抽象的含义是指，被建模的原型系统中的可能的执 行路径能够在抽象系统中被重现，或者说，能够在诸如s p i n 的模型检测工具中 进行分析【2 4 】。 应用模型检测技术的前提是首先获得待验证系统的模型，通常有两种办法： 手工编写或者自动生成。长期以来，模型检测的用户通常针对应用程序的关键模 块实行手工建模 2 5 , 2 6 】。然而这个方法具有几个局限性：第一，手工建模的方法不 可靠。如果人们工作中出现的错误比率是问题规模的函数，那么这不仅适用于构 建原始系统程序中，也同样适用于构建模型的过程中。这意味着，当面对更大规 模的应用程序时，手工建模变得不可靠。第二，要求模型编写者对原型系统具有 3 面向自动化模型拎测的樱犁抛取t 只的改汁j 实现 深刻的认识以及使用模型检测技术的经验，工作量大，难以推广；第三，时效性 和相关性差。团队开发的软件可能经常变化，甚至每天都在变。手工建造应用程 序的任何一个版本的抽象模型都可能花费几个星期甚至几个月。然而有可能等手 工做出模型后，原来的系统已经升级了，这就会造成模型与系统的不一致性，从 而导致模型的失效，而上一次的验证结果很可能变得不相关。由此可见，手工建 模阻碍了模型检测的进一步推广，已经变得不合时宜，如果我们希望利用模型检 测这一强大的测试手段，就迫切需要自动化的模型生成工具。 c 语言【2 7 】是主流的程序设计语言之一， 由贝尔实验室的d e n n i sr i t c h i e 于 1 9 7 2 年开发，初衷是为了重写u n i x 操作系统。由于c 语言用法十分灵活，且提 供了直接访问内存和分配内存的方式，被称为“高级语言中的低级语言 ，因此广 泛地用于编写系统软件和应用软件。但另一方面，如a n d r e wk o e n i g 所言，“c 语 言就像一把刻刀：简易，锋利，在有经验者的手中极其有用。然而，像其它锋利 的工具一样，c 会伤害不能控制它的人 【2 趴。实践表明，比起其他高级语言，c 语言实现的系统更有可能含有各种隐晦的潜在错误，而且往往是致命的，比如局 部变量未初始化，野指针，内存泄漏等。考虑到多处理器和分布式计算的日益普 及，仅仅依靠传统的测试手段来寻找软件错误将更加吃力，而错误的危害性却会 更加严重。 国外已经有一些工作着眼于把模型检测技术应用于检测c 应用程序，但是具 体到从c 源代码中自动生成p r o m e l a 模型方面，还很少见。因此本文的研究课 题就是c 程序的模型提取技术，并开发一款工具自动地完成这项工作，从而做到 自动化模型检测c 程序。比起已有的工作，本文独立设计了一套模型提取的方法， 更好地解决了枚举类型和递归函数等难题的处理。利用c 2 s p i n 生成的模型，模 型检测工具s p i n 可以验证模型是否满足某个属性，如果满足，则给出肯定回答， 否则产生一个反例，帮助测试人员跟踪并定位程序的错误，从而节省人工和时间 成本，提高软件测试效率。 1 2 国内外研究现状 1 2 1 国外的相关工作 从源代码中自动提取验证模型是一项复杂而繁琐的工作。截至目前，该领域 已经取得了重要的研究成果，但数量上相对有限。 1 9 8 9 年，h o l z m a n n 曾经从c c i t t 的规格语言s d l 的真子集中提取模型 2 9 1 。 虽然在验证技术上取得了成功，但一方面，由于该方法对于输入语言s d l 作了过 于严格的限制，且s d l 是一种专用编程语言，不够普及，所以在应用上，这次尝 试不算成功。这类工作基本上是对源程序作一个文本层次上的转换，而不采用抽 4 硕j j 学位论文 象技术。作为代价，这些方法都需要对输入语言加以限制，或者需要在语言中新 增一些元素，或者只能处理语言的真子集，代表性的语言有：a d a 30 1 ，j a v a 3 1 1 。 已有的研究成果主要集中在j a v a 语言【3 2 】。其中有两个颇具影响的项目，都系 统地采用了抽象技术，分别是：k a n s a s 州立大学的b a n d e r a ，和n a s a 的j a v a p a t h f i n d e r2 。b a n d e r a 实际上是一个开放的工具平台，集成了多个已有的成熟验 证系统。其模型提取过程基于程序切片技术【33 1 ，将j a v a 程序转换成中间代码，并 提供了灵活的后端接口以适应多种模型检测器，包括s p i n 和s m v 。j a v a p a t h f i n d e r 的第一代，即j p f l 能够处理j a v a 的大多数语言特性，比如类继承、线 程和异常等，但不能解决浮点数、方法重载、方法重写和递归函数等。而j p f 2 不但包含了更多的j a v a 特性，而且实现了一个m c j v m 来解决内存分配和垃圾 回收等难题，取得了良好的效果。b a n d e r a 和j p f 2 的目标都是融合自动验证谓词 抽象技术，不同的是，分别把模型提取过程连接到定理证明器和p r e s s b u r g e r 算术 的判定过程【3 4 1 。另外，文献【3 5 】也实现了j a v a 到p r o m e l a 的转换，但是没有处 理异常和多态等。 在c + + 【3 6 】方面，文献【3 7 】定义了一种增加了同步机制的c + + 语言一s c + + ，引 入了活动对象等概念，有效降低了从c + + 向p r o m e l a 转换的难度。文献【3 8 】实现 了从s c + + 的真子集中提取p r o m e l a 模型，不足之处在于s c + + 并不流行。 1 9 9 8 年，为了对一个大型的商用电信应用程序进行验证，h o l z m a n n 等人设 计了一个从c 语言源程序提取模型的原型系统【3 9 1 。这个电信应用软件是采用带有 特殊标记的a n s i c 语言编写的，到目前为止，这是在c 源代码级别上应用模型 检测方法的最大规模的案例。在超过1 8 个月的运行周期中，该方法被证明是有效 的。只需要少量的人工参与，就可以寻找到软件的缺陷。2 0 0 0 年2 月开始， h o l z m a n n 等人改进了原来的做法中需要对输入语言进行限制的不足之处，进一步 完善了这个工具，并命名为m o d e x 4 0 1 ，在此期间以模型提取为主题相继发表了一 些论文【41 , 4 2 】。 值得一提的是还有一类工作的出发点是结合传统测试和程序验证的优势，比 如贝尔实验室的v e r i s o f l 4 ”，可以直接测试c 源代码，而e r a s e r 4 4 】贝0 能够检测j a v a 代码。这两者都通过监控代码的实际运行来做测试，其缺点在于仅能验证基本的 安全属性，而无法扩展到通用的时序逻辑属性。 1 2 2 国内的相关工作 目前国内对于模型检测的研究可以粗略划分为两个方向：一是案例分析，比 如对协议正确性、安全性、一致性等性质的验证以及硬件系统方面的验证，这种 类型的文献中占据了9 0 左右的比例；二是基础理论研究，比如提出新的检测方 法或改进已有的算法，约占5 的比例。而从源代码中提取验证模型方面，据作 面向自动化模型柃测的模型提取t 只的设计0 实现 者所知，还没有相关文献可供参考。 张玉清等提出了使用模型检测工具s m v 分析密码协议的方法【4 5 1 ，并对 n e e d h a m s c h r o e d e r ( n s ) 公钥协议进行了验证。结果表明，入侵者可以对n s 公钥 协议进行有效攻击，而这个攻击是b a n 逻辑分析没有发现的，并给出了一种经 过改进的协议。 文献【4 6 】使用s p i n 对n s p k 协议进行检测，通过建立该协议的p r o m e l a 模 型，采用l t l 描述模型性质，通过验证进而生成入侵者的攻击序列。 文献【4 7 1 研究的是互联网密钥交换协议i k e v 2 ，利用s p i n 对其进行建模和分 析。针对现有的建模方法构造的模型可读性差、验证效率较低等缺点，提出了一 种新的建模方法，便于对复杂的安全协议进行建模。最后利用s p i n 对i k e v 2 协 议的模型进行了验证，发现i k e v 2 协议不能抵御主动攻击，并给出了两个攻击序 列图。针对i k e v 2 协议不能保护发起者身份的缺陷，提出了一种改进意见。 另外，文献【4 8 5 0 】的主题都是对协议进行分析与验证。 蒋屹新等研究了基于p e t r i 网的模型检测【5 ，描述了线性时态逻辑、b u c h i 自 动机、p e t r i 网和同步积之间的内在联系，并探讨了基于线性时态逻辑的p e t r i 网 模型检测方法。并通过对一个并发系统形式化的模型检测分析，验证了相应的结 论。 文献 5 2 深入研究了l t l 公式转换为b u c h i 自动机的一类算法【5 3 】，重新定义 了基于迁移的扩展b t l c h i 自动机的求交运算，减少了需要复制的状态个数，使转 换后的自动机具有更少的状态。 针对现有的模型检测工具，比如s m v ，只能对c t l * 5 4 】的真子集( 如l t l ， c t l ) 进行检测的不足，苏开乐等提出了一个关于时态逻辑c t l * 的符号化模型检 测算法【55 1 ，并实现了一个模型检测工具。 文献 5 6 研究了基于标号迁移系统的c 程序模型检测，提出一种软件模型检 测并行化的方法。该方法利用模型检测工具m a g i c 的模块化特性对c 程序进行 组件分解，将各组件均匀地分发到若干计算节点，由各节点调用m a g i c 完成验 证。由于节点间只有少量的通信与同步，该方法能达到较好的并行加速比，具有 良好的可扩展性。 1 3 本文的研究内容 为了把模型检测技术更加方便地应用于检测a n s i c 程序，本文设计了一套 对c 程序进行模型提取的方法，并开发了模型提取工具c 2 s p i n ，从而实现了对c 程序的自动化模型检测。c 2 s p i n 能够自动分析c 程序并且从c 源代码中提取 p r o m e l a 模型，然后使用模型检测工具s p i n 验证模型的性质，比如死锁等。 实验结果表明，使用c 2 s p i n 辅助检测c 程序是可行的。 6 硕 ：学位论文 本文的具体研究内容如下： ( 1 ) 模型检测工具s p i n 和p r o m e l a 语言 s p i n 是最重要的模型检测工具之一。首先需要了解s p i n 的基本原理，学会 在发现错误后追踪定位反例。为了实验需要，学习使用了s p i n 的两款图形界面 软件：j s p i n 5 7 】和x s p i n 5 8 1 。 p r o m e l a 是s p i n 的建模语言。在掌握p r o m e l a 的语法和语义的基础上， 考查源语言c 和目标语言p r o m e l a 的差异性是本文的一个研究重点。一方面， 在生成模型的过程中要充分利用p r o m e l a 的特性；另一方面，对于那些 p r o m e l a 不支持的c 语言特性，则要考虑如何弥合这种差异，这是一个难点。 s p i n 采用线性时序逻辑l t l 描述系统属性。l t l 具有丰富的表达能力，能 够表示死锁、安全性、活性等最有用的程序性质，因此需要掌握用l t l 描述常用 属性的基本方法。 ( 2 ) 设计模型提取方法 为了达到使用s p i n 自动化模型检测a n s i c 程序的目的，本文设计了一套面 向a n s i c 语言的模型提取方法。对各种主要的c 语言结构都实现了有效的转换， 主要特色在于较好地解决了一些棘手问题，比如标识符冲突，指针，枚举类型和 递归函数等。 ( 3 ) 实现模型提取工具c 2 s p i n 本文依据的语言标准是i s o i e c9 8 9 9 ：1 9 9 9 5 9 1 ，简称c 9 9 。作者手工编写了 c 9 9 的语法文件，涵盖了c 9 9 的绝大部分特性。然后利用j a v a c c ( j a v ac o m p i l e r c o m p i l e r ) 6 0 】和j t b ( j a v at r e eb u i l d e r ) 6 1 1 来编写a n s i c 的词法和语法分析器。如 果分析器发现程序有语法错误，则中断分析过程并给出清晰的错误提示。另外， 还涉及构造各种用途的符号表和映射表，各种结构类型的存储数据结构等。 基于一组模型提取方法，我们实现了转换器，它和分析器共同构成模型提取 工具c 2 s p i n ，做到了从a n s i c 源代码中直接提取p r o m e l a 模型。为了得到更 加有效的模型，在转换器中适当加入了部分语义分析、简单抽象和模型优化技术。 ( 4 ) 实验及结果分析 为了验证c 2 s p i n 的价值，作者进行了一定数量的测试。在实验中，借助c 2 s p i n 自动生成的模型，我们发现了两个新错误，分别是s p i n 4 3 0 的一个语义错误以 及h o l z m a n n 在文献 6 2 1 中对两个经典互斥算法一d e k k e r 算法和p e t e r s o n 算法的 实现中的活锁错误。对于这两个错误，本文都给出了解释以及相应的修正方案。 1 4