（计算机应用技术专业论文）基于模型检查的程序验证和测试用例生成.pdf

“每大学硕t 学位论文 摘要 随着计算机软硬件系统规模的日益复杂化，如何保证计算机系统的正确性 和可靠性，逐渐成为当前理论界和产业界共同关心的重要问题。而当前限制计 算机实际广泛应用的因素已经不再是机器硬件“缓慢”的速度和“低下”的计 算能力，而更多的是我们在设计和实现复杂系统时，设计与验证的能力还比较 有限，无法保证所设计系统的正确性和可靠性。而基于状态搜索的模型检查技 术为系统验证提供了有效的保证手段。 模型检查是一种针对有限状态并发系统的形式化验证技术，其基本思想是 构造系统的有限状态模型，在系统模型的状态空间内运算，检查建立的系统模 型是否满足期望的性质。本文考察模型检查技术的基本原理，研究模型检查在 软件验证上的应用，并开发实现了一个针对c 语言编写的程序进行验证的系统 原型。并且按照存在量词公式的证据是全称量词公式的反例的特性，用模型检 查的反例生成机制对测试用例生成技术进行研究，然后把模型检查的算法引入 到软件测试领域，寻找满足规格说明的路径，生成测试用例，据此对系统进行 测试。 本文的主要工作主要有： 1 研究模型检查技术，考察时序逻辑公式的特点，改进并实现模型检查的 符号算法，开发一个针对c t l 公式的模型检查器。 2 研究模型检查在c 语言中的应用，提出把程序源代码作为模型检查的输 入数据，直接对程序代码进行模型检查。 3 开发一个软件验证系统原型，实现从代码直接转换成状态迁移系统。 4 考察时序逻辑算子，根据存在量词公式和全称量词公式的转换关系，生 成反例路径，生成测试用例，用于软件测试。 关键词：模型检查，软件验证，反例，测试用例生成 v j ：海大学硕i j 学位论文 a b s t r a c t w i t hc o m p u t e rs y s t e mb e c o m i n gm o c o m p l e xg r a d u a l l y , i ti st h em o s ti m p o r t a n tc o m m o n r e q u i r e m e n tt h a th o wt og u a r a n t e et h ec o i t e c t n e s sa n dr e l i a b i l i t yo fc o m p u t e rs y s t e mi nt h e o r y r e s e a r c ha n di n d u s t r yc u r r e n t l y h o w e v e r , t h ef a c t o rr e s t r i c t sw i d ea p p l i c a t i o no f c o m p u t e ri sn o t t h el o ws p e e da n dw e a kc o m p u t ec a p a b i l i t yo fm a c h i n eh a r d w a r e ，b u to u rn a r r o w 曲i l i t yo f d e s i g na n dv e r i f i c a t i o nw h i l ed e s i g n i n ga n di m p l e m e n t i n gc o m p l e xs y s t e m s o ，t h ec o r r e c u l e s s a n dr e l i a b i l i t yc o u l dn o tb ee n s u r e d t h e n , t h em o d e lc h e c k i n gb a s e do ns e a r c h i n gs t a t e s p r o v i d e se f f e c l i v em e t h o df o rs y s t e mv a l i d a t i o n t h em o d e lc h e c k i n gi sak i n do ff o r m a lt e c h n o l o g yt ov a l i d a t ef i n i t e - s t a t eg o n c m t g l l t s y s t e m ，w i t ht h ep r i m et h o u g h to ft h a tt oc o n s t r u c tf i n i t e s t a t em o d e lo fs y s t e ma n dc h e c k w h e t h e rt h em o d e ls a t i s f i e ss o m ep r o p e r t i e se x p e c t e dt h o u g hc o m p u t a t i o ni ns t a t es p a c e i t c h e c k sw h e t h e rs y s t e mm o d e lb u i l tb e f o r es a t i s f i e ss o m e p r o p e r t i e se x p e c t e d , b a s e d o n c o m p u t a t i o ni ns t a t es p a c eo fs y s t e mm o d e lo ff i n i t e s t a t es y s t e m c o n s i d e r i n gt h ep r i n c i p l eo f m o d e lc h e c k i n g , ap r o t o t y p es y s t e mw i t ha i ma tv a l i d a t i n gp r o g r a mc o d ew r i t t e nb ycp r o g r a m l a n g u a g ei sb u i l t i n t h i sp a p e r + t h er e l a t i o n s h i pb e t w e e nc o u n t e r e x a m p l ea n dt e s tc a s ei s r e s e a r c h e da c o o r d i n gt ot h ef a c tt h a tt h ew i t n e s s e so f e x i s t e n t i a lp a t hq u a n t i f i e rf o r m u l a sa r et h e c o u n t e r e x a m p l e so fu n i v e r s a lp a t hq u a n t i f i e rf o r m u l a s a n dt h ea l g o r i t h mo fm o d e lc h e c k i n gi s i n t r o d u c e di nt h ef i e l do fs o f t w a r et e s ti no r d e rt of i n do u tt h ev e r i f i e dp a t ha n dp r o d u c et e s t c a s e su s e dt ot e s ts y s t e m t h em a i nc o n t r i b u t i o n so f t h i sp a p e ra r es h o w na sb e l o w ： 1r e s e a r c h i n gm o d e lc h e c k i n ga n dt e m p o r a ll o g i cf o r m u l a , t h ea l g o r i t h mo f l a b e l i n gm o d e l c h e c k i n gi sm o d i f i e da n da c h e c k e rf o rc t li sd e v e l o p e d 2c o n s i d e r i n ga p p l i c a t i o no fm o d e lc h e c k i n gi ns o f t w a r ed e v e l o p m e n tw i t hcp r o g r a m l a n g u a g e ，an e wm e t h o do fv e r i 矗i n gp r o g r a mc o d ed i r e c t l yi si n t r o d u c e dw i t hc o d es e g m e n t 觞 i n p u t 3a p r o t o t y p ev a l i d a t i o ns y s t e mi sd e v e l o p e dt oc a r r yo u tt h es w i t c hf r o mp r o g r a mc o d et o s t a t es p a c e 4c o n s i d e r i n gt e m p o r a ll o g i co p e r a t o r s ，t h et e c h n o l o g yo fm o d e lc h e c k i n gi se x p a n d e dt o t h ef i e l do fs o f t w a r et e s t ，a c c o r d i n go ft h er e l a t i o nb e t w e e nu n i v e r s a la n de x i s t e n t i a lp a t h q u a n t i f i e rf o r m u l u s k e y w o r d s ：m o d e lc h e c k i n g ，s o f t w a r ev a l i d a t i o n ，o u a t e r e x a m p l e ，g e n e r a t i o no ft e s t c a s e v l 原创性声明 本人声明：所呈交的论文是本人在导师指导下进行的研究工作。 除了文中特别加以标注和致谢的地方外，论文中不包含其他人已发 表或撰写过的研究成果。参与同一工作的其他同志对本研究所做的 任何贡献均已在论文中作了明确的说明并表示了谢意。 签名：奎垒盈日期：兰堕：y 本论文使用授权说明 本人完全了解上海大学有关保留、使用学位论文的规定，即： 学校有权保留论文及送交论文复印件，允许论文被查阅和借阅；学 校可以公布论文的全部或部分内容。 ( 保密的论文在解密后应遵守此规定) 签名：奎全盘导师签名：i 坠墨! 翌日期： u 上海大学硕士学位论文 t h ep o s t g r a d u 脏1 m e s i so fs h a n g h a lu n i v e r s h y 1 1 引言 第一章绪论 随着计算机软硬件系统规模的日益复杂化，如何保证计算机系统的正确性和 可靠性，逐渐成为当前理论界和产业界共同关心的重要问题。今天我们已经很难 承受计算机系统发生故障所带来的损失，尤其是对于航天、金融、交通等行业的 计算机系统，其对安全性与可靠性的要求更是特别严格，系统中的任何一个小的 问题都有可能带来灾难性的后果。在计算机技术日新月异的今天，限制计算机实 际广泛应用的因素已经不再是机器硬件“缓慢”的速度和“低下”的计算能力， 而更多的是在设计和实现正确可靠的复杂系统时，我们本身的设计和保障能力还 比较有限，无法保证所设计系统的安全性和可靠性【l 】。传统的保证系统有效性的 方法是仿真和测试1 2 】。测试就是用选定的输入数据集合运行系统，通过比较所产 生的输出与预期值来判断系统是否会有错误。这种方法在检验的早期阶段还比较 有效，但是当要求系统更加“干净”一些时，就需要大量时间来寻找哪怕一点点 小的阀题。更为严重的闯题是，没有人知道什么时候可以结束测试，没有人知道 系统中是否还有潜伏的缺陷。正如著名计算机科学家e w d i j k s t r a 所说，测试只 能证明错误的存在，但不能证明错误的不存在，测试的局限性就在于此。所以需 要一种新的验证手段来确定系统的有效性和安全性。 在这种情况下，以数学方法为主要表达形式的形式化方法，正从理论研究走 向实际应用。形式化方法( f o r m a l m e t h o d s ) 【3 】是基于数学方法来描述目标软件系 统性质的- - 1 3 技术，用严格的数学符号和数学法则对目标软件系统的结构与行为 进行有效的综合、分析和推理，它为系统的说明、开发和验证提供了一个框架， 以便于发现目标软件系统需求中的不一致性、不完整性，及设计与要求相违背等 情况。形式化方法用数学方法描述系统的规格说明，并且根据数学理论来证明或 检查所设计的系统是否满足所期望的性质，它可以尽量避免错误和尽可能地发现 错误。实践进一步证明，形式化方法确实通过形式化的自动验证发现了用其它方 法不能发现的设计错误。模型检查( m o d e lc h e c k i n g ) 就是一种形式化验证方法， 上海大学硕士学位论文 卫! ! q 墅坠旦型! 望望竖竖堡! 幽鱼坚笪型! g 垦! ! 型 它基于状态搜索的基本思想，验证有限状态并发系统的有效性。模型检查以其简 洁明了和自动化程度高而引人注目。本文研究的对象就是模型检查。 1 2 当前研究概况 1 2 1 基本研究状况 模型检查方法最初由e m c l a r k e 和e a e m e r s o n 于1 9 8 1 年提出的。他们 用时序逻辑表示系统的期望性质，用状态迁移图表示系统模型，通过对系统状态 的搜索来判断系统模型是否满足这些性质。模型检查在机器理论证明、协议验证 和硬件验证方面都有非常好的应用。它有两个最显著的优点：其一是可以完全自 动化，不需要人工干预就可以完成整个检查过程：其二，当系统模型不满足某个 性质时可以给出反例，标识出错的位置，方便于排错。 而模型检查方法最大的缺点就是“状态爆炸”问题。当系统的规模越来越大 时，模型检查需要的空间和时间的开销将呈指数级增长，也就是状态数飞速增加， 实际运行检查需要的资源急剧膨胀。因此当一个系统的并发分量较多时，直接在 其状态空间上进行搜索在实际上是不可行的。为了能够有效地应用模型检查方 法，需要研究减少和压缩状态空间。通过大量研究人员的长期努力，一些方法已 经得到实现，并且已经应用到不同的模型检查工具中。 符号模型检查( s y m b o l i cm o d e lc h e c k i n g ) 的基本原理是将系统的状态转换 关系用时序逻辑公式表示 4 1 。在这种方法中，二叉判定图( b i n a r yd e c i s i o n d i a g r a m 。简称b d d ) 是用来表示时序逻辑公式的重要手段垆l ，它能较为紧凑地 表示状态转换关系，以降低系统模型所需要的内存空问。另外，状态转换的计算 可以以集合为单位，以提高搜索的效率。 o n t h e n y 搜索技术的基本原理是根据需要展开系统路径所包含的状态，这 些状态只是搜索状态空间的一部分，避免预先生成系统中包含的所有状态1 6 】。 一个系统可以由多个进程组成，并发执行时不同进程的动作可以有许多不同 的次序。基于对这一问题的认识，我们可以将某些状态的次序固定，以减少重复 验证本质上相同的路径。这种方法称为偏序归约( p a r t i a lo r d e r r e d u c t i o n ) 【7 】。 2 上海大学硕士学位论文 t h ep o s t g r a d u a t et h e s i $ o fs h a n g h a lu n i v e r s r r y 在由多进程组成的系统中某些进程可能完全类似，并发执行的结果可能产生 许多相同或相似的路径。基于对这一问题的认识，我们可以只搜索在对称关系中 等价的一种情形，以避免重复搜索对称或相同的系统状态。这种方法称为对称模 型检查技术( s y m m e t r y ) i 钔。 一般来讲，能够减少搜索空间的方法就能够同时节省时间和内存空间的需 求。由于内存空间在某些情况下比时间更为重要，有些方法的目标是以时间换空 间。例如在模型检查工具s p i n 6 】中实现压缩方法和用自动机表示可达状态的方 法【9 】o 除了在模型检查的过程中应用不同的方法以增加效率和减少内存空间的需 求外，还有许多研究的目标是减少模型本身或验证性质的复杂性。这方面的方法 包括：不同类型的抽象【1 0 l 、程序切片【1 1 1 、模型分解f 1 2 1 和验证性质的分解【1 3 1 。抽 象的基本想法是抽掉系统中的细节、用尽可能少的状态来刻画系统的运行过程。 程序切片基本的想法是将程序中不影响所要验证的性质的语句去掉以减少模型 的复杂性。模型分解的想法是将一个模型分解成若干部分，或者分别验证，或者 提供一个较好的组合方法以降低验证的复杂性。同样，一个需要验证的性质也可 能分解成若干部分分别验证，然后组合在一起验证。 1 2 2 模型检查技术的当前研究进展 作为模型检查基础的传统时序逻辑可以方便地表示离散事件或状态是否发 生以及发生的先后顺序，而在许多实际应用中人们不仅关心某一事件是否发生， 而且还要求它在确定的时间间隔内发生。这类对相关事件发生的时间有明确要求 的系统称为实时系统。实时系统涉及飞机控制系统、机器人、工业及军事控制系 统等安全性至关紧要的应用领域。对实时系统模型检查的研究取得了重大进展。 出现了表示实时系统的各种数字模型，如时间p e t r in t l 4 - 1 5 1 ，时间自动机以及各 种进程代数的时间扩充。 随着研究的深入，提出了多种描述系统的时序逻辑，如a c t l l l 6 1 ，c c t l i r 丌， e c t l l i s ，p l t l 和u 演算的实时扩充嘲，以及基于这些时序逻辑的各种算法研 究和归约研究。针对实时系统的数学模型和逻辑设计了各种模型检查的算法，并 上海大学硕士学位论文 t h ep o s t g r a d u a t et h e s i so fs h a n g h a iu n i v e r s i t y 实现了相应的分析与验证工具，如u p p a l l 、k r o n o s 、s t e p 、h y t e c h 等。 传统的模型检查是基于命题时态逻辑，如前面所介绍的e c t l ，p l t l 和u 演算。由于在实际问题中不可避免地要遇到数据与变量，为了用命题时态逻辑来 描述性质。在建模时往往需要做很多简化，这不仅增加了工作量，而且性质的描 述也不自然。而适用于带数据系统的逻辑是一阶逻辑( 也称谓词演算) 。为了描 述系统状态的改变以及并发进程之间的通讯，需要在经典的一阶逻辑中引入时态 词；为了表示无穷的行为，需要引入递归( 不动点) 算予 2 0 - 2 2 对于无穷数据域， 一阶时态逻辑的模型检查一般来说不终止，但是对于一些特定的问题，往往可以 用有限多个抽象数据对象来代表所有的数据对象( 例如通讯协议中被传输的数 据) ，因此可以进行模型检查。这一方法也可以应用于面向移动计算的形式模型， 如p 演算和a m b i e m 演算1 2 3 l 。还有基于三值逻辑的模型检查的研究也正在迸入实 际应用领域1 2 4 1 。 现在对模型检查技术的应用同样发展迅速。早期的模型检查侧重于硬件设计 的验证，随着研究的深入，模型检查的应用范围逐步扩大，涵盖了通讯协议、安 全协议、控制系统和一部分软件。利用已有的对u m l 的研究，把u m l 状态机， 实时活动图及顺序图转化到模型检查【2 5 脚1 ，从而可以直接利用u m l 作为建模工 具，再转化为模型检查的状态迁移模型，进行相关性质的验证。把模型检查的技 术应用于非线性相似系统的验证【2 7 1 ，应用c t l 模型检查生成x m l 的搜索路径堋， 应用模型检查分析系统的脆弱性等，都是模型检查的最新应用。随着网络和企业 应用发展，模型检查也被应用到w 曲应用程序设计1 2 0 、企业信息化、及工作流控 制等领域。通过验证和分析网络通讯协议【3 l 】及应用程序模型，以提升网络和 企业信息化的稳定性和可靠性，形成高效的商业价值。一种基于模型检查的入侵 检测方法解决了检测中的重复验证等问题，通过增加推理链的长度约束，引入时 序算子处理统计攻击，从而优化了入侵检测过程网。用分布处理来解决状态空间 爆炸，就是用分布式的概念划分模型，从而可以检查更大规模的系统模型【3 ”。在 验证中运用代理机制，把模型检查技术应用到对基于代理的系统进行验证【) ”。 当前模型检查技术正在飞速发展。从对模型检查本身理论的研究，到扩展其 应用领域都在经历着日新月异的变化。各种时序逻辑算子，和三值逻辑的应用 4 上海大学硕十学位论文 t h ep o s t g r a d u 肌1 1 1 e s i so fs h a n g h a iu n i v e r s i t y 也为研究模型检查提供了利器。 1 2 3 模型检查工具 模型检查的优点在于可以完全自动地进行验证。这一方法的成功在很大程度 上应归功于有效的软件工具的支持，以下介绍几个验证不同类型逻辑公式的软件 工具。 s m v 3 5 】是美国卡耐基梅隆大学开发的模型检测工具，用以检测一个有限状态 系统是否满足c t l 公式，它的建模方式是以模块为单位，模块可以同步或异步组 合。模块描述的基本要素包括非确定性选择，状态转换和并行赋值语句。其模型 检测的基本方法是以二叉图表示状态转换关系。 s p i n l 3 6 1 是美国贝尔实验室开发的模型检测工具，用以检测一个有限状态系统 是否满足p l t l 公式及其他一些性质。 c w b 3 7 1 的不同版本是英国爱丁堡大学和美国北卡洛莱纳州立大学相继开发 的模型检测工具。用以检测系统间的等价关系，p e r ，o r d e r 关系，以及系统是 否满足u 演算公式。 v e r i s o f t 3 8 是贝尔实验室开发的又一个检测分析工具，是一个大的工业化软 件产品。集成朗讯公司c d m ac a l l p r o c e s s i n g 软件库，每天通过无线网络处理百 万级的移动设备通信。 现在各种工具相继出现，通过不同的实现方法推动模型检查技术的发展和应 用。工具的复杂性也越来越大，集成化和功能也是越来越强大，已经不是单一的 对c t l 或l t l 时序逻辑的支持，已经发展为集成代码分析，建模，和语言转化等 多种功能。本文开发一个支持c t l 的模型检查器，输入和输出都以字符文件的方 式进行，从而为代码转换提供接口，并且当数据规模相对较大时，可以进一步实 现在局部状态空间进行搜索，为进一步开发集成化分析工具做好基础工作。 1 2 4 模型检查技术在软件领域的研究进展 模型检查技术是基于系统的轶态转移图，通过遍历状态空间，来检查系统是 否满足所要求的性质。对于软件验证通常局限于软件韵某些重要的组成都分，或 上海大学硕士学位论文 t h ep o s t g r a d u a t et h e s i so fs h a n g h a iu n i v e r s i 丁y 某些特定的属性，是基于系统的抽象和简化的模型。其基本思想是将一个过程或 系统抽象成一个有穷状态模型，然后加以分析验证。从验证角度来讲，这并非十 分严谨，更为确切的说法应该是对协议和软件的分析。然而，模型检查用于软件 系统的验证可以进一步保证系统的正确性。由于软件的复杂性和不确定性，使得 软件系统的状态个数通常没有实质上的限制，即系统模型的状态空间很大。而模 型检查的一个弱点就是状态爆炸问题，当系统的规模越来越大时，模型检查需要 的空间和时间的开销将呈指数级增长，使实际直接在其状态空间上进行搜索是不 可行。因此。模型检查技术在软件上的应用难度相对更大。 软件由于涉及无穷数据域上的运算而往往呈现出无穷状态，这是软件模型检 查的主要难点。软件验证的例子包括飞行系统软件的验证，验证的性质包括系统 所处的状态和可执行动作之间的关系。但是很多系统( 如控制软件) 并不涉及复 杂的数值计算，往往只用到线性实数约束或整数加减等简单的运算，因此可以采 用诸如线性约束求解等技术实现模型检查。另外也可以应用抽象技术映射到有穷 域上进行模型检查。这些都是建立在软件模型基础之上的。也就是说，先要有软 件系统的一个模型，然后在这个模型的基础上，对相关属性进行验证。所以当前 对软件的验证主要集中于系统设计与分析阶段，即在设计系统时，对某些特定要 求的属性加以验证，以证明达到设计的目的。 随着建模工具的发展，现在通过u m l 实现系统的建模，然后对相应的u m l 模型进行模型检型3 9 】。对于u m l 不同类型的图也出现不同的转换方式，如：从 顺序图i 删、活动图h ”、类卧4 2 1 、状态图【4 3 1 等到状态迁移系统的转换。对u m l 状 态切片【删与z 语言【4 5 1 到状态迁移系统的转换研究也是对模型检查技术的扩展。利 用u m l 不但可以为系统建模型，而且还可以自动生成相关的程序代码片段。这 也是u m l 应用于模型检查技术的一大优势。 同时模型检查还可以应用于其他方面，其基本思想是将一个过程或系统抽象 成一个有穷状态模型，加以分析验证。这方面的例子包括化学过程验证，验证的 性质包括阀门，管道和容器的状况；公司操作过程分析，分析的内容包括操作过 程是否具有所需的功能；电站操作程序的验证，验证的性质包括操作程序的动作 前后关系和操作是否安全可靠。 6 上海大学硕士学位论文 t h ep o s t g r a d u a t et h e s i so fs h a n g h a iu n i v e r s i t y 但是，现在对于代码级的模型检查研究很少。只在国外出现一些对程序代码 的验证工具f 4 6 4 7 ) 。本文的一个思想就是去掉从抽象到实现又从实现再回到抽象的 检查过程，直接从程序代码转换成状态，进而生成状态迁移系统，建立个用于 模型检查运算的模型，以此为基础，对代码的正确性进行验证，减少因为建模时 而增加的人为错误因素。 测试是保证软件产品可靠性和正确性的传统手段。与模型检查不同，测试是 对选定的输入数据集运行系统，通过比较所产生的输出与预期值来判断系统是否 会有错误。测试的主要局限性在于：对给定数据集通过了测试并不能保证在实际 运行中对其它输入不发生错误。与测试不同，模型检测不是针对某组输入，而是 面向某类性质来检查系统是否合乎规约。在系统不满足所要求的性质时，模型检 查算法会产生一个反例来说明不满足的原因，这一功能与测试有相同之处。如何 将模型检查与测试技术相结合，使两者有机结合，是当前研究的一个方向4 8 l 。本 文的另一个研究目标就是从模型检查入手，联系测试，应用模型检查的反例机制 生成测试用例，实现事前保证方式和事后检测手段的结合，把模型检查的方法和 有关应用推向测试领域，拓展模型检查的应用范围， 1 3 研究内容 本文提出建立集成化的模型检查工具的构想，把对一般的模型验证，并发系 统的验证，对程序代码的编译和分析，及对软件系统测试用例的生成和测试集成 在一个工具系统中，为用户提供系统化的验证服务。基于这一构想，本文研究模 型检查技术的基本原理和当前的应用，着重讨论模型检查在软件领域的应用，提 出把程序代码转化为时序逻辑结构，并对其进行验证。同时，也提出了基于模型 检查算法会输出路径的特点，把路径与测试用例相结合，实现软件测试用例的自 动生成，把模型检查技术扩展到软件测试。以上两方面的研究工作为集成化系统 工具的构想做了基础研究和相关的实例化工作。本文的主要内容包括以下几部 分： 1 ) 研究模型检查的标号算法，针对程序代码的验证，考察逻辑算子，提出 对程序代码的转换，并给了相关规则说明。考察模型检查路径与测试用例的联系， 7 上海大学硕士学位论文 t h ep 0 s 卫塑塑堕a t et h e s i so fs h a n g h a iu n i v e r s i t y 提出用路径生成测试用例，把模型检查技术应用于软件测试，给出了相关算法描 述。 2 ) 实现一个针对c t l 逻辑公式的模型检查器，作为软件模型检查和测试用 例生成的前提。 3 ) 实现程序转换算法，将程序代码和模型检查的状态结合，完成从程序代 码到k r i p k e 结构的转换。实现了测试用例生成算法，把软件测试与模型检查有 机结合，扩展模型检查的应用范围。 1 4 本文的组织结构 本文共分五章，内容安排如下： 第一章，绪论。综述当前对于模型检查技术的研究进展，及最新成果。关注 模型检查在软件领域的应用，发现本课题的研究入口，提出建立自己的模型检查 器，以代码为基础，直接生成状态迁移系统用于检查，以及模型检查技术和软件 测试技术的结合应用。 第二章，模型检查技术。首先概述了模型检查技术的主要思想，给出广泛采 用的数据表达形式k r i p k e 结构，及对时序逻辑c t l 公式的介绍。最后给出模型 检查标号算法的语言描述，并指出可以按此算法实现模型检查器。 第三章，软件验证技术。这一章是本文两个研究内容之一。首先，讨论对程 序代码进行验证的必要性。然后，针对c 语言程序代码的特点，在研究时序逻 辑公式的基础上，提出c 语言程序转换为逻辑公式的一般规则。分别从顺序程 序，并发程序，和同步与互斥三个方面具体描述转换方法。最后给出具体的开发 实现，根据不同的内容给出相关的数据表示形式和算法。包括：一个基于c t l 公式的模型检查器和一个对c 语言代码实现转换的验证工具。 第四章，测试用例生成技术。这是本文两个研究内容的另一个。研究时序逻 辑算子，根据存在量词公式的证据是全称量词公式的反例的特性，考察时序逻辑 算子，寻找验证公式的路径，并应用路径生成测试用例进行软件测试。首先给出 算法描述，然后对算法进行实现，构造一个测试用例生成器，最后给出一个实例 具体说明测试用例的生成。本章把模型检查技术扩展到软件测试领域，深化了模 上海大学硕士学位论文 1 h ep o s t g r a d u a t et h e s i so fs h a n g h a iu n i v e r s l 下y 型检查的应用。 第五章，总结与展望。总结全文的主要工作，指出下一步需要开展的研究工 作，并对集成化的系统工具提出了展望。 9 上海大学硕士学位论文 t h ep q 墅堕! 蚀u a t et h e s i so fs h a n g h a iu n i v e r s i t y 第二章模型检查技术 随着计算机软硬件系统日益复杂，如何保证其正确性和可靠性成为紧迫需要 解决的问题，由此提出的诸多理论和方法中，模型检测以其简洁明了和自动化程 度高引人注目。模型检测的研究范围大致涵盖以下内容：时序逻辑，模型检查算 法及其时空效率的改进，以及支持工具的研制。这几个方面之间有着密切的内在 联系，不同时序逻辑的模型检查算法的复杂性不一样，针对的问题不一样。本章 主要介绍基于计算树逻辑( c t l ，c o m p u t e r t r e el o g i c a l ) 的模型检查技术。 2 1 模型检查技术概述 模型检查是一种针对有限状态并发系统( f i n i t e s t a t ec o n c u r r e n ts y s t e m ) 的形 式化自动验证技术，它通过穷尽搜索系统的整个状态空间( s t a t es p a c e ) 来检查 系统模型是否满足给定的性质。对模型检查的研究始于上个世纪8 0 年代初，当 时c l a r k e ，e m e r s o n 等人提出了用于描述并发系统性质的c t l 逻辑，设计了检查 有穷状态系统是否满足给定c t l 公式的算法，并实现了一个原型系统，这一工 作为自动验证并发系统的性质开辟了一条新的途径。模型检查的基本思想是用状 态迁移系统( m ) 表示系统的行为，用时序逻辑公式( f ) 描述系统的性质，这 样系统是否具有所期望的性质，就转化为数学问题：“状态迁移系统m 是否是公 式f 的一个模型? ”，可用公式表示为 m | - f ? 这个问题是可判定的，也就是说在有穷的时间内是可以完成的。因为系统状 态的有穷性，检查器可以通过对系统状态空间的一次遍历，判断公式是否成立。 而对于一些具有无限状态的系统，可以通过抽象和归纳归约到有穷状态系统上。 用模型检查技术对系统进行验证，判断其是否符合设计要求，其过程可以描述如 下：( 如图2 1 所示) 建模：把需要设计分析的系统转化为一种模型检查接受的形式化的模型，即 1 0 上海大学硕士学位论文 t h ep o s t g r a d u a t e1 h e s i so fs h a n g h a iu n i v e r s i t y 状态迁移系统： 给出规格说明：把系统的属性及对系统的要求，作为规格说明以时序逻辑公 式的形式给出，以便于进行验证； 验证：根据模型检查算法，在系统模型的状态空间内对规格说明进行验证。 并对不符合要求的规格说明给出反例。指出错误所在。 图2 1 模型检查过程示意图 基于状态迁移系统的模型检查算法有两个重要的优点；一是建立在状态迁移 系统之上的模型检查是全自动的，并且不需要用户掌握很深的数学方面的专业知 识，就可以完成验证过程。这为模型检查的广泛应用提供了方便之门；二是如果 系统模型不能满足某一规格说明，模型检查算法会给出反例，也就是错误路径， 标识何处出现了错误，而这样的反例将会对查找错误原因和修正错误提供重要的 帮助。另外，通过对模型检查算法的修改，当对某一逻辑公式验证为真时，也可 以输出一条路径，表示公式的正确性，即证据路径，本文的第四章就是基于这一 特性展开研究的。 而模型检查的最大局限性就是系统“状态空间爆炸”问题。当系统规模庞大 时，系统的状态空间急剧增大，这样对时间和空间的需要，在实际工作中使模型 检查运算无法完成。针对这一问题很多研究工作已经进行，并取得了相应的成果。 一方面，从扩充计算机处理能力入手，解决用尽量少的资源处理尽可能多的状态。 如：o n t h e 。f l y 技术，o b d d 的采用。另一方面，从限制系统模型的规模入手， 上海大学硕士学位论文 t h ep o s t g r a d u a et h e s i so fs h a n g h a iu n i v e r s i t y 减少系统模型的状态，使系统模型的状态空间缩小到实际可以运算的程序。如： 归约，抽象，切片，局部状态空间等【3 1 。这样从一定程度上缓解了状态爆炸问 题。 随着研究的深入，模型检查的应用越来越广泛，涵盖了通讯协议、安全协议、 控制系统、电子线路、和软件系统等多领域。模型检查技术的应用，也标示着人 们对系统的安全性和正确性的关注又进展一步，同时对系统安全性越来越重视， 也促进了模型技术本身的发展。 2 2k r i p k e 结构 对系统进行验证的首要工作就是：构建系统的形式化模型，使计算机程序可 以方便地处理验证过程。这里用到的数据结构就是k f i p k e 结构，用状态迁移系 统来描述系统的形式化模型。k r i p k e 结构是一种基于状态迁移关系的结构，便于 模型检查运算，对系统的验证就是在k r i p k e 结构上，按状态关系寻找满足条件 的路径。k r i p k e 结构定义如下： 一个原子命题集( a p a t o m i cp r o p o s i t i o n ) 上的k r i p k e 结构是一个四元组m = s ，s o ，l ) ，表示一个有限状态并发系统模型。其中： a p 是原子命题集，表示系统具有的基本性质。 s 是系统的状态集，也就是状态空间，是模型检查的基础。 s 。s 是系统的初始状态集。 r s s 是系统状态间的转换关系集。 l ：s 一2 a p 是标号函数，标识在每个状态上为真的命题。对于任一状态s ， 如果一个命题f 出现在状态s 上，即：f e l ( s ) ，则说明命题f 在状态s 上是满足 的。 从而一个系统模型就是一个k r i p k e 结构。系统的运行过程，可以表示为一条 路径，就是一个状态的无限序列萨s o s l s 2 。表示从初始状态s o 开始的系统运行 轨迹。有时，在不考虑初始状态时s 。可以省略。如图2 2 所示是一个k r i p k e 结 构示意图。其中：s = 1 ，2 ，3 ) ；r = ， ，q ，l ，电，3 ，q ，3 ；l = ( 1 ， a ，b ) ，( 2 , b ，c ) ，( 3 ，c ) ) 。图中标出来的字母代表在此状态上为真的命题。 上海大学硕士学位论文 t h ep o s t g k a d u a t et h e s i so fs h a n g h a lu n i v e r s i t y 2 3 时序逻辑 2 3 1 计算树逻辑 图2 - 2 一个k r i p k e 结构状态迁移图 时序逻辑( t e m p o r a ll o g i c ) 是模型检查的理论基础，是一种命题逻辑，是研 究问题的必然性、可能性及其相关概念的一个逻辑学分支，在描述并发系统中是 非常有效的。时序逻辑并不直接需要时间向量，就可以描述出事件间的先后顺序， 表示事件的发生序列。时序逻辑应用原子命题和布尔运算符，如：与、或、非等， 可以组成复杂表达式，来表示系统的某一属性。而时序逻辑通过时序逻辑算子表 达事件的发生顺序。时序逻辑算子也可以和布尔运算符进行联合或嵌套，组成更 复杂的时序逻辑公式。一个时序逻辑公式，表示系统的某一属性，也可以说是系 统的一条路径，可以描述系统中某一状态是可能达到的，或者某一状态是永远也 无法到达的。 时序逻辑有多种表达方式，我们这里计论的是计算树逻辑( c t l ，c o m p u t a t i o n t r e el o g i c ) 。从概念上讲，计算树逻辑就是一种用计算树描述系统的形式化方法。 在k r i p k e 结构表示的状态空间中，以初始状态为根，每个状态又有多个可能的 后继，按所有可能的路径扩展成计算树，这样就形成一个计算树( 如图2 3 所示) 。 这棵计算树表现了从根结点开始的所有可能路径，是一种展开的系统状态图。 计算树逻辑是一种分叉时序逻辑，可以描述状态的前后关系和分叉情况。用 c t l 描述的状态或性质就是c t l 公式。c t l 公式由原子命题符号，逻辑连接符 号，路径算子( p a t hq u a n t i f i e r s ) 和时序算子( t e m p o r a lo p e r a t o r s ) 组成。 上海大学硕士学位论文 t h ep o s t g r a d u a ：r et h e s so fs h a n g h a lu n i v e r s | t y 展开胂杭番田 图2 - 3 与图2 - 2 对应的计算树 c t l 逻辑连接符号最基本的是： 一( 菲) ，v ( 或) ，a ( 与) 路径算子用来描述计算树上的分叉情况。表示在以从某状态开始的所有路径 或某一路径满足的性质。路径算子包括： e ( e x i s t s ) 表示对于某一分枝 a ( a l w a y s ) 表示对于所有分枝 时序算子用来描述贯穿计算树的路径的性质。存在五个基本算子： x ( n e x tt i m e )表示路径上当前状态的下一状态。 f ( i nt h ef u t u r e ) 表示路径上以后的某个状态。 g ( g l o b a l l y ) 表示路径上的所有状态。 u ( u n t i l ) 表示直到某一状态 r ( r e l a t i v e ) 表示u 的对偶状态 2 3 2 c t l 公式 c t l 公式有两种类型：一种是状态公式( s t a t ef o r m u l a s ) ，在某一状态上为 “真”；一种是路径公式( p a t h f o r m u l a s ) ，在某条路径上为“真”。 状态公式的合式公式定义如下： ( 1 ) 如果p a p ，那么p 是状态公式。 ( 2 ) 如果f 和g 是状态公式，那么- 1 f f v g 和f a g 都是状态公式。 1 4 上海大学硕上学位论文 t h e p o s t g r a d u a t et h e s i so fs h a n g h a iu n i v e r s i t y ( 3 ) 如果f 是路径公式，那么e f 和a f 都是状态公式。 路径公式的合式公式定义如下： ( 1 ) 如果f 是状态公式，那么f 也是路径公式。 ( 2 ) 如果f 和g 是路径公式，那么一f ，f v g ，f a g ，x f , f f , g f , f u g ，和 f r g 都是路径公式。 定义一是路径冗从状态s 开始的后缀。如果f 是状态公式，那么表达式m ，s l = f 就是说在k r i p k e 结构m 中f 在状态s 上为真。如果f 是路径公式，那么表达式 m ，f f 表示在k r i p k e 结构m 中沿着路径兀，f 为真。下面是l = 的些表达式：( f l 和f 2 是状态公式，9 1 和啦是路径公式) 1 m ，s f p静p u s ) 2 m ，s 产一f lm ，s j f l 3 m ，s 户f l v 龟铮m ，s l = f i 或m ，s | - 龟 4 m ，s i = f l 八营m ，s p f i 且m ，s | - f 2 5 m ，s p eg t铮存在一条从s 开始的路径兀满足m ，兀p g l 6 m ，s p a g l 所有从s 开始的路径兀都满足m ，霄| - g l 7