（计算机应用技术专业论文）论b方法在抽象机库中的实践与应用.pdf

中文摘要 b 方法( 俗称b 语言) 是一种用于描述、设计计算机软件的严格方法，其作用 一直延伸到代码生成，并用伪程序语言来描述需求模型，进行软件设计和实现。 b 建立在z e r m e l o - f r a n k e l 集合理论的基础上，它使用符号表示法( 广义代换) 来表 达状态的转换，使程序及其规格说明处于统一的数学框架之下，减少了出现语义 错误的可能性。这种用形式化的b 方法，借助于b 工具的支持，极大地提高了软件 可靠性和开发的自动化效率。 目前在国外，b 方法在实时、仿真、信息处理和工程等很多领域已经得到了 成功应用，尤其是巴黎地铁列车信号系统，为减少列车间距、提高整个地铁系统 的安全性是b 方法在该系统的显著贡献。但在国内，对b 方法的研究还刚刚起步。 鉴于此，本文着重对b 方法在抽象机库中的应用进行了研究。 本文重点设计了抽象机库，利用规格说明语句对机器进行建模，它可以完成 一些基本的数学计算；其次提出初步精化的思想，这种思想通过数据或操作的变 换实现从抽象程序向具体程序转换的过程；然后采用数学原理，尤其是运用 d i j k s t r a 的最弱前置谓词定理完成规格说明和精化的证明义务，这种定理把程序 开发与正确性证明交替进行的程序验证结合起来，大大提高了程序设计的精确性 和减少了程序设计的周期，在此基础上引入了自动精化算法来完成机器的数据生 成，这种算法可以将抽象的规约逐步精化成一个可执行的程序，程序的正确性依 赖于精化过程中每一步骤的正确性；最后运用分布式原理完成基本的实现。 本文仅仅对b 方法在抽象机库实践中的可行性和有效性进行初步探讨，旨在 为我国在这方面的研究提供一定的参考和借鉴作用，希望b 方法在国内也能得到 广泛、深入的研究和应用。 关键词：形式化方法b 方法抽象机精化证明义务 a b s t r a c t b - m e t h o di sas t r i c tm e t h o dt od e s c r i b ea n dd e s i g nc o m p u t e rs 0 1 c a r e i t s f u n c t i o ne x t e n d st oc o d eg e n e r a t i o n ，a n di tu s e sp s e u d op r o g r a m m i n gt od e s c r i b e m o d u l er e q u i r e m e n ta n dt od e s i g na n di m p l e m e n ts o f t w a r e bi se s t a b l i s h e do n z e r m e l o f r a n k e ls e tt h e o r y i te x p r e s s e ss t a t e st r a n s f e r r i n gb ys i g n a lm e t h o d s ob o t h p r o g r a ma n di t ss p e c i f i c a t i o na r eo nu n i f o r mf r a m e w o r k , w h i c hc a l l r e d u c et h e p o s s i b i l i t yo fs e m a n t i ce r r o r w i t l lt h es u p p o r to rb - t o o l k i t , t h i sf o r m a l i z e db - m e t h o d i m p r o v e ss o f t w a r er e l i a b i l i t ya n da u t o m a t i o ne f f i c i e n c yg r e a t l y a tp r e s e n t ，b m e t h o d sh a v eb e e na p p l i e dt oaw i d er a n g eo ft e c h n i c a la r e a s s u c c e s s f u l l yi no v e r s e a s ，i n c l u d i n gr e a l - t i m e ，s i m u l a t i o n ，i n f o r m a t i o np r o c e s s i n ga n d e n g i n e e r i n g ，e s p e c i a l l yp a r i st u b e - t r a i ns i g n a l i n gs y s t e m ，w h i c hc o n t r i b u t et od e c r e a s e t r a i ns p a c i n ga n di m p r o v es e c u r i t yo ft h ew h o l ei r o ns y s t e m b u t t h es t u d yo n b m e t h o di sj u s tt h ef i r s ts t e pa th o m e s o ，t h i sp a p e rc o n c e n t r a t e so nt h eu s eo f b m e t h o di np r o g r a m m i n g f i r s t l y ，t h i sp a p e rf o c u s e so nd e s i g n i n ga l la b s t r a c tm a c h i n el i b r a r y ，w h i c hu s e s t h es p e c i f i c a t i o ns t a t e m e n tt ob u i l dm a c h i n em o d e lt h a tc a nc o m p l e t es o m eb a s i c m a t h e m a t i c a lc o m p u t a t i o n ；s e c o n d l y ，t h ei d e ao fe l e m e n t a r yr e f i n e m e n ti sp r e s e n t e d h e r e ，w h i c hi m p l e m e n t sat r a n s f o r m a t i o nf r o ma b s t r a c t i n gp r o g r a mt oc o n c r e t i n g p r o g r a mb yt h et r a n s f o r mo fd a t ao rf u n c t i o n ；t h e nu s i n gm a t h e m a t i c a lp r i n c i p l e ， e s p e c i a l l yd i j k s t r a sw e a k e s tp r e c o n d i t i o n st h e o r y ，t oc o m p l e t ep r o o f o fs p e c i f i c a t i o n a n dr e f i n e m e n t d i j k s t r a st h e o r yc o m b i n e sa l t e r n a t i n go fp r o g r a md e v e l o p m e n tw i t h c o r r e c t n e s sp r o o ft op r o g r a m m i n g i ti m p r o v e st h ea c c u r a c ya n dr e d u c e st h ec y c l eo f p r o g r a m m i n g o nt h i s b a s i s ，a u t o m a t i cr e f m e m e n ta l g o r i t h m i si n t r o d u c e dt o c o m p l e t ed a t ag e n e r a t i o n o fm a c h i n ea n di tc a ng r a d u a l l yr e f i n et h ea b s t r a c t s p e c i f i c a t i o nt o ap e r f o r m a b l ep r o c e d u r e t h ep r o g r a mc o r r e c t n e s sd e p e n d so nt h e v a l i d i t yo fe a c hs t e pi nr e f i n e m e n tp r o c e s s ；f i n a l l y ，i m p l e m e n t a t i o ni sc o m p l e t e db y u s i n gd i s t r i b u t e dt h e o r y t h i sp a p e rp r i m l yi n t r o d u c e st h ev a l i d a t i o na n df e a s i b i l i t yo fb m e t h o da t a b s t r a c tm a c h i n el i b r a r yi np r a c t i c e ，a i m i n ga tp r o v i d i n gc e r t a i nr e f e r e n c ea n d s i g n i f i c a n c ei n t h i sf i l e d ，a n dh o p i n gf u r t h e ra n dw i d er e s e a r c hc a nb ed o n ei nt h e f u t u r ei nc h i n a k e yw o r d s ：f o r m a lm e t h o d ，b m e t h o d ，a b s t r a c tm a c h i n e ，r e f i n e m e n t ，p r o o f o b l i g a t i o n s 独创性声明 本人声明所呈交的学位论文是本人在导师指导下进行的研究工作和取得的 研究成果，除了文中特别加以标注和致谢之处外，论文中不包含其他人已经发表 或撰写过的研究成果，也不包含为获得苤鲞盘堂或其他教育机构的学位或证 书而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中 作了明确的说明并表示了谢意。 学位论文作者签名：易卜 签字日期： 力。7 年月2 7 日 学位论文版权使用授权书 本学位论文作者完全了解丞鲞盘堂有关保留、使用学位论文的规定。 特授权苤盗盘堂可以将学位论文的全部或部分内容编入有关数据库进行检 索，并采用影印、缩印或扫描等复制手段保存、汇编以供查阅和借阅。同意学校 向国家有关部门或机构送交论文的复印件和磁盘。 ( 保密的学位论文在解密后适用本授权说明) 学位论文作者签名： 书再 签字同期：如吵年月矽同 聊签缘彦 筝钾飙印年，月歹同 第一章绪论 第一章绪论 1 1 问题的由来和相关背景知识 什么是形式化方法，对形式化方法的研究虽已开展几十年，但并无一个精确 而统一的定义。在1 9 8 9 年的形式化方法会议报告中，有人把形式化方法定义为“利 用严格的数学方法发展、分析、操作计算机系统并以此建立应用软件 f l 】、“运 用数学理论一形式化逻辑来增强软件系统的设计和分析”；r o b i nb 1 0 0 m f i e i d 把形式化方法定义为“建立在严格的数学基础上的软件规范和操作的方法。它包 括根据软件产品的规范、设计和发展阶段来选择数学符号；利用形式规范和形式 验证建立合乎逻辑的理论系统；规范能被证实的方式建立软件模型，1 2 1 。在本文 中我们将形式化方法定义为“应用数学的综合分析技术发展计算机的控制系统”。 我们认为发展形式化技术最主要的原因是在计算机控制系统中根据它的习性能 够建模。 形式化方法有两方面重要的研究内容包括形式规约和形式验证。形式规约 ( f o r m a ls p e c i f i c a t i o n ，也称形式规范或形式化描述) ，它是对程序“做什么” ( w h a tt od o ) 的数学描述，是用具有精确语义的形式语言书写的程序功能描述， 它是设计和编制程序的出发点，也是验证程序是否正确的依据1 3 】。对形式规约通 常要讨论其一致性( 自身无矛盾) 和完备性( 是否完全、无遗漏地刻画所要描述的 对象) 等性质。形式验证( f o r m a lv e r i f i c a t i o n ) 与形式规约之间具有紧密的联 系，就是验证已有的程序( 系统) p ，是否满足其规约( 巾，1 l r ) 的要求( 1 p pi = ( 巾， 1 l r ) ) 。 b 方法和抽象机器符号( a b s t r a c tm a c h i n en o t a t i o n ) 是在牛津大学p r g 的 r d 项目研究中产生出来的 4 1 。该项目由英国国石油公司发起，从1 9 8 5 至f j l 9 8 8 年， 历时三年。b 方法的产生源于8 0 年代早期z 语言的研究。在z 的研发中，j - r a b r i a l 使用了集合论来书写规格说明，这大大激发了人们想用集合论来描述行为属性、 编写计算机程序的兴趣。r j b a c h ，j m m o r r i s ，c c m o r g a n 和其他研究人员曾 做过研究将用于程序的d ij k s t r a 演算【5 1 扩展到规格说明上，牛津大学的扩展版本 直接导致了b 方法中广义替换语言( g s l ) 的产生。g s l 和它的相关演算提供了一 个统一的推演规格说明和程序的数学框架，g s l 在d i j k s t r a 的命令符号中添加了 前置条件的谓词演算。b 的精化符号是z 的精化规则的重新公式化，b 精化规则的 第一章绪论 公式化最先由在牛津大学的d g r ie s ，j p r i n z 和c c m o r g a n 提出。a m n 是b 的规格 说明和设计语言，g s l 是a m n 的基础，在三年的研究实践中，j r a b r i a l 提出了很 多a m n 和b 方法的设想，同时在b p 项目组工作的c c m o r g a n ，p g a r d i n e r 及其他同 事也有很大的贡献，另外由c c m o r g a n 和i h s o r e n s e n 发起的p r g 组中其他项目 成员也有一定的贡献。 简要来说，b 方法( 俗称b 语言) 在形式化方法中属于基于模型的规格说明 符号语言的范畴，它以规格说明语言z 语言的研究为背景，在引入一些面向对象 机制等特点的同时，保留了z 语言的优点。b 语言使用人们熟悉的符号表示法( 广 义代换) 来表达状态的转换，从软件的规格说明到编码的形成是一致的形式描述， 使程序和程序的规格说明处于统一的数学框架之下，以一种基于集合论的符号表 示法来书写，减少了出现语义错误的可能性。这种数学框架是通过谓词变换和扩 展的d ij k s t r a 最弱前置条件提供的。b 语言中的抽象机非常类似于e f f i e l 中的 类的概念，或者a d a 语言的包。 1 2b 方法在国内外的研究现状 1 9 8 8 年以后，关于b 方法的进一步研究包括a m n 、支持工具、b i 具集都从p r g 项目组转移到b p 研究项目的信息技术研究单元( i t r u ) 中。从1 9 8 8 年直至u 1 9 9 2 年， b p 项目组中，i h s o r e n s e n 负责商品化工作，b d s n e i l s o n 负责b i 具集的开发， j - r a b r i a l 是项目的首席顾问，并开发了编译器，成为b 工具集的核心部分。 b - t o o l 在1 9 9 1 年作为b 商品化的程序由b p 发布，在1 9 8 8 至u 1 9 9 2 年间，很多b i i ：具相 继发布，而且具有统一的界面，d s n e ii s o n 、j - r a b r i a l 、i h s o r e n s e n 、 i m c n e i l 、s d a v i e s 和p s c h a r b a c h 为b 工具集的开发做出了重要贡献，b - t o o l k i t 工具集1 9 9 2 发布了a l p h a 测试版【6 】。在这期间，b p 和法国的g e c 达成合作协议，g e c 的f m 设计了一些b - t o o l k i t 组件。 1 9 9 3 年开始，英国的b c o r e 公司继续b 的开发工作，1 9 9 4 年b - c o r e 公司拥有 了b - t o o l 、b - t o o l k i t 和相关语言的知识产权，1 9 9 4 年b - t o o l k i t 正式发布。 b 方法在法国得到进一步的应用，g e ca l s t h o m 和m a t r at r a n s p o r t 用b 方法实 现了铁路安全控制系统，这个应用包括3 0 0 0 行源代码的简单的地铁速度【7 】控制系 统和1 6 0 0 0 行源代码的高级的速度控制系统。 1 9 9 2 年，在d t i 的资助下，成立了b 用户试验项目，该组成员包括b p 研究组、 r a l 和皇家军事学院，这个研究项目旨在支持实例化的安全研究得到b 工业应用的 经验和建议，项目在以下领域得到了应用：病员监视系统、货船调度系统、实时 处理控制、图形标准( g k s 系统) 的规格说明、b a m n 和s p a d e 静态系统的结合。再 第一章绪论 往后，又有两个由欧洲e s s l 资助的应用：一是m a t h m e t h ，包括布尔信息系统和r a l ， 结合了b 和v d m 两种方法来实现财政系统的规格说明；二是m i s t 。另外英国i b m 也 用b a m n 规格化和实现了c i c s 系统的一些模块。 如上所说，b 语言和方法已在很多工业领域得到成功应用，包括实时【8 l 、仿 真t 9 1 、信息处理和工程 1 0 1 等，国内研究b 方法的起步较晚，主要是学习和研究 国外的技术，但国内已有将该方法应用于网络银行系统模型开发的报道【1 1 1 。 1 3 本文研究工作及组织 论文的研究内容及组织结构如下： 第一章：问题的提出，并简要介绍了相关背景知识。 第二章：介绍形式化方法的历史、引起的争议、存在的问题、建议和发展方 向。 第三章：讨论了各种形式化方法之间的联系，对b 、z 和v d m 方法进行了详细 的比较。 第四章：详细介绍b 方法的数字符号、规格说明、操作定义、抽象机器、精 化过程及实现，并用例子说明。 第五章：构造抽象机库，用b 方法给出抽象机库的规格说明，并说明程序的 可验证性。从而得到精化和实现。 第六章：对本文工作进行总结，并指出今后进一步的研究方向。 第二章形式化方法 2 1 形式化方法简介 2 1 1 目的 第二章形式化方法 其目的是：协调政府和工业界的规章和标准1 2 1 ；使软件系统具有较高的可 信度和正确性，并能使系统具有良好的结构、易维护、能较好地满足用户要求； 指导将来研究和发展科技的相关领域。 2 1 2 发展进程 1 9 6 9 1 9 7 2 年c a rh o a r e 撰写了”计算机编程的公理基础( a na x i o m a t i c b a s i sf o rc o m p u t e rp r o g r a m m i n g ) ”和”数据表示的正确性证明”两篇开创性的 论文，并提出了规格说明的概念； 1 9 7 4 1 9 7 5 年b l i s k o w s n z i l l e s 和j g u t t a g 弓 入了”抽象数据类型”的概 念： 1 9 7 6 年e w d i j k s t r a 定义了”最弱前置条件”的概念； 1 9 7 7 年r b u r s t a l l 和j g o g u e n 提出了第一个代数规格说明语言：c l e a r ； 1 9 8 8 年s t a n d f o r d 的s r i 开发了代数规格说明语言o b j 3 ： 1 9 8 0 1 9 8 6 年c j o n e s 定义了v d m 语言，也就是维也纳开发方法； 1 9 8 5 - 1 9 9 2 年牛津大学的程序研究小组开发了z 规格说明语言。随后j - r a b r i a l 开发了称之为b 方法的面向模型的规格说明语言； 1 9 8 5 - - 1 9 9 3 年在m i t 和d i g i t a ls r c 开发了代数规格说明语言l a r c h ： 从1 9 9 1 年开始，面向对象的形式规格说明语言开始发展，例如，o b j e c t z ， v d m + + ，c a f e o b j 等语言； 1 9 9 6 - - 2 0 0 0 年在欧洲c o f i ( c o m m o nf r a m e w o r ki n i t i a t i v e ) 项目资助下开 发”统一”代数规格说明语言c a s l ( c o m m o na l g e b r a i cs p e c i f i c a t i o nl a n g u a g e ) 。 2 2 形式规约 形式规约的方法主要可分为两类：一类是面向模型的方法也称为系统建模 第二章形式化方法 n 4 1 ，该方法通过构造系统的计算模型来刻画系统的不同行为特征；另一类是面 向性质的方法也称为性质描述，该方法通过定义系统必须满足的一些性质来描述 一个系统。 不同的形式规约方法要求不同的形式规约语言，即用于书写形式规约的语言 ( 也称形式化描述语言) ，这些规约语言由于基于不同的数学理论及规约方法，因 而也千差万别，但它们有一个共同的特点，即每种规约语言均由基本成分和构造 成分两部分构成。前者用来描述基本( 原子) 规约，后者把基本部分组合成大规约。 构造成分是形式规约研究和设计的重点，也是衡量规约语言优劣的主要依据。根 据对目标软件系统进行说明的方法可以把规约语言分为以下几类【l 习： ( 1 ) 基于模型的方法。利用一些已知特性的数学抽象( 如域、元组、集合、 序列、包、映射等) 来为目标软件系统的状态特征和行为特征构造模型，但对于 并发没有显式的表示。如v d m 、z 、b 、p a r 等。 ( 2 ) 代数方法。通过联系不同操作间的行为关系而给出操作的隐式定义( 描 述性质) ，而不定义状态，同样它也未给出并发的显式表示，如基于性质的代数 规约语言o b j 、l a r c h 、c l e a r 等。 ( 3 ) 进程代数方法。提供了描述抽象概念并进行进程间联接和推理的方法， 给出并发进程的一个显式模型，女h c s p 、c c s 等。 ( 4 ) 基于交叉语义假设的方法。认为事件并行发生的效果和以任一顺序串 行发生的效果一样，采用逻辑来描述系统的特性，女i t e m p o r a ll o g i c 、u n i t y 、 y i - - c a lc u l u s 等。 ( 5 ) 基于网络的方法。根据网络中的数据流显式地给出系统的并发模型， 包括数据在网中从一个结点流向另一个结点的条件，如p e t r i 网、谓词变换网。 2 3 形式验证 目前常见的形式验证方法主要可分为两类：演绎验证( d e d u c t i v e v e r i f i c a t i o n ) 和模型检测( m o d e lc h e c k i n g ) ( 图2 - 1 ) 。 2 3 1 演绎验证 演绎验证是早期采用的主要验证技术，它基于定理证明( t h e o r e mp r o v i n g ) 的基本思想，采用逻辑公式描述系统及其性质，通过一些公理或推理规则来证明 系统具有某些性质。 第二章形式化方法 图2 - 1 形式验证的主要发展历程 演绎验证的优点是可以使用归纳的方法来处理无限状态的问题，并且证明的 中间步骤使用户对系统和被证明性质有更多的了解。缺点是现有的方法不能够做 到完全自动化，还需与用户交互，要求用户能提供验证中创造性最强部分( 建立 断言等) 的工作。因而演绎证明方法的效率较低，很难用于大系统的验证。 目前主要演绎验证工具有：基于m a n n a p n u e l i 证明系统的s t e p ( s t a n f o r d t h e o r e mp r o v e r ) 、t l v 、机器定理证明器( a c l 2 c o q 、h o l 、i s a b e l l e 、l a r c h 、 n u p r l 、p v s 、t p s 、) 等。 ( 1 ) 组合验证器( c o m b i n a t i o nc h e c k e r s ) - p v s p v s ( p r o t o t y p ev e r i f i c a t i o ns y s t e m ) 是s r i 从8 0 年代中期开始开发的一个 规范和验证系统。它把各种形式验证方法集成在一起，能用于各种复杂的系统的 验证。它使用的规范语言建立在经典的类型高阶逻辑之上，并内置了很多常用的 数据类型。p v s 作为定理证明器支持多种形式的逻辑和推导规则，而作为模型检 验器也支持c t l 模型检验。p v s 的集成特性使得它被成功用于多种困难问题的形式 化和分析，如验证飞行控制系统的算法和结构，硬件和实时系统等。 ( 2 ) 用户指导的自动化推导工具( u s e r - - - g u i d e da u t o m a t i cd e d u c t i o nt o o l s ) - - - - - - - - a c l 2 a c l 2 是k a u f m a n n 等人在1 9 9 4 年开发的定理证明系统，a c l 2 是ac o m p u t a t i o - n a ll o g i cf o ra p p l i c a t i v ec o m m o nl i s p 的缩写。它的前身是b o y e r - - m o o r e 定 理证明器和n q t h m 。a c l 2 既是一种数学逻辑同时又是一个用以形式证明和验证的 形式化工具。它的逻辑是c o m m o nl i s p 的一个子集，而c o m m o nl i s p 本身就是一种 第二章形式化方法 可以运行在多种平台上的高级语言，所以用户可以直接使用a c l 2 编程并执行来测 试计算机系统。另一方面，由于a c l 2 又是一种数学逻辑，因此可以用a c l 2 推理和 证明系统的特性，成为一个定理证明器。 ( 3 ) 证明检验器( p r o o fc h e c k e r s ) 卅o l h o l ( h ig h e ro r d e rl o g ic ) 是一个使用高阶逻辑进行交互式定理证明的环境， 它最显著的特征是高度的可编程性。h o l 的前身是e d i n b u r g hl c f 系统，由g o r d o n 在8 0 年代中期开发，最初是面向硬件验证，将l c f 进行修改后使其支持高阶逻辑 以满足硬件验证的需要。h o l 系统使用m l 语言来实现，它有一个简单但表示能力 很强的核心逻辑，通过扩充库的方式可以提供灵活的证明模式和风格。h o l 目前 已有多个版本，包括h o l 8 8 、h o l 9 0 、h o l 9 8 、p r o o f p o w e r 、i s a b e u e h o l 、h o ll i g h t 等。h o l 目前不仅被广泛应用于硬件验证方面，而且开始应用于软件验证。 ( 4 ) 组合证明器( c o m b i n a t i o np r o v e r s ) - - i s a b e l l e i s a b e l l e 是一个通用的广谱定理证明环境，由p a u l s o n 和n i p k o w 在1 9 8 6 年开始开发的。它提供了一个元逻辑( m e t a l o g i c ) ，目标逻辑( o b j e c tl o g i c ) 的 推理规则可以用元逻辑显式地构造出来。目前i s a b e l l e 可支持一阶逻辑、高阶 逻辑、z f 集合论、m a r t i n - - l o f 类型理论、时序逻辑、计算函数逻辑等主要逻辑 系统。i s a b e l l e 深受l c f 的影响，使用s t a n d a r dm l 来实现系统，因此也具有 l c f 和h o l 的二些特征。 2 3 2 模型检测( 算法验证) 模型检测是对有穷状态系统的一种形式化确认( v a l i d a t i o n ) 方法，它基于状 态搜索( s t a t e - - e x p l o r a t i o n ) 的基本思想，是模拟和测试方法的自然延伸，搜索 的可穷尽性有赖于为系统建立有穷状态的模型，这为建模造成一定的难度，但能 保证搜索过程终止。 模型检测方法的基本思想是通过状态空间搜索来确认系统是否具有某些性 质。即给定一个程序( 系统) p 和规约1 l r ，生成对应于程序( 系统) 模型m ，然后证明 m 1 l r 。即规约公式1 l r 在模型m 中成立，这样就证明了程序( 系统) p 满足规约1 l r 。 模型检测主要适用于有穷状态系统，早期主要用于硬件和协议的验证( 图2 2 ) 。 模型检测的优点是完全自动化并且验证速度快，即便是只给出了部分描述的 系统，通过搜索也可以提供关于已知部分正确性的有用信息。尤其重要的是，在 性质未被满足时，搜索终止可以给出反例，这种信息常常反映了系统设计中的细 微失误，因而对于用户排错有极大的帮助。 第二章形式化方法 r r u eo rc o u r l t e r e x a m p l e 图2 2 模型检测 模型检测方法的一个严重缺陷是“状态爆炸( s t a t ee x p l o s i o n ) 问题”，即 随着所要检测的系统的规模增大，模型检测算法所需的时间空间开销往往呈指 数增长，因而极大限制了其实际使用范围。解决此问题的途径有两个：一是将模 型检测与定理证明相结合，如斯坦福大学的s t e p 时态证明器；二是引入符号模型 检测方法，该方法最初由j r b u t c h 等在1 9 9 2 年提出，采用二元判定图b d d 描述系 统，如s m v 符号模型检测器用于大型软件系统的验证。目前，基于b d d 的符号模型 检测器己可用于状态数目超过1 0 2 0 的硬件电路的验证。此外，用以克服“状态爆 炸”问题的方法还有o n - t h e - f l y 算法、抽象归纳、偏序方法和对称归约、局部状 态空间( 法) 等。 目前的模型检测工具主要有：c o s p a n f o r m a lc h e c k ( b e l l ) 、 删r p h y ( s t a n f o r d ) 、s p i n ( b e l1 ) 、s m v ( c m u ) 、v i s ( b e r k e l e y ) 等。 ( 1 ) 时序逻辑模型检验器s m v 和s p i n s m v ( s y m b o l i cm o d e lv e r i f i e r ) 是m c m i l l a n 在1 9 9 3 年开发的，它使用一种 分支时序逻辑c t l 表示规范，而状态转移系统用o b d d ( o r d e r e db i n a r yd e c i s i o n d i a g r a m ) 表示。它是第一个使用o b d d 的模型检验器，可以比较有效地表示状态转 移系统，因此可以验证工业规模的软件和硬件系统。 s p i n 是贝尔实验室形式方法和验证组在1 9 8 0 年开发的一个面向软件验证的 时序逻辑模型检验器。s p i n 的规范语言是p r o m e l a ，它是一种非确定式语言，类 似于c s p ，并使用线性时序逻辑( l t l ) 表示规范。使用偏序归约方式来减少系统状 态规模。可以有效地描述和验证软件系统的逻辑一致性。 ( 2 ) 行为一致性检验器f o r m a l c h e c k f o r m a l c h e c k 是一个用于硬件验证的商业模型检验器，它的前身是 c o s p a n ( c o o r d i n a t e ds p e c i f i c a t i o na n a l y s i s ) 。作为商业软件，f o r m a l c h e c k 是一个e d a 集成开发环境的组成部分，提供了对v h d l 和v e r i l o g 两种r t l 语言 的支持，形式设计规范是一些查询( q u e r y ) ，每个查询都是一些特性( p r o p e r t y ) 和约束( c o n s t r a i n t ) 的组合。在f o r m a l c h e c k 里，每个特性被定义为一些模板 第二章形式化方法 集( t e m p l a t e ) ，这些模板则用一些自动机表示。因此，通过检验自动机之间 的相互包含关系即可验证设计是否满足规范要求。 2 4 关于形式化方法的讨论 由于形式化方法本身的局限性( 与规范确认和规范解释问题有关) ，形式化 方法的反对者对形式化方法提出了一些质疑。虽然有些意见是片面的，例如在形 式化方法的表达能力与支持工具的能力方面的质疑，但这些反对意见无疑是有益 于形式化方法的研究与广泛的应用的。关于形式化方法的理论问题也影响着实际 系统的开发，尽管早在1 9 7 6 年g e r h a r t 和y e l o w i t z 提出了形式验证程序的失败 之处，但其问题的原因在于其证明过程的不适当，而不是证明本身有问题。许多 反对者认为形式化方法及技术在本质上就是错误的，它不适于软件开发过程。另 外，形式化方法的局限性到底对其应用有多大的影响? 我们认为，形式化方法的 局限性并不影响形式规范本身作为交流和文档工具的价值，而验证精化问题是一 个实质性的问题1 1 6 1 ，我们需要用其他方法来丰富精化的证明，并不是形式化方 法本身有什么错误。 形式化方法是有争议的，其支持者认为形式化方法是对软件开发的一场革 命，而其反对者则认为形式化方法不可能有多大的发展。因为大多数人对形式化 方法并不是很熟悉，所以就很难断定哪一方是正确的，于是就造成了对形式化方 法的一些误解和误用。h a l l0 7 以其研究和应用形式化方法的事实分析了当时对 形式化方法认识的七个误区： ( 1 ) 形式化方法能够保证软件是完全正确的。事实是，形式化方法也是能 够出错的。 ( 2 ) 形式化方法的全部即是程序证明。事实是，形式化方法的全部是规范。 ( 3 ) 形式化方法只适用于s a f e t y c r i t i c a l 系统。事实是，形式规范有助 于任何系统。 ( 4 ) 形式化方法要求具有很高的数学基础。事实是，规范所需的数学是简 单、容易的。 ( 5 ) 形式化方法增加了开发的费用。事实是，从长远的观点来看，形式规 范可以降低开发的费用。 ( 6 ) 形式化方法对用户来说是不可接受的。事实是，形式规范可以帮助用 户理解软件系统。 ( 7 ) 形式化方法未能应用于真正的大型软件的开发中。事实是，形式化方 法每天都应用于工业项目中。 第二章形式化方法 最后h a l l 提出，虽然形式化方法不是“万灵药”，但它是一个有力的工具。 h a l l 还针对上述七个误区，给出了对形式化方法的七点认识。 随着形式化方法的不断研究和发展，对形式化方法亦有了更新的认识，同时 也在软件开发界产生了对形式化方法认识的新的误区。b o w e n 墙】【1 9 1 根据其使用形 式化方法的切身经验及对形式化方法更深入的研究，又给出了另外七个误区，并 以事实解释了误区的形成原因，及误区的错误所在。这七个误区分别是： ( 8 ) 形式化方法延误开发过程。 ( 9 ) 形式化方法缺乏工具。 ( 1 0 ) 形式化方法代替了传统的工程设计方法。 ( 1 1 ) 形式化方法只能应用于软件。 ( 1 2 ) 形式化方法是不必要的。 ( 1 3 ) 形式化方法并没有被支持。 ( 1 4 ) 形式化方法的使用者总是使用形式化方法。 其结论与h a l l 基本相同，即形式化方法并不是“万灵药”，而只是一种用于 改进系统可靠性的方法之一。 对于形式化方法可以说，每一种方法都有其自身的理论背景和应用条件，使 用形式化方法亦要清楚其理论背景和应用条件，若将形式化方法应用于文学创 作，这显然是不合时宜的。形式化方法的使用应限制在可形式化的范围之内。然 而，现实世界中，并不是所有的实体都能够形式化的，这就提出了人工智能中的 基本问题：常识( c o m m o ns e n s e ) 的表示问题( 这一问题也是阻碍人工智能发展 的重要因素之一) ，若能将常识形式化，那么形式化方法的应用范围将能大大地 扩大。在反对形式化方法的意见中，有很多是将形式化方法应用于不适用的情况 而得到的结论，这也是对形式化方法认识之误区和质疑的主要来源。当然，也必 须承认，形式化方法的确有其自身的局限性，这也是任何一种方法所不可避免的。 我们必须深入认识软件开发过程，对软件开发中的非精确、非形式化领域予以同 样的重视，以科学的研究方法来研究形式化方法。 2 5 应用形式化方法的益处 ( 1 ) 形式化说明以逻辑精确性为特色，除去了在非形式化说明中不可避免 的大部分含糊不清的描述，这种精确性为开发人员与用户对需求的一致性理解， 对需求的正确执行提供了更大的可能性。 ( 2 ) 形式化证明通过对需求分析中所描述的系统行为提供逻辑的精确论证， 除去了需求分析中的模糊性和主观性。通过形式化说明和证明实现了系统的重复 第二章形式化方法 分析、一致性分析以及一个较少依赖特定分析者技术和毅力的分析过程。形式化 说明和证明可以通过“裁剪”以适合于给定的项目及技术要求，也就是说能被调 整以满足具体项目的需要。 ( 3 ) 形式化说明和证明能够应用于任何开发阶段，包括目前最需要分析方 法的开发早期，越早发现和确定错误比晚一些发现付出的代价要小的多。例如， 在开发早期，人们通过“裁剪 形式化说明和证明而集中于对重要属性的确认。 ( 4 ) 形式化说明和证明可以被基于计算机的工具所支持，这使得一致性检 查和证明等实现了自动化，提高了系统的可靠性，减少了在分析方面的费用。同 时，这些工具容许证明能够被重复执行而大大增强了分析的重复性m 】。 ( 5 ) 形式化说明和证明弥补了现有的测试方法，通过提供一个精确的形式 化说明而得以获取一个好的测试计划。 ( 6 ) 有事实表明形式化方法能提高系统的质量，这些事实来自于形式化方 法商业上和其它项目上的应用，形式化方法被用来发现需求说明方面的问题以及 提高复杂系统的理解性。 2 6 形式化方法存在的问题 ( 1 ) 由于形式化方法是以计算逻辑、代数理论和软件结构为基础的，因而 形式化方法从本质上是一种较为严格的、灵活性较差的方法，所以形式化方法仍 无法为大多数系统设计者和程序设计者接受【2 1 1 。 ， ( 2 ) 实际规范和实际代码间的差异仍然很大。尽管人们在类型理论、最弱 前提条件、程序变换和程序设计等方面已做出了长期而艰辛的努力，但是程序编 码在很大的程度上仍然是手工完成的。 ( 3 ) 由于形式化方法本身的特点，形式化方法与软件开发过程较难平滑地 结合起来。 2 7 形式化方法的建议 我们提出对形式化方法的几点可能的改进，从而也就确定了形式化方法的一 些发展方向。 ( 1 ) 可重用的规范库及更易接受的符号系统将更有助于形式化方法的研究 与应用。如：形式化方法与结构化方法符号系统的结合，即可将形式化方法的严 密性与结构化方法的结构性结合起来，使得规范更易理解，更易于交流。在这方 面目前也有一些研究成果，但对可重用规范的研究目前较少1 。当然，这一改 第二章形式化方法 进工作并不是短期内可以完成的。 ( 2 ) 改进形式规范的语法、语义定义的质量，从而可以使得形式化方法更 加“稳定”。 ( 3 ) 加强规范语言中对并发控制和容错处理的表达能力，同时也要使精化 技术能够处理这类并发机制和容错。这方面的改进也是长期的研究课题。 ( 4 ) 对于支持形式化方法的工具的可信度问题，一直是困扰形式化方法发 展的重要因素之一，如何度量与提高支持工具的质量亦是一个长期的研究问题。 ( 5 ) b e l l g ；验室的p t d e v a n b u 在第十六届软件工程国际会议中( 1 9 9 4 ) 指出：目前大多数软件系统的容量和复杂度日益增大，需要对软件开发过程中的 各个阶段增强基于知识的描述和维护。基于知识的软件工程( 1 ( b s e ) 研究范式正 是形式化的知识表示和推理机制，支持多种软件开发过程。随着k b s e 的发展， 该方式需要在基于知识的系统构造、维护、运行和理解方面增强描述能力和推理 能力，而描述逻辑可在终止性、形式化语义和高效的推理过程诸方面提供有效的 支持。 从总体来说，若要在以上各方面得以改进，完全依赖于形式化方法研究的前 人结果是不现实的，必须开辟一条新的研究道路，尽力摆脱前人结果的束缚，这 样才有可能超越形式化方法，使得形式化方法得到充分的利用。 另外，形式化方法的研究与发展，也依赖于其他相关学科的发展，如：代数