（计算机应用技术专业论文）面向对象msvl语言及其在组合web服务验证中的应用.pdf

摘要 摘要 时序逻辑是一种规范语言，适合于并发系统的规范与验证，已经广泛的应用 于数字电路、软 孛工程等领域的形式化验证中。时序逻辑程序设计语言是时序逻 辑的一个可执行子集，可以将程序的书写、性质描述和验证统一在时序逻辑的框 架中进行。对软硬件系统使用时序逻辑程序设计语言进行建模，对系统期望的性 质采用时序逻辑公式来描述，将模型和性质统一在时序逻辑的框架中，从丽实现 对软硬件系统的形式化验证。 现有的时序逻辑程序设计语言与传统的高级程序设计语言相比，存在形式化 程度过高、缺少指针数据结构和面向对象机制等不足之处，使用这些语言进行程 序设计较为不便。另外，组合w e b 服务的形式化验证是爱前研究的一个热纛，使 用时序逻辑程序设计语言对组合w e b 服务进行建模和验证，能够将模型和性质统 一在时序逻辑的框架中，给形式化验证带来了方便。 本文以框架时序逻辑语言m s v l 为研究对象，提出了指针数据结构的形式纯 方法和实现方案，给出了对象、类和继承等面向对象概念的澎式化定义，并在 m s v l 解释器中实现了指针数据结构和面向对象机制。为了应用m s v l ，研究了 以o w l 。s 为过程描述模型的组合w e b 服务，提出了组合w e b 服务的基于m s v l 的建模方法和验证方法。 本文的主要贡献如下： ( 1 ) 以框架时序逻辑语言m s v l 为研究对象，从逻辑语言的角度出发，提 墨了基于名字常量的指针形式化方法和实现方案；从命令式语言的角度出发，提 出了基于内容变量的指针形式化方法和实现方案。 ( 2 ) 在m s v l 解释器中实现了基于内容变量的指针，使用指针模拟实现了 引用调用的参数传递方式，使用指针实现了原地逆置单链表的程序，并使用解释 器对该程序进行了基于模型检测的形式化验证。 ( 3 ) 对投影时序逻辑进行扩展，基于变量集合的层次化和谓词的分组，给了 对象、类和继承等面向对象概念的形式化定义，并将扩展投影时序逻辑的一个可 执行子集定义为瑟向对象m s v l 。 ( 4 ) 提出了面向对象m s v l 的解释器基本框架和实现方案，使用v i s u a l c + + f l e x b i s o n 实现了该解释器；使用面向对象m s v l 编写数字信号处理程序， 使用面向对象m s v l 的勰释器在仿真模式下挟行该程序，麸丽实现了数字信号处 理的仿真。 ( 5 ) 使用面向对象m s v l 语言描述以o w l s 为过程描述模型的组合w e b 服务，使用命题投影时序逻辑描述期望的性质，使用面向对象m s v l 的解释器在 i i 面向对象m s v l 语言及其在组合w e b 服务验证中的应用 验证模式下执行带性质描述的程序，从而实现了组合w e b 服务基于模型检测的形 式化验证。 关键词：时序逻辑语言指针面向对象组合w e b 服务形式化验证 a b s t r a c ti i i a b s t r a c t t e m p o r a ll o g i ci sas p e c i f i c a t i o nl a n g u a g ew h i c hi ss u i t a b l ef o rs p e c i f i c a t i o na n d v e r i f i c a t i o no fc o n c u r r e n ts y s t e m s ，a n di th a sb e e nw i d e l yu s e di nt h ef o r m a l v e r i f i c a t i o no fd i g i t a lc i r c u i t sa n ds o f t w a r ee n g i n e e r i n g at e m p o r a ll o g i cp r o g r a m m i n g l a n g u a g ei sa l le x e c u t a b l es u b s e to ft e m p o r a ll o g i c ，a n di tp r o v i d e saf r a m e w o r ki n w h i c hw r i t i n go fp r o g r a m s ，p r o p e r t i e so f p r o g r a m s ，a n dv e r i f i c a t i o no fp r o g r a m sc a n a l lb et r e a t e dw i t h i nt e m p o r a ll o g i c t h et e m p o r a ll o g i cp r o g r a m m i n gl a n g u a g e sa r e u s e dt om o d e ls o f - t 、) v a r ea n dh a r d w a r e ，a n dt e m p o r a ll o g i cf o r m u l a sa r eu s e dt od e s c r i b e d e s i r e dp r o p e r t i e s ，t h u st h em o d e la n dp r o p e r t i e sa r eb o t hi nt e m p o r a ll o g i c ，a n dt h e n t h ef o r m a lv e r i f i c a t i o no fs o f t w a r ea n dh a r d w a r ec a nb ep e r f o r m e d c o m p a r e dw i t h t r a d i t i o n a l h i g h l e v e lp r o g r a m m i n gl a n g u a g e s ，t h ee x i s t i n g t e m p o r a ll o g i cp r o g r a m m i n gl a n g u a g e sh a v e s o m e s h o r t a g e s s u c ha sh i g h f o r m a l i z a t i o n ，l a c ko ft h ep o i n t e r sa n do b j e c t o r i e n t e dm e c h a n i s m s ，a n di ti s i n c o n v e n i e n c et op r o g r a mi nt h e s el a n g u a g e s i na d d i t i o n ，t h ef o r m a lv e r i f i c a t i o no f c o m p o s i t ew e bs e r v i c e s i sar e s e a r c hf o c u sa tp r e s e n t t h e t e m p o r a ll o g i c p r o g r a m m i n gl a n g u a g e sc a l lb eu s e dt om o d e la n dv e r i f yc o m p o s i t ew e bs e r v i c e s ，t h u s t h em o d e la n dp r o p e r t i e sa r eb o t hi nt e m p o r a ll o g i cw h i c hb r i n g sc o n v e n i e n c e st ot h e f o r m a lv e r i f i c a t i o n t h i sd i s s e r t a t i o nm a i n l yf o c u s e so nt h ef r a m e dt e m p o r a ll o g i cp r o g r a m m i n g l a n g u a g em s v l ，a n dp r o p o s e st h ef o r m a l i z a t i o na n di m p l e m e n t a t i o no fp o i n t e r s t h e f o r m a ld e f i n i t i o n so fo b j e c t - o r i e n t e dc o n c e p t ss u c ha so b j e c t s ，c l a s s e sa n di n h e r i t a n c e s a r eg i v e n t h e na ni n t e r p r e t e rf o rm s v lh a sb e e nd e v e l o p e dt os u p p o r tp o i n t e r sa n d o b j e c t o r i e n t e dm e c h a n i s m s i no r d e rt oa p p l ym s v l ，t h ec o m p o s i t ew e bs e r v i c e s b a s e do nt h eo w l sp r o c e s sm o d e la r ea n a l y z e d ，a n dam o d e l i n ga n dv e r i f i c a t i o n m e t h o do fc o m p o s i t ew e bs e r v i c e sb a s e do nm s v li sp r o p o s e d t h em a i nc o n t r i b u t i o n so ft 1 1 i sd i s s e r t a t i o na r ea sf o l l o w s ： ( 1 ) t h ef r a m e dt e m p o r a ll o g i cp r o g r a m m i n gl a n g u a g em s v l i sa n a l y z e d ，a n dt h e f o r m a l i z a t i o na n di m p l e m e n t a t i o no fp o i n t e r sb a s e do nn a m ec o n s t a n t sa l ep r o p o s e d f r o mt h ep o i n to fv i e wo fl o g i cl a n g u a g e s ，t h e nt h ef o r m a l i z a t i o na n di m p l e m e n t a t i o no f p o i n t e r sb a s e do nc o n t e n tv a r i a b l e sa r ea l s op r o p o s e df r o mt h ep o i n to fv i e wo f i m p e r a t i v el a n g u a g e s ( 2 ) t h ep o i n t e r sb a s e do nc o n t e n tv a r i a b l e sa r ei m p l e m e n t e di nt h ei n t e r p r e t e rf o r m s v l p o i n t e r sa r eu s e dt os i m u l a t ep a r a m e t e rp a s s i n gb yr e f e r e n c ea n da r eu s e di nt h e p r o g r a mf o ri np l a c er e v e r s a lo fs i n g l yl i n k e dl i s t , a n dt h e nt h ep r o g r a mi sv e r i f i e dv i a m o d e lc h e c k i n gw i t ht h ei n t e r p r e t e r ( 3 ) p r o j e c t i o nt e m p o r a ll o g i ci s e x t e n d e d ，a n dt h e n f o r m a ld e f i n i t i o n so f o b j e c t o r i e n t e dc o n c e p t ss u c ha so b j e c t s ，c l a s s e sa n di n h e r i t a n c e sa l eg i v e nb a s e d o nt h e h i e r a r c h i c a lv a r i a b l es e t sa n dg r o u p i n gp r e d i c a t e s o b j e c t - o r i e n t e dm s v l i sd e f i n e da s a ne x e c u t a b l es u b s e to fe x t e n d e dp r o j e c t i o nt e m p o r a ll o g i c ( 4 ) t h eb a s i cf r a m e w o r ka n dd e s i g np l a no ft h ei n t e r p r e t e rf o ro b j e c t 。o r i e n t e d m s v la r ep r o p o s e d ，a n dt h ei n t e r p r e t e rh a sb e e nd e v e l o p e di nv i s u a lc + + f l e x b i s o n a p r o g r a mf o rd i g i t a ls i g n a lp r o c e s s i n gi sw r i t t e ni no b j e c t o r i e n t e dm s v l ，a n d t h e i n t e r p r e t e rf o ro b j e c t o r i e n t e dm s v li s u s e dt oe x e c u t ei ti ns i m u l a t i o nm o d et o s i m u l a t ed i g i t a ls i g n a lp r o c e s s i n g ( 5 ) o b j e c t o r i e n t e dm s v l i su s e dt om o d e lt h ec o m p o s i t ew e bs e r v i c e sb a s e do n t h eo w l sp r o c e s sm o d e l ，a n dp r o p o s i t i o n a lp r o je c t i o nt e m p o r a ll o g i ci su s e dt o d e s c r i b ed e s i r e dp r o p e r t i e s ，t h u st h ei n t e r p r e t e rf o ro b j e c t - o r i e n t e dm s v l e x e c u t e st h e p r o g r a m sw i t hp r o p e r t i e si nv e r i f i c a t i o nm o d e t ov e r i f yt h ec o m p o s i t ew e bs e r v i c e s v i am o d e lc h e c k i n g k e y w o r d ：t e m p o r a ll o g i cp r o g r a m m i n gl a n g u a g e p o i n t e ro b j e c t o r i e n t e d c o m p o s i t ew e b s e r v i c e sf o r m a lv e r i f i c a t i o n 西安电子科技大学 学位论文独创性( 或创新性) 声明 秉承学校严谨的学风和优良的科学道德，本人声明所呈交的论文是我个人在 导师指导下进行的研究工作及取得的研究成果。尽我所知，除了文中特别加以标 注和致谢中所罗列的内容以外，论文中不包含其他人已经发表或撰写过的研究成 果：也不包含为获得西安电子科技大学或其它教育机构的学位或证书而使用过的 材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中做了明确的说 明并表示了谢意。 申请学位论文与资料若有不实之处，本人承担一切的法律责任。 本人签名：鹄 r 期 西安电子科技大学 关于论文使用授权的说明 本人完全了解西安电子科技大学有关保留和使用学位论文的规定，即：研究 生在校攻读学位期f 日j 论文工作的知识产权单位属西安电子科技大学。学校有权保 留送交论文的复印件，允许查阅和借阅论文；学校可以公布论文的全部或部分内 容，可以允许采用影印、缩印或其它复制手段保存论文。同时本人保证，毕业后 结合学位论文研究课题再攥写的文章一律署名单位为西安电子科技大学。 ( 保密的论文在解密后遵守此规定) 本人签名：至墨二鱼 导师签名： 同期毕r 醐半。 第一章绪论 第一章绪论 1 1 研究背景与意义 形式化方法是借助数学的方法来研究计算机科学中的有关问题。形式化方法 的一种定义为：“用于开发计算机系统的形式化方法是基于数学的用于描述系统性 质的技术。这样的形式化方法提供了一个框架，人们可以在该框架中以系统的方 式刻画、开发和验证系统【l 】。从广义角度，形式化方法是计算机系统开发过程 中分析、设计及实现的系统工程方法。狭义地，形式化方法是规范和验证的方法。 形式化规范是使用具有严格数学定义语法和语义的方法或语言，对系统的期望特 性或者行为进行的精确、简洁描述。形式化验证是基于已建立的形式化规范，对 系统的相关特性进行数学分析和证明。 形式化方法最早可以追溯到2 0 世纪5 0 年代后期，j o h nb a c k u s 和p e t e rn a u r 为了定义a l g o l6 0 语言而设计了b n f ，后来它被作为描述程序设计语言语法的元 语言。在2 0 世纪6 0 年代，面对当时出现的软件危机，f l o y d 、h o a r e 等开展的程 序正确性证明研究推动了形式化方法的发展【2 3 l 。2 0 世纪8 0 年代，在硬件设计领 域形式化方法的工业应用结果，促进了软件形式化开发方法的学术研究和工业应 用，a m i rp n u e l i 提出了反应式系统规范和验证的时序逻辑方法1 4 ，5 1 ，e d m u n dm c l a r k e 和e a l l e ne m e r s o n 等提出了有穷状态并发系统的模型检测方法 6 1 。近十几 年来，形式化方法的研究及其在工业中的应用得到了长足的发展。研究人员建立 了系统设计人员易于理解的规范概念和术语，以及有效应用这些概念和术语的形 式化规范方法及语言，建立了功能更加强大和完善的定理证明和模型检测技术， 并开发出了与之相应的从研究原型到商品化产品的支撑工具和环境【l 】。 定理证吲7 j 采用逻辑公式描述系统及其性质，其中的逻辑由一个具有公理和 推理规则的形式化系统给出，进行定理证明的过程就是应用这些公理和推理规则 来证明系统具有某些性质定理。定理证明的优点是可以处理无限状态的问题，在 证明的过程中，用户可对系统和被证明性质有更多的了解。定理证明的缺点是现 有的方法不能够做到完全自动化，要求用户在交互过程中提供验证中需要的断言， 还有可能要选择证明的策略，这造成的结果是：一个性质定理无法证明，并不能 说明这个性质定理不成立，很可能是证明策略的应用不当。 模型检测【8 】是对有穷状态系统的一种形式化验证方法，是对模型的状态空间 进行穷尽搜索，以确认该系统模型是否具有某些性质，是模拟和测试方法的自然 2面向对象m s v l 语言及其在组合w e b 服务验证中的应用 延伸。模型检测方法的基本过程是：首先给定一个系统s 和应满足的性质p ，然 后将s 翻译为某种形式化模型地再验证mi _ p 是否成立。模型检测的好处在于 它有全自动化的检测过程，并且如果一个性质不满足，它能给出违反该性质的反 例，据此可对系统进行改进。模型检测的缺点在于首先是它所能检测的是有限状 态模型，这样，对于一般软件来讲，需要有一个从任意状态到有限状态的建模过 程，并且这个模型的状态空间会面临组合爆炸的问题。 1 2 时序逻辑程序设计语言 在形式化验证中，需要描述系统的期望性质，这主要通过逻辑公式来表达， 在模型检测中使用的都是时序逻辑。时序逻辑又称时态逻辑、时间逻辑等，最初 产生于哲学和语言学，它是由模态逻辑演变而来的。时序逻辑适合于并发系统的 规范与验证，作为一种规范语言已经广泛地应用于数字电路系统、软件工程等领 域的形式化验证中【9 j 。时序逻辑系统有很多种类，其中最具代表性的是z o h a r m a n n a 和a m i rp n u e l i 提出的线性时序逻辑( l i n e a rt e m p o r a ll o g i c ，l t l ) 、e d m u n d m c l a r k e 和e a l l e ne m e r s o n 提出的计算树逻辑( c o m p u t a t i o nt r e el o g i c ，c t l ) 。 在l t l 中，时间被看成是线性的，每个时刻有且只有一个后继；而在c t l 中， 时间被看成是分支的，即每个当前时刻有多个未来时刻。1 9 8 3 年，为了定量的表 示数字电路的时间特性，b e nm o s z k o w s k i 提出了区间时序逻辑( i n t e r v a lt e m p o r a l l o g i c ，i t l ) ，它基于时间区间而不是时间点，有一个特殊的操作符c h o p ( ：) 来连 接区间。1 9 9 2 年，l e s l i el a m p o r t 创建了操作时序逻辑( t e m p o r a ll o g i co f a c t i o n s ， t l a ) ，用于描述和推理并发反应系统。 a m i rp n u e l i 首先提出了用时序逻辑对程序性质进行形式化验证的思想，基于 此的程序验证技术需要三种不同的语言：编写程序的程序设计语言、描述程序性 质的规范语言、证明程序满足性质的时序逻辑语言。为了简化验证过程，唐稚松 教授首先提出用时序逻辑的一个子集作为一个程序设计语言的思想【l0 1 ，使得程序 的书写、性质描述和验证在同一语言中进行，这样的语言称为“时序逻辑程序设 计语言”。对软硬件系统使用时序逻辑程序设计语言进行建模，对系统期望的性质 采用时序逻辑公式来描述，将模型m 和性质尸统一在时序逻辑的框架中，就可以 对软硬件系统进行形式化验证，它被转化为判定时序逻辑公式m 寸p 是否永真的 问题，采用的方法有定理证明和模型检测。 定理证明试图证明时序逻辑公式m 专p 是一个定理，具体方法是使用时序逻 辑系统的公理和推理规则不断的推导。如果能证明该公式是一个定理，则证明成 功，系统满足期望的性质；如果证明失败，则系统不满足期望的性质。通过分析 第一章绪论 可知，时序逻辑程序如果要进行定理证明，就需要该时序逻辑系统有一个可靠、 完备的公理系统。 模型检测需要判定时序逻辑公式m p 是否有效，它被转化为ma1 尸的可 满足性问题：如果ma1 p 不可满足，则m 寸p 三- 1 ( m k _ 1 尸) 始终为真，模型检 测成功，系统满足期望的性质：如果m 1 尸可满足，模型m 就违反了性质p ， 则系统不满足期望的性质。通过分析可知，时序逻辑程序如果要进行模型检测， 就需要该时序逻辑系统是可判定的。 目前，存在许多时序逻辑程序设计语言，如x y z e t l l ，1 2 , 13 1 、t e m p u r a 1 4 ，15 1 、 f r a m e dt e m p u r a l l 6 1 、t o k i o 【1 7 ，1 引、m e t a t e m f l 9 ，2 0 1 、t l a f 2 1 】等。这些时序逻辑程序 设计语言的逻辑基础各不相同，语法结构和语义各有区别，另外也采用了不同的 形式化验证技术，它们在各种软硬件系统的开发和验证中得到了广泛应用。为了 简便起见，在不产生混淆的情况下，本文以后采用“时序逻辑语言 来特指“时 序逻辑程序设计语言 。 1 2 1x y z e 2 0 世纪8 0 年代初，唐稚松教授以中庸的哲学思想为指导，提出和研制了软 件工程工具系统x y z 。x y z 系统的主要特征是以统一的程序框架表示动态语义 与静态语义，在此基础上将逐步求精、程序规范、验证与速成原型表示在一个平 滑的过渡过程之中。x y z 系统融合了时序逻辑和软件工程【2 2 1 ，它的核心是基于 l t l 的语言族x y z e 。 x y z e 是系列化语言族，其中各子语言分别表示不同的程序设计范型1 2 2 。 x y z e 的最基本特征是以统一的框架，既能表示适应冯诺依曼体系的状态转换机 制的命令式语言，又能表示适应逻辑推理特征的直言式公式语言。前者可在冯- 诺 依曼型机器上有效执行，称为可执行x y z e ；后者用于表示程序规范或抽象描述， 称为抽象x y z e 。 x y z e 的控制结构共三种形式：一种是直接表示状态转换的命令，称为基本 x y z e ；另一种是结构化高级语言的语句形式，称为结构化x 狐；第三种控制 结构是产生式规则的形式，称为产生式规则型x y z e 。 x y z e 中所表示的各种机制包括了各种并发性或不确定性( 通信、共享变量、 实时等) 、不同通信方式( 同步、异步) 、不同类型的可重用模块( 过程、进程、 包块或代理机构及由一并行语言组成的进程) 的机制。 x y z e 是以l 1 l 为基础的，l t l 有高效的判定算法，正好可用于x y z e 的 模型检测，x y z e 的形式化验证即用此算法实现其自动化瞄l 。经过二十多年的发 4 面向对象m s v l 语言及其在组合w e b 服务验证中的应用 展，x y z 系统已经在许多行业得到了广泛的应用。在电信领域，用x y z e 可完 成国际标准语言s d l ( s p e c i f i c a t i o na n dd e s c r i p t i o nl a n g u a g e ) 的验证1 2 引。使用 x y z e 中面向对象的a g e n t 结构，能够表示动画中角色的运动特征及角色之间的 同步协调关系，在统一的逻辑框架下实现了计算机动画中运动对象的行为抽象和 运动的抽象描述【2 4 1 。x y z e 也可用于对多媒体系统进行建模，并可将规范转换为 可执行代码 2 5 , 2 6 】。近些年来，随着w e b 服务的兴起，x y z e 被用于描述工作流【2 7 】、 w e b 服务的重用和组合1 2 引。 1 2 2t e m p u r a t e m p u r a 是b e nm o s z k o w s k i 基于i t l 设计的一种时序逻辑语言。因为i t l 中 包含c h o p ( ；) 操作符，所以能够为t e m p u r a 定义顺序、循环等常见的语句结构。 相对于x y z e 使用非逻辑标号实现语句的跳转而言，t e m p u r a 更接近高级程序设 计语言，更易于人们理解和使用。 在过去的二十年中，t e m p u r a 语言及其工具得到了不断的发展。b e n m o s z k o w s k i 用l i s p ”】编写了第一个解释器，这个解释器是关于最原始的t e m p u r a 的。在1 9 8 4 年后半年，他又改写了这个解释器，使其能够处理双层存储以及多次 扫描的问题。r o g e rh a l e 于1 9 8 5 年在剑桥大学开始了一个c 版本【1 4 j 的解释器。 基于c t e m p u r a 的a n a t e m p u r a 【2 9 j 是一个运用i t l 及其可执行子集t e m p u r a 对系 统进行运行时验证的一个工具。运行时验证技术是使用断言点来检验一个系统是 否满足时间性，安全性以及用i t l 描述的安全性性质。断言点被插入到系统的源 代码中并会在系统的运行中产生一个信息序列，像变量的值和变量变化的轨迹。 i t l 性质对应一个状态( 区间) 序列的集合，运行时验证就是检查验证系统所产 生的集合是不是所要验证性质的序列集合的子集。 在上述的t e m p u r a 语言及其工具中，大部分传统的语言结构都已经定义并实 现了，例如顺序、分支和循环等，另外许多的数据类型，例如整型、数组等也被 实现了。不过，t e m p u r a 语言并没有解决时序逻辑语言中经典的框架问题( f r a m e p r o b l e m ) 3 0 】，不包含指针的实现，也不支持面向对象的程序设计范型。 最初，i t l 和t e m p u r a 一起被用于描述和模拟硬件电路3 1 , 3 2 , 3 3 】，现在已经用 于软件并发系统、语义w 曲服务的描述和验证1 3 4 ，”】。 1 2 - 3m s v l 框架时序逻辑语言m s v l ( m o d e l i n g ，s i m u l a t i o na n dv e r i f i c a t i o nl a n g u a g e ) 3 q 第一章绪论 5 的初级版本是时序逻辑语言f r a m e dt e m p u r a 3 刀。f r a m e dt e m p u r a 是在t e m p u r a 的 基础上发展起来的，它定义了框架操作符f r a m e ，解决了时序逻辑语言中经典的 框架问题，并且增加了投影操作符p r j ，过去时序操作符o 和无穷模型。在f r a m e d t e m p u r a 的基础上，通过引入等待语句和非确定的选择语句，形成了框架时序逻 辑语言m s v l 。 m s v l 的逻辑基础是投影时序逻辑( p r o j e c t i o nt e m p o r a ll o g i c ，p t l ) ，换言 之，m s v l 是p t l 的一个可执行子集【1 6 1 。与t e m p u r a 的逻辑基础i t l 相比较， p t l 增加了投影操作符、过去操作符和无穷模型，表达性更科3 8 】。另外，命题投 影时序逻辑( p r o p o s i t i o n a lp r o j e c t i o nt e m p o r a ll o g i c ，p p t l ) 存在一个可靠和完备 的公理系统，它为m s v l 程序的定理证明奠定了理论基础【3 9 1 。更为重要的是，p p t l 存在一个可判定的算法【3 8 , 4 0 】，它为m s v l 程序的模型检测提供了理论基础，使程 序验证可由计算机自动化实现。 f r a m e dt e m p 嗽解释器的第一个版本出现于1 9 9 6 年【4 ，使用的编程语言是 s i c s t u sp r o l o g 。第二个版本的f r a m e d t e m p u r a 解释器是在v i s u a lc 州f l e x b i s o n 环境中开发的【3 7 】。通过修改该f r a m e dt e m p u r a 解释器，引入等待语句和非确定的 选择语句，形成了m s v l 解释器，最初不包含指针的实现，也不支持面向对象的 程序设计范型。m s v l 解释器可以对m s v l 程序进行仿真执行，也可以进行建模 和验证。其中，仿真是找到程序的一个模型，建模是找到程序的所有模型，验证 即是模型检测程序，判断其是否满足p p t l 定义的期望性质。 目前，p t l 和m s v l 已经用于并发工作流建模【4 2 1 、组合w 曲服务模拟【3 7 1 、 描述和验证【4 引、混合系统的形式化验证【删等领域。 1 2 4 其它语言 受到日本第五代计算机计划的影响，s h i n j ik o n o 对p r o l o g 进行了扩展【1 7 ，1 8 , 4 5 1 ，引入了i t l 公式，定义了一种新的时序逻辑语言t o k i o 。与同样基于i t l 的 t e m p u r a 不同，t o k i o 可以执行一些非确定的i t l 公式【4 引。由于t o k i o 是p r o l o g 的扩展，如果不使用i t l 公式，t o k i o 就退化为p r o l o g ；如果包含i t l 公式，p r o l o g 原有的执行机制将被扩展，用于构造满足时序约束的区间。 m i c h a e lf i s h e r 发明的m e t a t e m 语言是以l t l 为基础的【4 7 1 ，与x y z e 语言 不同，它的程序可以是任意的l t l 公式，执行m e t a t e m 程序即是试图为l 1 l 公式建立一个模型，因此这个过程是不完备 4 6 , 4 8 】。近年来，m e t a t e m 及其后 继语言在分布式人工智能的研究领域得到了关注，用于描述、实现和验证多代理 系统1 1 9 】。 6面向对象m s v l 语言及其在组合w e b 服务验证中的应用 1 9 9 2 年，l e s l i el a m p o r t 定义了操作时序逻辑( t e m p o r a ll o g i co f a c t i o n ，t l a ) 【2 1 1 ，它包含的时序操作符是a l w a y s ( 口) 。与其它时序逻辑都不同的是，l a m p o r t 出于公平性考虑，反对使用下一状态操作符n e x t ( o ) ，转而用p r i m e ( 7 ) 来表示 变量在新状态的值。随后，l a m p o r t 为t l a 加入了一阶逻辑和z f 集合的特性， 改进后的t l a 包含了模块概念，这个新的规范语言被称为t l a + 1 4 9 1 ，可以用于描 述和验证大型的并发系统。t l c 是基于t l a + 的模型检测器【5 0 ，5 1 1 ，同时可以执行 t l a + 的一个子集【5 2 】。目前，t l a 已经在大型并发系统的描述和验证中得到了广 泛的应用【5 0 j 。 迄今为止，上述三种时序逻辑语言没有包含指针的实现，也不支持面向对象 的程序设计范型。 1 3 组合w e b 服务的形式化验证 近年来，随着电子商务的迅速崛起，w 曲应用从局部化发展到全球化，从b 2 c ( b u s i n e s s t o c u s t o m e r ) 发展到b 2 b ( b u s i n e s s t o b u s i n e s s ) ，从集中式发展到分 布式。w e b 服务作为一种新兴的w e b 应用模式，是一个崭新的分布式计算模型， 是w e b 上数据和信息集成的有效机制。从电子商务应用领域来看，复杂的应用连 接和程序代码造成了电子商务应用的高维护代价和更新代价，而w e b 服务正好能 够解决这一问题，成为目前应用环境中最为合理的解决方案【5 引。 面向服务的体系结构( s e r v i c e o r i e n t e da r c h i t e c t u r e ，s o a ) 基于三种角色：服 务提供者、服务注册中心和服务请求者，它们之间的交互涉及发布、查找和绑定 三个基本操作。服务注册中心负责管理和索引服务，提供存储和发现服务的功能； 服务提供者通过在服务注册中心注册发布服务，同时作为服务的宿主控制对服务 的访问；服务请求者则通过在服务注册中心查询已发布的服务描述来发现合适的 服务，并和服务提供者建立绑定以使用服务。 从技术上说，w e b 服务的价值在于服务重用，而重用的目的则是使服务增值。 除了服务本身的重用外，还可以组合不同的w e b 服务以产生不同于各个单一w e b 服务的功能【5 4 1 。在s o a 中，通过组合已有的w e b 服务可以形成更大粒度的w e b 服务，从而提高w e b 服务开发者的开发效率，降低开发成本。例如，常见的旅行 预订服务、订单服务等，都是组合已有的组织内和组织外的服务来实现单个服务 所不能完成的复杂功能。基于组合w e b 服务，形成了一种新的系统构造方式：当 有新的需求到来时，w e b 服务开发者先查找是否有恰好满足需求的服务可供重用， 如果没有，则看是否存在一组服务能够通过协作来完成需求。当没有合适的服务 或者服务的组合满足需求时，进一步分解需求，继续搜索新的可用服列 j 。 第一章绪论 7 组合w e b 服务包含了多种异构w e b 服务，是一个具有新功能的w e b 服务， 具有分布性、异构性、平台无关性等特点。在组合w e b 服务中，可能存在着多个 并发运行的服务，从而加大了该服务的复杂性。同时，单个服务的低可靠性也加 大了组合w e b 服务的低可靠性。如何使得w e b 服务真正进入实用的阶段，使得 w e b 服务实现跨组织、跨管理域的系统集成和自动交互，还面临着诸多的问题； 其中一些问题是在传统的中间件应用中已经解决了的，而另外一些则是新问题， 例如w e b 服务如何组合、能否自动组合以及组合的正确性验证等问题1 5 训。这些问 题已成为影响w e b 服务技术的进一步推广与应用的瓶颈。 为了保证组合w e b 服务的可靠性和安全性，人们通常采用的技术有仿真和测 试。与传统的程序仿真和测试面临的问题一样，尽管这两种技术在保障合成w e b 服务的可靠性方面有着很重要的作用，但它们无法从根本上保障系统的正确性。 组合w e b 服务能否满足企业提出的系统需求和性质，解决该问题的一种较好方法 是对组合w 曲服务进行形式化验证。 组合w 曲服务的形式化验证如同软件系统形式化验证一样，是一个极其困难 的工作，是本世纪计算机科学面临的重大挑战之一。目前，组合w e b 服务的形式 化验证使用的方法有进程代数【5 4 1 、p e t r i 网1 5 6 1 、自动机【5 7 】、时序逻辑【2 8 5 8 】等。在 一般情况下，组合w e b 服务的模型和性质通常采用不同的形式化方法来建立和描 述，这给用户的使用带来了不便。考虑到时序逻辑语言提出的初衷，如果使用时 序逻辑语言描述w e b 服务模型，用时序逻辑公式描述期望的性质，就能够将系统 模型和性质统一在时序逻辑的框架中，这样只使用时序逻辑这一种形式化方法， 与其它形式化验证方法相比具有一定的优势。在时序逻辑框架中，进一步还可以 采用定理证明或模型检测的方法来验证w e b 服务是否满足期望的性质。 1 4 论文的主要工作与组织结构 本文选题来源于国家自然科学基金重点项目“框架时序逻辑程序设计 和面 上项目“组合w e b 服务的建模与验证”，对框架时序逻辑语言m s v l 和组合w e b 服务的形式化验证进行了研究。 根据节1 2 中的分析可知，目前的时序逻辑语言与传统的高级程序设计语言 相比，存在形式化程度过高、缺少指针和面向对象机制等不足之处，造成了这些 语言不够友好，使用不方便的现状。为了改变这种状况，本文以框架时序逻辑语 言m s v l 为对象，研究的重点是为其引入指针数据结构，增加面向对象机制，进 一步探索面向对象m s v l 在组合w e b 服务形式化验证中的应用。本文研究工作 的主要内容如下： 8 面向对象m s v l 语言及其在组合w e b 服务验证中的应用 1 以m s v l 语言为研究对象，提出基于名字常量、基于内容变量的两种指 针形式化方法和实现方案。 2 在m s v l 解释器中实现基于内容变量的指针，使用指针模拟实现了引用 调用的参数传递方式，使用指针实现了原地逆置单链表的程序，并用 m s v l 解释器验证了该程序。 3 对投影时序逻辑进行扩展，给出对象、类和继承等面向对象概念的形式化 定义，并将扩展投影时序逻辑的一个可执行子集定义为面向对象m s v l 。 4 提出面向对象m s v l 解释器的基本框架和实现方案，使用v i s u a l c + + f l e x b i s o n 实现该解释器，并使用面向对象m s v l 和解释器仿真数字 信号处理。 5 使用面向对象m s v l 描述以o w l s 为过程描述模型的组合w e b 服务，使 用p p t l 描述期望的性质，使用面向对象m s v l 的解释器进行模型检测， 验证组合w r e b 服务是否满足期望的性质。 本文由六章组成，具体安排如下： 第一章为绪论部分。首先简要介绍了形式化方法，分析了多种时序逻辑语言 的发展现状，同时表明了组合w e b 服务的形式化验证是国内外研究的热点之一， 最后说明本文的研究重点是为框架时序逻辑语言m s v l 增加指针数据结构和面 向对象机制，并将面向对象m s v l 用于组合w e b 服务的形式化验证。 第二章简单介绍了框架时序逻辑语言m s v l 。首先简要介绍了相关的时序逻 辑语言x y z e 和t e m p u r a 的逻辑基础和语句结构，然后介绍了m s v l 的逻辑基 础- - p t l 的语法和语义，随后给出了m s v l 的语法和