航天嵌入式操作系统的分析与验证.pdf

第 1 8 卷第 6期 2 0 1 2年 1 1 月 载 人 航 天 Ma n n e d S p a c e f l i g h t Vo 1 1 8 No 6 6 9 航天嵌入式操作系统的分析与验证 李斌，马 越，李 潇，刘 剑(中国科学院软件研究所基础软件国家工程研究中心，北京 1 0 0 1 9 0)摘要在介绍航天嵌入式操作 系统的特点和应用概况的基础上，阐述 了对航 天嵌入 式操作 系统进行 自动分析与验证 的必要 性，综述 了自动分析和验证技术，并重点介 绍了模 型检测和符号执行两种分析技术，列举 了领域内近年来具有代表性的工具及分析实例。结 合航天嵌入式操作系统的特点，总结了嵌入式操作系统 自动分析与验证技术面临的挑战，包括状态爆炸、描述不精确性、代码复杂度、实时性分析等。关键词嵌入式操作 系统；分析验证；静态分析；模型检测；符号执行；航天 系统 中图分类号：T P 3 1 6 文献标识码：A 文章编号：1 6 7 4 5 8 2 5(2 0 1 2)0 6 0 0 6 9 0 6 1引 言 嵌入式系统是一种“完全嵌入受控器件内部，为 特定应用而设计的专用计算机系统”。与一般的通用 计算机相比，嵌人式系统一般专用于特定的任务。嵌 入式系统对成本、软件安全性、功耗约束等的要求通 常高于通用计算机，而其运行环境往往比较恶劣，系 统资源较少。应用在航天领域中的嵌入式系统，其设 计标准要远高于一般的嵌入式系统。从硬件方面来 说，航天领域中的嵌入式系统硬件必须具有较好的 耐用性，具备在恶劣环境(高 f 氐 温度，强辐射，强干 扰)下的工作能力等等。对于其操作系统，必须具有 高实时I生，高可靠性等特点。高实时眭保证嵌入式系 统能及时地对中断进行响应，并在限期内完成每一 个任务。高可靠性则保证嵌入式系统能够正确地执 行全部任务。嵌 入式 操作 系统(e m b e d d e d o p e r a t i n g s y s t e m，E O S)是嵌入式系统软件的核心部分，是应用软件运 行的平台。它负责嵌入系统的全部软 硬件资源的分 配、调度、控制、协调和并发等活动；它必须体现其所 在系统的特征，能够通过装卸某些模块来达到系统 所要求的功能。嵌入式操作系统和通用操作系统的 主要差别是，通用操作系统追求最大的系统吞吐量，合理的响应速度，公平的资源分配；而嵌入式操作系 统表现为实时高效、强硬件依赖性、软件固态化和应 用专用化等；实时操作系统的根本要求是保证实时 任务的时间正确性，强调实时性、可靠性、灵活性，以 及系统行为的可预测性。伴随计算机应用技术的提升，嵌入式操作系统 从 8 0 年代起得到了很大的发展。常见的商用嵌入式 操作系统有 V x wo r k s、p S O S、Q N X、O S 一 9、L y n x O S、Wi n d o w s C E、P a l m O S、L i n u x等。其 中 V x Wo r k s、p S O S、L y n x O S 等操作系统以其较高的实时生 和可靠 性被广泛应用于航空航天，军事，国防的关键领域。除商用的嵌入式操作系统外，也有些开源的嵌入 式操作系统，其中较有代表l生 的是 R T E M S 系”。该 系统作为最早用于美国国防系统的开源嵌入式操作 系统，目前仍广泛应用于军事、航天等领域。表 1 总 结了航空航天领域内，一些重大项 目中应用的嵌入 式操作系统。最近几年，国内对嵌入式操作的系统 收稿 日 期：2 0 1 2 0 2 2 9；修回日 期：2 0 1 2 0 9 0 7 基金项 目：载人航天领域预先研究项 目(0 0 0 3 0 1)，国家自然科学基金项 目(6 1 0 0 3 0 2 8、6 1 0 7 3 0 4 4、6 0 9 0 3 0 5 1)作者简介：李斌(1 9 8 5 一)，男，硕士，助理工程师，主要从事操作系统的形式化分析与验证工作。E-m a i l：l i b i n n f s i s c a s a c c n 万方数据7 0 载人航天 第 1 8 卷 表 1 嵌入式操作系统在航空航天领域中的代表性应用 嵌入式操作系统 曾用项 目 是否继续开发 从 1 9 9 2年到 1 9 9 9年间的 中小型太空探测器 V X T X 1 9 9 5 年的x射线定时探测器 否“哈勃”空间望远镜 I n t e t y 美国空间服股中的多种飞机：F 一 2 2、F 一 3 5 战斗机，U H 一 6 0 直升机等等“哈勃”空间望远镜 N u c l e u s 是 戈达德航天中心的抗辐射Co l d f i r e G P S系统 地球观测卫星一 1 号“流浪者”系列火星探测器 V X W O r k s 是“战神”一号和“战神”五号的运载器使用的飞航指挥计算机 MS 一 1 号推进系统的控制器 s T 一 5 卫星、研究地球磁场风暴的T H E M I S 计划 眦 M S 是 关于外星体探测：太阳动态探测器 的研究越发重视，已经有 中科院的 H o p e n O S(女娲 计划)，浙江大学的 H B O S 等 自主研发的实时系统 面世。嵌入式操作系统主要面临的问题是响应时间和 硬件资源消耗受限，以及内存访问错误、缓冲区溢出 错误、指针引用错误、异常控制、堆栈溢出等造成的 安全隐患。如果操作系统的实时陛和安全性不能得 到有效保障，有可能会使得整个系统产生严重的事 故。例如，1 9 9 7年火星“探路者”号在执行任务时，遇 到系统频繁重启问题。导致频繁重启的根源是当高 优先级的母线管理进程在等待低优先级的气象处理 进程完成时，会产生一个启动通信进程的中断。这个 通信进程会把母线管理进程悬挂起来，进而导致系 统重启。正是因为航天领域中细微的错误往往能导 致灾难性的后果，如空间或地面设施 的损毁、工作人 员死亡或受伤。因此，对航天嵌入式操作系统进行分 析和验证是至关重要的。为规范航天系统的开发、测试和使用，并确保其 可靠性、安全性，各大航天机构建立了相关的标准。具有代表性的标准有 D O 一 1 7 8 B和 E C S S 标准2j。由 美国的航空无线电技术委员会提出的 D O 一 1 7 8 B标 准，对航空电子系统中的软件的各个方面制订了全 面的评判准则，包括生存周期、需求、验证与分析、质 量控制等等。E C S S 则是 E S A针对整个航空电子系统 提出的设计规范。其中 E 4 0 B是 E C S S中针对包括地 面控制系统和航空部件系统的软件工程和过程提出 的标准，包含响应性、交互性、硬件限制和软件验证 等方面。2形式化分析和验证技术 基于以上的背景和需求，工业界和学术界都非 常重视嵌入式操作系统的可信分析和验证技术。现 有的分析和验证技术可以通过是否需要运行软件划 分为静态分析技术和动态分析技术两大类。静态分 析技术多被用于软件缺陷检测、代码优化、程序转换 等方面，同时也可用于动态分析中。动态分析是通过 运行具体程序并获取程序的输出或内部状态等信息 来验证软件性质的过程。本文重点关注静态分析技 术，为了便于理解，又可将静态分析技术进一步细分 为以下几类：基本程序分析、基于形式化验证的分 析、指向分析和其它辅助分析方法。其中基本程序分 析方法有控制流分析和数据流分析。控制流分析是 面向程序控制流的一种静态分析方法。控制流分析 通过分析程序中循环、跳转等控制信息，对一些语句 进行合并，最后得出程序的一个控制流图。控制流描 述的是程序中各个语句之间的关系，它还可以对程 序进行一些优化，典型的如循环优化。典型的工具有 F o r t i f y、斯坦福大学的 C o v e r i t y t3 1等。数据流分析是试 图推导程序中各种变量沿着程序执行路径流动的信 息。数据流分析需要基于控制流图，分析的方向包括 前向和后向两种。有代表性的工具包括 V i r g i n i a 大学 开发的 L c L i n t，主要针对缓冲区溢出漏洞；S t a n f o r d 万方数据第 6 期 李斌 等：航天嵌入式操作系统的分析与验证 7 1 大学开发的 A R C H E R t 工具，主要分析大型软件 中数 组越界问题。基于形式化验证的分析方法主要有模 型检测、约束求解、抽象解释和定理证明。模型检测同 是基于模型系统，自动测试模型是否满足给定的性 质。模型检测技术多用在硬件或者软件系统中，是一 种面向有限状态系统的自动验证安全性质的技术。验证的内容包括系统是否会出现死锁状态，或者其 它的一些导致系统崩溃的极端状态。通常模型检测 的对象并非程序本身，而是使用数学语言将 目标系 统转化形式化描述，同时验证的性质是使用时序逻 辑表示 的公式。近年来软件模型检测技术成功地应 用在了通用操作系统的分析和验证中，例如微软开 发的 S L A M 川 和 S D V等工具应用于 Wi n d o w s 7等商 用操作系统的开发中，并极大提高了开发效率和目 标系统的可靠性。具有代表性的工具还有 MO P S t8 1、B a n d e r a 9 1 和 J a v a P a t h F i n d e r f 埘，可 以认为上述技术也 可以成功应用嵌入式操作系统的分析和验证。表 2 是近几年在软件检测领域广泛认可的 1 1 种模型检 测工具以及所用的技术支持嗣。约束求解【1 1】又称为约束满足性问题，指的是定 义的对象需要满足一组约束或者限制。在程序分析 中，将程序代码转化为一组约束，并利用求解器来获 取满足约束的解。约束求解多和数据流分析等其它分 析方法相结合使用，可解决如路径可达性分析、程序 不变式分析等问题。主要工具有早期的谓词抽象求解 器 s i m p l if y、z a p a t o 切，经典的用于抽象模型的求解器 S A T 】、能力更强的 S M T求解器，如 B a r c e l o g i c【14 、B e a v e r t垌、Bo o l e c t o r 6 1、C VC 3 、AL E r g d 垌、Ma t h s a t 4 t 、O p e n S MT t Z l、S w o r d E”、V e r i T 、Y i e e s 2 3 1、Z 3 t2 4 1、S T P 2 、以 及 S p e a r u 等。抽象解释_27 是使用抽象对象域上的计 算逼近程序真实的对象域上的计算，使得程序抽象 执行的结果能够反映出程序真实运行的部分信 息。抽象解释最终为程序建立一个抽象模型，如果 抽象模型中不存在错误，就证明其对应的源程序中 也不存在错误。许多集成模型检测系统在建模阶段 也使用了抽象解释技术，具有代表性的分析工具有 P r o v e r i f t E s 和 AS T R E E 2 9 。自动定理证明3 0 1 也称为机器 定理证明，是通过将验证问题转换为数学上的定理 证明问题来判断待分析程序是否满足指定属性。自 动定理证明属于形式化理论和人工智能领域，其成 果也可用在程序验证中。定理证明工具都要求程序 员通过向源程序中添加特殊形式的注释来描述程 序的前置条件、后置条件以及循环不变量。代表性 工具有 E S C 3 和 E s c J a v a l32 l，如 I s a b e l l e 交互式定理 证明器也在实际工作中有所应用，但巨大的工作量 使其无法应用于大型系统。表 3 罗列了一些利用自 动定理证明形式化验证的非商业 O S内核的分析结 果。其中 V F ia s c o R o d i n、E R O S C o y o t o s 都是针对嵌 入式微内核分析和验证项 目。V e r i s o f t L 4 v e ri f i e d是 由澳大利国立研究院和德国慕尼黑大学等知名研究 机构和大学主导的嵌入式操作系统验证的典型例 子，其目标是研发经过严格形式化验证的 O S内核，该项 目在学术界和工业界都有一定 的影响。另外，指向分析方法主要有：别名分析、指针分 析、形态分析和逃逸分析，其主要与系统特定性质密 表 2 模型检测部分工具列表 模 型 检测 的某 方法概述 实现工具 不足 一分支 有界限的模型 所有的无限类型的代码结构，比如 只能发现错误，不能证明程序是正确的，因为它不能保证在真如过 n 检测 w h i t e 循环，最多展开 n 次。C B M C 次展开的情况下会出现反例。使用调用定理证明器或 S A T 求解器，B L A S T、B O O P、调用次数会呈爆炸式增长。断言抽象 数据溢出问题 对数据下断言的方法来抽象数据。M AGI C、S L M 对部分 C语言结构不支持 转换为 中间模 先把 目 标程序转换为一种模型，这种 F E A V E R、在目标程序中的 c 语言和底层硬件细节在转换过程中被过滤了。模型可以被通用的模型检测器处理。F O C U S C、只有被通用的模型检测器支持的c语言代码结构能被检测。型的方法 然后检测这些模型。H E C K、M O P S 转换会导致模型增大 转换 为机器语 将 C 语言转化为机器语言，再对后者 转换会导致模型增大 言的方法 进行模型检测。S T E A M、Z I N G 状态空间爆炸。万方数据7 2 载人航天 第 1 8 卷 表 3 利用自动定理证 明的 O S验证工作【项 目 最高级别 最低级别 规格 证明 证明器 方法 时间 l V F ia s c o R o d i n 不 会 崩 溃 C+7 0 0 P V S s e m a n ti c c o m p ile r 2 0 0 1-2 0 0 8 E R 0 S C o v o t o s 安全模型 B i t C 安全模 型 O A C L 2(?)l a n g u a g e b a s e d 2 0 0 4 一(?)V e r i s o f t 应用程序级别 门级 1 0 0 7 5 I s a b e l l e f u l l y p e r v a s i v e 2 0 0 4 一(2 0 0 8)I Av e r i fi e d 安全模 型 C a s s e mb l y 1 0 0 7 O I s a b e l l c p e r f o r ma n c e p r o d u c t i o n c o d e 2 0 0 5 一(2 0 O 8)切相关。其它辅助分析方法主要有：符号执行、切片 分析、结构分析。其中符号执行f3 嗵过使用抽象的符 号跟踪程序中的变量来模拟程序的实际执行。符号 执行可 以看作抽象解释的一种。其特点是通过记 录 程序执行状态，包括程序变量的符号值、路径条件、程序标记等信息为程序分析提供了准确的上下文信 息。符号执行方法可以被应用于一些大型程序的分 析中，但其分析结果的可靠性需依赖于所允许的分 析时间和对路径及其数 目的选择等方面。有代表性 的符号执行工具包括早期 的 P e r fi x t3 4 和 E S P E 3 以及能 力更强大的 E X E 3 6 1、C u t e r3 7 1、D A R T 3 S 、S A G E 3 9 1、K L E E 和 S 2 E 4 等。此外，系统化测试技术也是当前嵌入式分析验 证的重要技术之一，该技术一般基于某种 自 动推理 方法和技术，例如，符号执行 以及约束求解等。N A S A支持符号执行技术开发的 J P F，成功应用于 火星探路者系统的软件开发中。由中科院软件所开 发 中的 N F S V e r i fi e r 就是基 于上述两种方法实现 的 验证工具。与通用软件的验证和分析相比，针对嵌入式操 作系统的分析与验证面临着很多特殊的问题。其中 主要包括：许多嵌人式系统设计时只关注系统功能 的实现，缺乏异常处理机制的支持；嵌入式系统函数 调用逻辑非常复杂，并伴有中断处理从而难以精确 地模拟程序的运行状态；静态检测工具很多都是商 业化的，开源的检测工具较少；嵌入式操作系统和一 般的嵌入式软件系统相比，与硬件结合的更紧密，采 用内联的代码检测增加了检测的难度等。3结束语 近年来，随着航天科技的发展，嵌入式系统在航 天领域的应用变得愈发广泛。嵌入式操作系统作为 嵌人式系统的核心，对其各项性质的验证是至关重 要的。中国科学院软件研究所在嵌人式操作系统的 可靠性验证方面有长期的积累，进行过系统化的研 究工作。例如，早在上世纪 9 0 年代，唐稚松院士领导 的研究小组就基于 X Y Z 逻辑语言 对某嵌入式系统 进行了验证分析，发现其中存在的优先级逆转的问 题。近年来，软件所国家基础软件研究中心积极研发 嵌入式操作 系统 的分析验证技术，其中包括：基于抽 象解释技术对嵌入式操作系统的驱动模块进行分析 验证的方法，基于动态二进制代码转换技术和符号 执行技术对系统的单元模块进行系统测试等。在我国航天技术迅猛发展的今天，嵌入式操作 系统和软件的分析和验证技术将是很有发展前景 的研究方向，作为一项同时具备基础性研究和工 程应用意义的课题，航天嵌入式操作系统的分析 与验证已经成为我国航天高可信软件技术研究的焦 点之一。参考文献 1 J H e l d e r S i l v a，J o s e S o u s a。D a n i e l F r e i t a s，S e r g i o F a u s t i n o R T E MS I mp r o v e m e n t S p a c e Q u a l i fi c a t i o n o f R T E MS E x e c u t i v e D A t a S y s t e ms i n Ae r o s p a c e，2 0 0 7 【2 j L j e r k a B e u s D u k i c C O T S R e al-T i me O p e r a t i n g S y s t e ms i n S p a c e Th e S a f e t y Cr i t i c al S y s t e ms Cl u b，2 0 01 3 j C o v e r i t y C o m p a n y H o me P a g e，h t t p：w w w c o v e ri t y c o m【4 j DE v a n s，DL a r o c h e l l a I m p r o v i n g S e c u ri t y U s i n g E x t e n s i b l e L i g h t w e i g h t S t mi c A n a l y s i s I E E E S o f t w a r e 2 0 0 2(1)：4 2 5 1 5 J Yi c h e n X i e，A n d y C h o u，D E n g l e r A RC H E R：Us i n g S y m b o l i c，P a t h s e n s i t i v e An a l y s i s t o De t e c t Me mo r y Ac c e s s Er r o r s Pr o c e e d i n g s o f t h e 9 t h E u r o p e a n s o f t w a r e e n g i n e e r i n g c o n f e r e n c e h e l d j o i n t l y w i t h 1 l t h AC M S I GS OF T i n t e r n a t i o na l s y mp o s i u m o n f o un d a t i o n s o f s o f t wa r e e n g i n e e ri ng 2 0 0 3：3 2 7 3 3 6 6 J B a s t i a n S c h l i c h，S t e f a n K o w a l e w s k i Mo d e l c h e c k i n g C s o u r c e c o d e f o r e mbe d d e d s y s t e ms I nt e r n a t i o n a l J o u r n al o n S o f t ware To o l s，一 S p rin g e r，2 0 0 9 1 7 J B a l l T，R a j a m a n i S K T h e S L AM p r 0 j e c t s De b u g g i n g s y s t e m s o f t w a r e v i a s t a t i c a n a l y s i s 2 0 0 2 【8 J C h e n H，Wa g n e r D A MO P S：An i n f r a s t r u c t u r e f o r e x a mi n i n g s e c u ri t y p r o p e i e s o f s o f t wa r e P r o c e e d i n g s o f t h e 9 t h ACM C o n f e r e n c e o n 万方数据第 6 期 李斌 等：航天嵌入式操作系统的分析与验证 7 3 C o mp ut e r a n d Co mmu n i c a t i o n s S e c u r i t y W a s h e n g t o n，DC，US A，2 0 0 2：2 3 5 2 4 4【9 J C o r b e t t J e t a 1 B a n d e r a：E x tr a c t i n g fi n i t e s t a t e mo d e l s f r o m J a v a s o u r c e c o d e P r o c e e d i n g s o f t h e 2 2 n d I CS E L i me ric k，I r e l a n d，2 0 00：43 9-4 5 8 1 0 V i s s e r W，Ha v e l u n d K，B r a t G，P a r k S Mo d e c h e c k i n g p r o g r a ms P r o c e e d i n g s o f t h e I nt e r n a t i o n a l C o n f e r e n c e o n Au t o ma t e d S o f t wa r e En g i n e e ri ng Gr e n o b l e，F r a n c e，2 0 0 0 1 1 Z h a n g J，Wa n g X A c o n s t r a i n t s o l v e r a n d i t s a p p l i c a t i o n t o p a t h f e a s i b i l i t y a n a l y s i s 2 0 01 1 2 De t l e f s D，N e l s o n G，S a x e J B S i mp l i f y：A t h e o r e m p r o v e r f o r p r o gra m c h e c k i n g J o u r n a l o f t h e A C M，2 0 0 5，5 2(3)：3 6 5-4 7 3 【1 3 B all T，C o o k B，L a h M S K，Z h a n g L Z a p a t o：A u t o ma t i c t h e o r e m p r o v i n g f o r p r e d i c a t e a b s t r a c t i o n r e fin e me n t I n：Ha r ald G，e d P r o c o f t h e 1 6 t h I n t 1 Co n f o n Co mp u t e r Ai d e d Ve r i fi c a t i o n Be r l i n：S p r i n g e r-Ve r l a g，2 0 0 4 4 5 7 46 1 1 4B o r r a l l e r a s，C，L u c a s，S，N a v a r r o-Ma r s e t，R ，R o d r l g u e z C a r b o n e l l，E，Ru b i o A S o l v i n g No n-l i n e ar P o l y n o mi al Arit h me t i c Vi a S AT Mo d u l o L i n e a r Ar i t h me t i c I n：P r o c o f t h e 2 2 n d I n t e rna t i o na l C o n f e r e n c e o n Au t o ma t e d De d u c t i o n，2 0 0 9，v o l u me 5 6 63 o f L e c t u r e No t e s i n Ar t i fic i a l I n t e l l i g e n c e，P P2 9 4-3 0 5 1 1 5 S J h a，R L i m a y e；a n d S S e s h i a B e a v e r：E n g i n e e r i n g A n E f f i c i e n t S MT S o l v e r Fo r Bi t Ve c t o r Ar i t h me t i c I n Pr o c o n Co mp u t e r Ai d e d V e ri fi c a t i o n(C A V)，2 0 0 9：6 6 8 6 7 4 1 1 6R B r u mma y e r a n d A B i e r e B o o l e c t o r：A n E ffic i e n t S M T S o l v e r f o r B i t-Ve e t o r s a n d Ar r a y s I n P r o c C o n f e r e n c e o n T o o l s a n d Alg o r i t h ms for t h e C o n s t r u e t i o n a n d A n a l y s i s o f S y s t e m s(T A C A S)2 0 0 9，S p r i n g e r P P 1 7 4 1 7 7 1 7 C l a r k B a rr e t t a n d C e s a r e T i n e l l i C V C 3 I n We rne r D a m m a n d Ho l g e r He r ma n n s，e d i t o r s，P r o c e e d i n g s o f t h e 1 9 t h I n t e r n a t i o n a l C o n f e r e n c e o n C o m p u t e r A i d e d Ve ri fi c a t i o n(C A V，0 7)v o l u m e 4 5 9 0 o f Le c t u r e No t e s i n Co mp u t e r S c i e n c e，S p rin g e r，J u l y 2 0 0 7，P P 2 9 8-3 0 2 1 1 8 S y l v a i n C o n c h o n，E v e l y n e C o n t e j e a n，a n d J o h a n n e s K a n i g Ho me p a g e o f t h e Ah Er g o Th e o r e m P r o v e r h t t p：alt e r g o 1 r i f r J u n e，5，2 01 0 1 1 9 B r u t t o m e s s o，R，C i m a t t i，A，F r a n z e n，A ，G r i g g i o，A，a n d S e b a s t i a n i，RT h e Ma t h SAT 4 S MT s o l v e r I n CAV0 8：Co mp u t e r-Ai de d Ve ri f i c a t i o n Le c t u r e No t e s i n Co mp u t e r S c i e n c e 51 2 3 S p r i n g e r-Ve r J a g，2 0 0 8 P P 2 9 9-3 0 3 2 0 R o b e o B rnt t o me s s o，E d g ar P e k，N a t a s h a S h a r y g i n a，a n d A l i a k s e i Ts i t o v i c h T h e Op e n S MT s o l v e r I n J a v i e r Es p arz a a nd Ru p a k Mu md ar，e d i t o r s，T o o l s a n d A l g o ri t h m s for t h e C o n s t r u c t i o n a n d An a l y s i s o f S y s t e ms，v o l u me 6 01 5，S p rin g e r Be r l i n，He i d e l b e r g，2 0 1 0，P P1 5 0 1 5 3 2 1 RWi l l e，GF e y S WO R D：A S A T l i k e P r o v e r Us i n g Wo r d L e v e l I nfo r ma t i o n I n I n t 1 Co nfe r e n c e o n Ve r y Larg e S c ale I n t e gra t i o n，2 0 0 7 P P 8 8-9 3 1 2 2 J T B o u t o n，DC a mi n h a Bd e O l i v e i r a，D D e h arb e，a n d P Fo n t a i n e Ve r i T：An Op e n T r u s t a b l e a n d E ffic i e n t S MTs o l v e r I n RA S c h mi d t e d i t o r,2 2 n d I n t 1 Co n f Au t o ma t e d De d u c t i o n (C A DE 一 2 2)，2 0 0 9，P P 1 5 1-1 5 6 【2 3 j B Du t e rt r e a n d L e o n a r d 0 d e Mo u r a T h e Y i c e s S MT s o l v e r S y s t e m d e s c rip t i o n r e p o r t h t t p：y i c e s c s 1 s r i c o m t o o l p a p e r p d f,De c 1 0，2 0 0 9 2 4 L e o n a r d o d e Mo u r a a n d N i k o l a j S j?rne r Z 3：A n E ffic i e n t S MT S o l v e r，Co nfe r e n c e o n T o o l s a n d Al g o rit h ms for t h e Co n s t r u c t i o n a n d A n al y s i s o f S y s t e m s(T A C A S)B u d a p e s t，H u n g a ry，2 0 0 8，P P 3 3 7 3 4 0 2 5 C C a d a r，DD u n b ar，a n d D E n te r K l e e：U n a s s i s t e d A n d Au t o ma t i c Ge n e r a t i o n Of Hi g h C o v e r a g e T e s t s F o r Co mp l e x S y s t e ms P r o g r a ms I n US ENI X S y mp o s i u mo n Op e r a t i n g S y s t e ms De s i g n a n d I mp l e me n t a t i o n OS DI 0 8，S a n Di e g o，CA，2 0 0 8，P P 2 0 9 2 2 4 1 2 6 J C l a r k B a r r e t t a n d C e s a r e T i n e l l i C V C 3 I n We rne r D a mm a n d Ho l g e r He rm a n n s，e d i t o r s，P r o c e e d i n g s o f t h e 1 9 t h I n t e r n a t i o n a l C o nfe r e n c e o n C o mp u t e r A i d e d Ve r i fi c a t i o n(C A V，(】7)，v o l u m e 4 5 9 0 o f L e c t u r e No t e s i n C o mpu t e r S c i e n c e，S p ri ng e r,J u l y 2 0 0 7，p p 2 98 3 0 2 2 7 李梦君、李舟军、陈火旺 基于抽象解释理论的程序验证技术 软件学报 1 9(1)，2 0 0 8 2 8 E e n N，S o r e n s o n N A n e x t e n s i b l e S A T s o l v e r P r o c e e d i n g s o f t h e 6 t h I n t e r n a t i o n a l Co nfe r e n c e o u T h e o ry a n d Ap p l i c a t i o n s o f S a t i s f i a bi l i t y Te s t i n g LNCS 2 91 9 S a n t a Ma r g h e r i t a L i g u r e，haly，2 0 0 3：5 02 5 1 8 1 2 9 J B l a u c h e t B，C o u s o t P，C o u s o t R，F e r e t J Ma u b o r g n e L，Mi n e A，Mo n n i a u x D，Ri v a l X A s t a t i c an aly z e r f o r l arg e s a f e t y-c rit i c al s o f t wa r e Pr o c e e d i ng s o f S I GP L AN Co nfe r e n c e o n P r o gra mmi n g L a n g u a g e D e s ig n a n d I m p l e me n t a t i o n(P L I X