（计算机应用技术专业论文）构件组装中“特征干扰问题”的时序逻辑检测方法研究.pdf

硕士学位论文 m a s t e r st h e s i s 摘要 当前，基于构件的软件开发方法已经受到越来越多的重视。大多数构件经 过了严格的质量认证，单独运行时功能十分明确，但当来自于不同开发者、不 同开发时间的构件组装在一起时，就会发生很多问题，这些问题被称为“特征 干扰”，而其中那些影响系统正常运行或降低系统运行效率的特征干扰被称为 “特征干扰问题”，这些问题是必须被检测出来并予以解决的。 由于构件可能具有不同的抽象层次和粒度，我们采用了时序逻辑语言 x y z e 作为构件描述语言，这种语言能够描述构件的静态语义和动态执行，并 且能在不同抽象层次上对系统进行形式化描述。在本文，我们主要针对设计阶 段的构件进行描述，并给出其组装中特征干扰问题的检测方法。但是，这种方 法还可以应用于其它阶段和其它抽象层次的构件。 构件间的特征干扰不仅与构件功能有关，还与构件间的组装方式相关，所 以我们提出了一种基于组装方式的特征干扰问题检测方法。这种检测方法分为 两个层次：状态控制层次，即检测构件以某种方式组装时状态之间是否存在不 匹配的问题；结构层次，对多个构件组装后的行为进行检测。 在特征干扰问题的检测中还需要考虑相关问题：状态、事件的相关性问题 和状态可达性问题。相关性问题是为了找出必须共存、可能共存和矛盾的状态、 事件，便于状态控制层次的检测。可达性问题是为了验证我们找出的发生特征 干扰问题的状态是否能由系统的初始状态通过变迁得到，即特征干扰问题是否 一定发生。 文章给出了使用这种方法检测i p 过滤系统和e m a i l 系统中特征干扰问题的 实例，并在附录中以升降机系统为例，说明了使用这种方法检测需求阶段的特 征干扰问题的过程。 关键词：构件；构件组装方式；x y z e 语青：x y z 图；时序逻辑：状态控制 特征干扰 本论文的研究t 作受软件f t 程国家重点实验室开放研究基金( s k l s e 0 4 0 1 8 ) 和湖北省重点科技攻关项 目( 2 0 0 3 a a l 0 1 c 2 6 ) 支持。 i 硕士学位论文 m a s i x g s 1 1 班s i s a b s t r a c t n o w a d a y s ，c o m p o n e n tb a s e ds o f t w a r ed e v e l o p i n gh a sa r o u s e dm a n yc o n c e r n s w h i l es i n g l ec o m p o n e n th a se x p l i c i tf u n c t i o n si nr a n t i m ea f t e rs t r i c t l yq u a l i f i e d ， p r o b l e m sc o m eo u tw i t hc o m p o s e dc o m p o n e n t s ，w h i c hd e v e l o p e db yd i f f e r e n t d e v e l o p e r si nd i f f e r e n tt i m e t h o s ep r o b l e m sa l e s oc a l l e d “f e a t u r ei n t e r a c t i o n a n dt h o s ef e a t u r ei n t e r a c t i o n s ，w h i c hi n f l u e n c et h en o r m a ls y s t e mo p e r a t i o n sa n d d e c r e a s et h es y s t e me f f i c i e n c y , a r ec a l l e d f e a t u r ei n t e r a c t i o np r o b l e m ”，a n ds h o u l d b ec h e c k c do u ta n db er e s o l v e d w eu s et e m p o r a ll o g i cl a n g u a g ex y z ea so u rc o m p o n e n td e s c r i p t i o n l a n g u a g ef o rc o m p o n e n t sm a yh a v ed i f f e r e n ta b s t r a c th i e r a r c h ya n dd i f f e r e n t g r a n u l a r i t y x y z ei sa b l et od e s c r i b et h ed y n a m i cs e m a n t i c sa n ds t a t i co p e r a t i o n s o fc o m p o n e n t ，a n dt of o r m a l l yd e s c r i b es y s t e mi nd i f f e r e n th i e r a r c h y i nt h i sp a p e r ， w em a i n l yf o c u s e do nd e s c r i b i n gc o m p o n e n t si nd e s i g n i n gp h a s e ，a n dp r o p o s i n gt h e a p p r o a c ht od e t e c tt h ef e a t u r ei n t e r a c t i o ni nc o m p o n e n ta s s e m b l e f u r t h e r m o r e ，t h i s a p p r o a c hc a na l s oa p p l yt oc o m p o n e n t si no t h e rp h a s e s t h ef e a t u r ei n t e r a c t i o nb e t w e e nc o m p o n e n t si sn o to n l yr e l a t e dw i t h c o m p o n e n tf u n c t i o n sb u ta l s ow i t hc o m p o n e n ta s s e m b l em o d e a c c o r d i n g t ot h a t ， w ep r o p o s e dac o m p o s i n gm o d eb a s e da p p r o a c ht od e t e c tf e a t u r ei n t e r a c t i o n p r o b l e m s t h e r ea r et w oa s p e c t so f t h i sa p p r o a c h ：s t a t ec o n t r o la s p e c t ，t od e t e c t u n m a t c h e dc o n d i t i o na m o n gs t a t e so f c o m p o n e n t sw h e na s s e m b l e dw i t hc e r t a i n m o d e ；s t r u c t u r ea s p e c t ：t oa n a l y z ec o m p o n e n t sb e h a v i o r sa f t e ra s s e m b l e d i nt h i sp a p e ri m p l e m e n tt h i sa p p r o a c hi ni pf i l t e rs y s t e ma n de m a i ls y s t e mf o r ac a s es t u d y w h a t sm o r e ，w ed e s c r i b eh o wt ou s et h i sa p p r o a c ht od e t e c tf e a t u r e i n t e r a c t i o np r o b l e m si nr e q u i r e m e n tp h a s eb yas a m p l eo f e l e v a t o rs y s t e m k e yw o r d s ：c o m p o n e n t ，c o m p o n e n ta s s e m b l em o d e ，x y z el a n g u a g e ， x y z g r a p h i c ，t e m p o r a ll o g i c ，s t a t ec o n t r o l ，f e a t u r ei n t e r a c t i o n i i 硕士拳住论文 m a 钮卫r st 皿s i s 郑重声明 本人的学位论文是在导师指导下独立撰写的，学位论文没有 剽窃、抄袭、造假等违反学术道德、学术规范和侵权行为，本 人愿意承担由此而产生的法律责任和法律后果，特此郑重声明。 学位论文作者( 签名) ：墙瓠蜗 2 0 0 4 年5 月2 5 日 项士学位论文 m 朝嘎r s t h e s i s 1 1 研究背景 第一章绪论 基于构件的软件开发方法( c o m p o n e n t b a s e dd e v e l o p m e n t ，c b d ) 提供 了一种全新的设计、开发应用软件的方法，软件由许多来源于多种渠道的可 复用构件集成而获得，构件本身可以用不同的程序语言开发、运行于不同的 系统平台上。使用这种技术，例如c o r b a 、c o m ，能够减少软件开发活动中大 量的重复性工作，提高软件生产率，降低开发成本，缩短开发周期。同时， 由于软件构件大都经过严格的质量认证，并在实际运行环境中得到校验。因 此，复用软件构件还有助于改善软件质量，软件的灵活性和标准化程度也能 得到提高3 。 但是，这种开发方法也带来了许多新的问题。例如，一个系统中的多个 构件可能是由不同设计者在不同时间开发的，构件设计和开发是相互独立的。 由此造成的结果是，构件作为一个独立模块运行时十分简单，功能也很明确， 但当它们组装在一起时，却会引发很多问题，这些问题就是“特征干扰” ( f e a t u r ei n t e r a c t i o n ，f i ) 。其中那些破坏其它构件正常操作、影响系统正常运行 的特征干扰就是“特征干扰问题”( f e a t u r ei n t e r a c t i o np r o b l e m s ，f i p ) i b , 7 j o 在过去的几年中，许多人已经逐渐认识到这个问题，并提出了许多避免、 检测和解决特征干扰问题的方法和技术。这些技术分别针对了构件组装的各 个阶段，从需求分析阶段到设计实现阶段、测试阶段。 1 2 特征和特征干扰问题 1 2 1 电信领域中的特征和特征干扰问题 一特征干扰问题最早是b e l l c o r e 针对电信系统提出的删主要表现为 各种服务之间的互相影响，以致无法向用户提供正常的服务或影响服务的质 量。 在电信领域，关于特征和特征干扰到目前还没有统一的概念。一种比较公 认的定义是：“特征”是一个具有增量和选择性质的功能实体，在没有一个 硕士学位论文 m a s l 圈盯s 1 1 删s 基本的功能集合的情况下，不能独立工作。比如：以特征作为基本单元的电 信系统可以表示为如下形式： s = b + f i + f 2 + f 3 + + f n 此表达式的涵义是：一个电信系统是由一个基本的特征集合b 和附加于其上 的若干特征f i ( i 1 ，2 ，n ) 组成的，特征脱离了基本的特征集合b 不 能运行【”。 “特征干扰”，是指发生在某个特征和系统环境、包括和其它的特征以 及同一特征的不同实例之间的交互关系1 9 】。 例如，用户a 定制了源禁止接通( o r i g i n a t i n gc a l ls c r e e n i n g ，o c s ， 允许用户设置禁止呼叫的号码) 服务，不希望接通对用户c 的呼叫；用户b 定制了无条件呼叫转移( c a l lf o r w a r d i n gu n c o n d i t i o n a l l y ，c f u ，任何呼 叫都将无条件地转接到另一台电话) 服务，希望所有呼叫都转接到用户c 当a 呼叫b ，而b 激活了对c 的c f u 服务时，a 的呼叫被接通到c ，用户a 定 制的o c s 服务失效【1 0 1 。如图1 1 所示。 c f ij ： o c s ： 禁i l 呼叫c 图1 1 电信领域特征干扰实例 c 自1 9 8 9 年b o w e n 等人开始，电信领域的研究人员针对特征干扰问题展开了 深入细致的研究，取得了一定的研究成果 1 1 - 2 0 】，为我们研究软件领域的特征干 扰问题提供了参考。但是，软件与电信领域之间的差异决定了在借鉴电信领域 经验与成果的同时，必须重点研究在软件构件开发这一特定背景下的特征干扰 问题。 2 硕士学位论文 b l a s t e r st h e s i s 1 2 2 软件领域的特征及特征干扰问题的定义 在基于构件的软件开发技术中，一般认为，“特征”指的是一个可以与其 它“特征”组合的、可操作的功能单元，也可能仅仅是具有一些非功能性的 属性，比如：容量、安全性、事务以及可靠性 9 1 。 “特征”可以看成是具有一定功能的可复用的构件。在组装的过程中， 不同构件或构件的不同实例间会相互发生关系、相互作用，他们的功能或属 性相互影响，就有可能发生非设计性的冲突，这种冲突被称为“特征干扰”。也 有人倾向于称之为“特征交互”【7 l 。而其中那些扰乱或破坏特征的正常操作、 影响系统正常工作的“特征干扰”，我们称之为“特征干扰问题”，这些问题是 必须检测出来并予以解决的。 现在，人们已经在升降机控制系统、电子邮件系统、数据流系统、基于 规则的系统、w e bs e r v i c e s 等软件系统中发现了类似电信领域的特征干扰问题 1 2 k 7 1 。究其本质，特征干扰问题源自对需求认识不足、对系统演化考虑不够、 设计和实现不当、运行环境资源有限等软件开发中经常遇到的问题。 1 2 3 软件领域特征和特征干扰问题的特点 在基于构件的软件系统中，一个构件可以实现一个或多个特征，一个特 征也可以由一个或多个构件组成，特征可以是一个功能单元，也可能是某个 非功能的属性【6 0 。 在软件领域，特征干扰发生时的表现和发生的原因很不同。它可能出现 在逻辑层次，比如与用户的目的冲突或者需求规约的不一致性；也可能出现 在技术层次，比如特征的实例之间( 同一特征不同实例或者不同特征的实例) 对资源的竞争：甚至出现在企业层次，比如所提供服务的合理性阅题例。 特征干扰可能发生在软件生命周期的任何阶段。从软件复用的角度看， 需求规约、体系结构描述、设计规约、源代码、可运行代码、测试用例都是 有价值、可复用的资源。如果将构件组装看成是对可复用资源的组装，那么 构件组装就不仅仅发生在实现阶段，还可能发生在需求分析、建模、设计、 测试等各个阶段。这种构件及其组装的多态性意味着，前一阶段没有特征干 硕士学住论文 m a s t e k s1 1 m 基i s 扰问题，经过转换后，可能在下一阶段产生新的特征干扰问题1 7 1 。 怎样解决“特征干扰问题”多年来一直是人们研究的热点和难点，为什 么解决“特征干扰问题”这么难呢? 特征作为一种随着系统的发展而增加功 能的单元是我们工作复杂的主要原斟2 8 】： 。 随着系统中特征数目的增加，潜在的特征干扰就会成指数增长。 。 在基于构件的软件开发中，目标系统的生成复用了很多构件，并且随 着系统的发展还会继续复用构件已满足新的需求。每增加一个构件， 就必须包含该构件与系统中已存在的其他构件闽进行交互的具体内 容。因此，为了了解某个构件的行为，研究系统中所有构件的规格说 明是很有必要。然而这一工作非常复杂、工作量也很大，并且对于构 件的要求很高，它必须确保所复用的构件的规格说明非常详细、清楚、 规范。 已经开发的特征常常要依赖于规格说明中的假设或规定，但当新的特 征加入系统中后，这些假设或规定可能不再成立，从而导致特征可能 依赖于相互矛盾的假设。 。 因为每增加一个特征都要考虑到它与系统中已存在的特征的相互作 用，这就需要另外一个新的特征开发者来协调这些相互作用，以至于 我们不能同时增加一系列特征。这主要是由于两个独立的新特征开发 者中任何一方都不会考虑这新增的两个特征在一起怎么相互作用。 由于一个大的系统的生命周期般很长、规模很大，并且在其生存期 的维护过程中，它不断被改造和扩充，这就会给后来的特征开发者理 解该系统带来困难，他们关于系统不全面或错误的理解很有可能使得 特征的规格说明中的假设不正确。 1 2 4 软件系统中的特征干扰问题实例 在软件系统中，存在有许多特征干扰问题的例子。例如： 实例1 ：在基于c o r b a 截取器( i n t e r c e p t o r ) 的分布服务系统中，c o r b a 会按照安装顺序依次激活各个截取器并输入调用请求 2 4 , 2 9 1 。截取器可以中断请 4 硕士学位论文 m a s t e k st h e s i s 求的处理，位于该截取器之后的其它截取器将无法处理该请求。当供应商提供 的描述信息不充分或安装人员对截取器语义不甚了解时，这种顺序执行模式会 导致特征干扰问题的出现。如，认证截取器检验到达请求携带证书的有效性， 证书有效则允许请求继续被处理，否则中断请求的执行，返回一个安全例外给 客户。而日志截取器记录所有到达的请求和返回的应答或例外，不会中断请求 的处理。如果认证截取器先于日志截取器安装，执行，前者将中断那些证书无 效的请求的处理流程，导致后者无法记录该请求，即，日志截取器没有正确履 行“记录所有到达请求”的职责。 实例2 ：w e bs e r v i c e s 体现了一种适合i n t e r a c t 的新型体系风格面向服务 的体系风格，这种风格与电信系统有许多类似之处，因而特征干扰问题也十分 明显【2 4 1 。例如，某用户向太平洋保险公司申请y v l e 服务，使之购买太平洋保 险可享受高达5 0 的优惠，因此，该用户希望今后所有的保险均从太平洋保险 公司购买。该用户某次向中青旅购买云南自助游服务，中青旅负责办理所有相 关事宣，如购机票、订饭店、买保险，在此过程中，中青旅可能向其长期合作 客户平安保险公司购买旅游人身保险，而机票公司可能提供人寿保险公司的飞 行人身保险。因此，该用户的旅游人身保险没有得到预期的优惠，即，用户定 购的v i p 保险服务与自助游服务发生特征干扰问题。 实例3 ：r o b e r tj h a l l 提出了一个简单的e m a i l 系统模型，用户按照e m a i l 消息格式标准从客户端程序发出一个消息，这个消息就通过一个或多个特征处 理构件进行传递，最后被交付给目的接收者的客户端j 。文中描述了十个常见 的e m a i l 特征，及在它们之间存在的2 6 种可能的特征干扰现象。例如，假如用 户a 和用户b 都申请了自动回复的特征，那么只要其中一个用户给对方发送了一 封邮件，就会有回复邮件不断地在两个用户的客户端之间传送。 1 3 特征干扰问题研究现状 特征干扰问题的研究最早集中在电信领域。从1 9 9 2 年开始每隔一两年就 会召开一次f e a t u r ei n t e r a c t i o nw o r k s h o p 国际会议对前阶段特征干扰问题研 硕士学位论文 m a s t e r st h e s i s 究的进展进行总结，并为以后的研究指明方向。从近两年的会议来看，特征 于扰问题的研究主要集中在三个主流方向【3 1 - 3 3 ： 软件工程方法：通过建立一个严格执行的工作流程，将服务开发的过程 规范化、标准化，在很大程度上增加了解决特征干扰问题的可能性，同时也 能极大地限制特征干扰问题的发生。 形式化方法：该方法的特点在于其关注点是特征干扰而不是特征的具体 实现，因此形式化方法仅需考虑特征需求及其规约。 在线检测方法：主要是针对运行时刻的服务而言，是避免特征干扰不良 影响的最后防线。在线检测方法往往包括检测和消除两部分，其最大优势在 于无需对现有系统进行任何改变，能够处理运行时刻网络中的附加功能，并 且允许系统的歼放和扩展。 f 3 4 对1 9 9 7 年至2 0 0 1 年期间电信领域采用软件工程方法、形式化方法和 在线检测方法研究特征干扰问题的工作进行了总结。 2 0 0 1 年1 0 月召开的“f e a t u r ei n t e r a c t i o ni nc o m p o s e ds y s t e m ( f i c s ) ”会 议首次明确提出了研究电信领域以外的其它软件系统中存在的特征干扰问题 1 3 5 。会议在传统的可组装软件系统的特征定义、特征干扰分类以及实例研究 方面取得了一定的成果。 目前，软件领域的特征干扰问题的研究正逐步展开，提出了不少解决方 案。例如，由于大多数的特征干扰都是由于不确定性而产生的，k e f l hp p o m a k i s 和j o a n n em a t l e e 提出一种思路，采用服务和特征的堆栈结构( 或 层次结构) ，通过区分先后次序的方法束解决不确定性问题，从而检测数据库、 操作系统、控制系统等领域中的特征干扰【3 6 , 3 7 】。这种方法能检测数据消耗、 数据修改、资源争夺和控制交互等几方面的特征干扰问题。如图1 2 所示。 m h e i s e l 和j s o u q u i e r e s 提出了一种解决需求阶段特征干扰问题的方 法1 3 “3 9 】。他们将需求表示为公式( 约束) ，如果某些约束的前置条件有交集， 而后序条件相矛盾，则出现特征干扰。这种矛盾的后序条件可能是前嚣条件 通过一次变迁得到的，如图1 3 ( a ) 所示；也有可能是前v 鼍条件通过多次变 迁得到的，如图1 3 ( b ) 所示。 6 e n e m 硕士学位论文 m a s t e r s 啊娜 图1 2 特征堆栈结构 s t a t e i s 妇l c “ 蚴q ( b ) s l 蛳h ( “1 ) 图1 3 需求阶段出现的特征干扰问题 c h r i s t i a n p r e h o f e r 提出了一种使用状态图检测特征干扰的方法【帅】。这种方 法将特征分为完整状态图的基本特征( 包括一个初始状态和一个最终状态) ， 基于变迁的特征( 定义一个局部变迁，不会为状态图添加外部可见的输入变 迁) 和状态扩展特征( 添加了全局状态和外部可见的变迁) 。文章分别对三类 特征间的干扰进行了分析。 1 4 本文的内容安排 在本文，我们提出了一种基于构件组装方式的特征干扰问题的时序逻辑 检测方法。文章具体内容安排如下： 第二章：时序逻辑语言x y z 甩的介绍。这一章主要介绍了时序逻辑语言 x y z e 的特点、语法以及使用x y z e 语言和x y z 图描述构件的方法。由于 本文我们主要是针对代码级的构件给出特征干扰问题的检测方法，所以只给 出了这类构件的描述方法。 第三章：介绍了基于构件组装方式的特征干扰的检测方法。首先简单说 明了构件组装方式对特征干扰问题检测的影响，然后从两个层次：状态控制 层次和结构层次介绍了我们提出的特征干扰问题的检测方法。 7 硕士学住论文 m s 弧st h e $ i s 第四章：介绍了与特征干扰问题的检测相关的两个问题：谓词相关性问 题和状态可达性问题。文中简单说明了研究这两个问题的重要性，并提出了 一些解决方法。 第五章：列举了使用这种方法检测特征干扰问题的实例。以坤过滤系统 为例，说明了状态控制层次的特征干扰问题的检测方法：以e m a i l 系统中的 两个特征为例，说明了结构层次特征干扰问题的检测方法。 第六章：对文中理论方法的总结和今后研究工作的展望。 附录：以升降机系统为例，给出了使用这种方法检测需求阶段特征干扰 问题的方法。 8 硕士学位论文 m a s t e r st h e s i s 2 1 概述 第二章时序逻辑语言x y z e 复用可以发生在软件开发生命周期的不同阶段，例如从需求分析到设计、 测试：复用也可以有不同的粒度。从子程序库到框架，到应用服务。例如， 小粒度的复用如以库形式存放的源代码以及算法、设计模式等的复用已经取 得了比较好的效果。大粒度的复用表现出较高层次的抽象，例如将一个完整 的产品集成到一个复杂系统中。如果将可复用的资源作为构件，则构件具有 不同的抽象层次和粒度。我们在检测特征干扰时，首先要对构件进行描述， 这就需要一种描述语言能够描述各种粒度和抽象层次的构件。 特征干扰存在于软件开发的所有阶段，并且前一阶段没有特征干扰问题 的，可能在下一阶段产生新的特征干扰问题。所以，检测方法如果仅仅针对 某一阶段是不够的，必须在一个统一的框架下，对软件开发的各个阶段进行 检测。 x y z 系统是一种以时序逻辑语言x y z e 为基础的软件工程工具系统 1 4 1 , 4 2 。x y z e 的基本特征是在统一的框架下，既能表示适应冯- 诺依曼体系的 状态转换机制的命令式语言，又能表示适应逻辑推理特征的直言式公式语言， 支持逐步求精和快速原型等软件工程方法，能在不同抽象层次上对系统进行 形式化描述；x y z e 语言与x y z 图能够简单地相互转换，将规范语言描述的 严谨与图形描述的直观性相结合。所以我们采用x y z e 语言作为构件描述语 言。 2 2x y z e 语言简介 2 2 1x y z e 语言的基本概念【4 3 t4 4 1 时序逻辑语言x y z e 是x y z 系统的核心，它既是一个时序逻辑系统， 又是一种程序语言。它的一个重要特点即强调动态语义与静态语义并重。适 应冯诺依曼机器体系的可执行语言的特点是表示自动机的状态转换机制，其 方式是命令式的，语义是动态的：而适于这种模型的规范语言，即h o a r e 逻 9 硕士学位论文 m a s t e r st h e s i s 辑中的p r e 与p o s t 断言( 用时序逻辑表示，即p r e 一p o s t ) ，其语义是静态 的。x y z e 的一个重要的特色就是用一种控制框架将规范的静态语义与可执 行的动态语义统一地表示出来，即表示动态语义与静态语义的两种命令可以 混合在一个程序中出现，能够表示出由完全抽象的规范到完全可有效执行的 程序之蒯的平滑过渡的过程。 静态语义与动态语义的联系还表现在程序的模块结构上。例如，具有流 程图结构的过程与进程是表示动态语义的，而作为面向对象程序设计的具有 封装性( e n c a p s u l a t i o n ) 与继承性( i n h e r i t a n c e ) 的对象模块是面向问题领域 的。其语义是静态的。x y z 系统中提供了一种面向基于通信的计算过程的模 块，称为并行语句进程( p s p ) ，可以将大型程序中静态语义与动态语义联结 成为一个整体。 x y z e 语言属于多种类逻辑系统，变量具有多种类型，可以分为两个层 次：上层为逻辑型，用于表示逻辑公式：下层为非逻辑型，用于表示常见高 级语言中所有在表达式中出现的各种类型，包括整型、字符串型、文件型、 布尔型、浮点型等基本类型，指针、栈、队列等系统类型，数组、记录等结 构化类型，以及扩充的其它类型如集合、枚举集、列表等。 x y z e 语言中还有一种特殊的作为控制类型的名字型，表示为n m ，它 在程序语言中可用来表示各种对象，如变量、常量、新的类型、一段含义完 整的程序模块，如过程、进程、包块或代理机构等；此外还有程序中的路标， 它表示程序执行过程中状态的集合，这种对象被称为标号( 1 a b e l ) ，它没有值， 但本身可以为某些变量的值。在x y z e 语言中有一种特殊的系统变量称为控 制变量，名字为“l b ”，其类型即n m ，它的值即一标号。 需要注意的是在x y z 甩语言中，布尔型是一种非逻辑类型，布尔常量分 别用“$ 1 v r ”与“s f f ”表示，而逻辑类型中的常量“真”与“假”分别表示 为“$ t ”与“$ f ”。 在x y z e 语言是一种逻辑语言，其中语句或命令都是具有逻辑型的合式 公式，在公式中允许出现的一目及二目连接词如下： ( a ) 一阶逻辑中常见的逻辑连接词 1 0 硕士学住论文 m a s 驮st h e s i s 否定词：即“非”，表示成“”，即通常的“一。 合取词：即“与”，表示成“八”。 析取词：即“或”，表示成“$ v ”。 不可兼析取词：即“( 不可同真的) 或”，表示成“$ p ”或“$ 矿。 蕴涵词：即“蕴涵”，表示成“一”，或“一 ”。 等值词：即“等值”? 表示成“= = ”。 全称量词：即“所有”，全称量词符，表示成“$ a ”，即通常的“v ” 存在量词：即“存在”，存在量词符，表示成“$ e ”，即通常的“j ” ( b )将来时时序算子 下一时刻算子：即一目算子“下一时刻”，表示成“$ 0 ”。公式$ o n 在所 指时刻( t 0 ) 为真，当且仅当在所指时刻的下一时刻( 即t + 1 ) 为真。 必然算子：即目算子“从所指时刻起以后所有时刻”，表示成“【】，或 “口”。公式口n 在所指时刻( t o ) 为真，当且仅当从所指时刻起( 包括当 前时刻) 任何时刻，n 均为真。 终于算子：即目算子“从所指时刻起某一时刻”，表示成“”，或“”。 公式n 在所指时刻( t o ) 为真，当且仅当存在所指时刻后某一时刻( t + k 0 ) ( k 表示一非负整数，当k = 0 时，即所指时刻) ，n 必将为真。 直到算子：即二目算子“左式真直到右式真”。表示成“$ u ”。公式m $ u n 在所指时刻( t 0 ) 为真，当且仅当m 从所指时刻起以后一直保持真，直 到n 为真的前一时刻止：并且假定，n 在从所指时刻起以后某一时刻必为真。 除非算子：即二目算子“左式真除非右式真”，表示成“$ w ”。公式m $ w n 与m $ un 只有点不同，其余均相同。这一点是：在公式m $ wn 中不 假定n 从所指时刻起以后某一时刻必为真，也就是在此式中n 可以从所指时 刻起以后所有时刻均取值假。 ( c )过去时时序算子 在x y z e 语言书写算法程序及规范时，一般只用到将来时时序算子：过 去时时序算子用来表示条件及程序性质时其含义比较符合同常语言的习惯， 但实现效率很低。因此只有在特殊情况下描述规范时才允许过去时时序算子 硕士学位论文 m 卯匮r s1 h e s l s 在条件中出现。这里我们只简单给出过去时时序算子的含义和表示。 上一时刻算子：即一目算子“上。时刻”，表示成“( ) ”或“$ 0 ”。 已然算子：即一目算子“过去( 不包括当前时刻) 所有时刻”，表示成【】”， 或“团”。 曾经算子：即一目算子“过去( 不包括当前时刻) 某一时刻”，表示成 “ ”，或“”。 自从算子：即二且算子“自从( s i n c e ) 右式真以来左式真”并假设右式必 曾经为真，表示成“$ s ”。 回溯算子：即二目算子“左式真可一直回溯到( b a c k - t o ) 右式真之后”，表 示成“$ b ”。 2 2 2 状态转换与单元 x y z e 作为时序逻辑语言的一个重要特色，即在于在直言式逻辑公式中 表示出状态转换的机制。在x y z e 中，具有如下形式的等式： $ 0v = e( 2 1 ) 称为状态转换等式。这里v 表示时序变量，e 表示类型与v 相同的表达式，2 1 式的含义是：v 在下一时刻的值等于表达式e 在本时刻的值。 当( 2 。1 ) 式左边变量为特殊的系统变量“l b ”，类型为n m ，恒取执行 标号为值时，其形式为： $ 0 l b = y ( 2 2 ) l b = y ( 2 3 ) 其中，( 2 。2 ) 式含义为“下一时刻的执行标号为y ”，即“转向标号y ”，表示 了常见高级语言中的转语句。( 2 3 ) 式表示“当前执行标号为y ”，也就是常 见高级语言中标号的定义性出现“y ：”。这两种表示状态控制流的公式被称为 控制等式或l b 等式。 利用上述表示状态转换机制的等式，可以表示出x y z e 中的基本命令形 1 2 硕士学位论文 m a s t e r st h e s i s l b = y r j $ 0 l b = z l b = y r 毒 ( q $ d l b = z ) ( 2 4 ) ( 2 5 ) 我们称之为条件元( c o n d i t i o n a le l e m e n t ，简写为c e ) 。其中符号“ ”表示 下一时刻算子$ o 或最终时刻算子：r ，“q ”为一阶逻辑公式，分别称为 c e 的条件部分与动作部分；“j ”是蕴涵词“一”在c e 这一语言层次的 特殊表示形式：标号y 与z 分别称为条件元c e 的定义标号和转出标号。 在x y z e 语言中，除了上面定义的转出标号外，还有一些有特殊含义的 由大写拉丁字母组成的保留字可以作为转出标号。它们的逻辑含义如下： s t o p 或s t o p ：表示该单元执行终止。_name n e x t ：代表它后面第一个条件元的定义标号。 e x i t ：表示它的出现位置后面第一个表示作用域结束的闭方括号“ ”后 砸的第一个定义标号。 r 阻u r n ：表示返回地址。 形式( 2 4 ) 所示的条件元直接定义了程序相邻状态之间的转换关系；形 式( 2 5 ) 所示条件元表示程序抽象规范。两种形式的条件元都是时序逻辑公 式，其语义为此时序逻辑式的语义模型。 单元( u n i t ) 是一个条件元序列，具有如下形式： 【】 a l ，一，a 。】 ，。趴 、 w h e r eb i 吃 其中a ，a ：，k 是条件元：b 八八b - 是一个时序逻辑公式，是对单元的 约束或是某些特别谓词的定义；符号“：”和保留字w h e r e 等同于逻辑联结词 合取。单元是构成x y z e 程序的基本元素。 2 2 3 控制结构 时序逻辑语言的重要特色，即将状态转换机制表示在直言式逻辑公式之 中。这里所谓的状态转换机制，又可以分解为两部分，一部分由条件元中由 1 3 硕士学位论文 m a s t e k st h e s i s 蕴涵式前后两个控制等式( 即l b = y 与$ ol b = z ) 所代表的控制结构，在单元 中，各条件元中的控制结构表示了该单元的控制流：另一部分由条件元中的 一阶公式q 或赋值等式所代表的动作部分，它表示程序进行中的每一步动作， 或者更具体地说即变量值的改变流程。x y z e 语言提供了三种不同的控制结 构形式，每个单元中只允许出现一种控制形式，但包含不同控制结构的单元 所组成的过程或进程等模块可以组成统一的程序。这三种控制结构在不同应 用方面各有所长。( 2 4 ) 、( 2 5 ) 式表示的是有穷状态自动机状态转换的控制 结构，除此之外，还有结构化高级语言语句形式的控制结构和产生式规则形 式的控制结构。 2 3 使用x y z e 描述构件 构件可以分为不同粒度和抽象层次，对不同构件描述方法不同。时序逻 辑语言x y z e 不仅能够描述程序、算法，还能描述软件构架【4 5 1 、需求【4 6 】等。 本文我们主要是针对代码级构件进行分柝，所以只给出代码级构件的描述， 可以由以下几部分组成： ( 1 ) 数据结构，具体描述如下： t y p e 【s t r u c t n a m e r e c o r d ( f i e l d l i s t ) 其中s t r u c tn a m e 表示数据结构的名称，结构定义与高级语言中的r e c o r d 相 似。但是，由于x y z e 语言数据类型是基于p a s c a l 的，它所提供的数据类 型是面向软件编码和实现的，而我们在对特征干扰问题进行检测时要求有较 高的抽象。把握构件的本质，简明地表达数据和其间的复杂关系。所以我们 需要对x y z e 语言的数据结构进行扩充，将幂集类型、笛卡儿积类型、序列、 包、关系、函数和模式都引入作为数据类型。同时允许用户运用方括号定义 基本数据类型，而不关心其内部结构【4 5 】。 例如，我们考虑i p 过滤系统中规则的描述，需要数据结构表达i p 地址 和端口，则可以简明定义如下： 1 4 硕士学位论文 m a s i f r st h e s i s t y p e 【 【i p a d d r e s s 】 i t 定义 p a d d r c s s 为基本数据类型表示i p 地址 p o r t 1 1 定- 义p o r t 为基本数据类型，表示目标端口 】 ( 2 ) 过程计算，描述如下。 p r o c p r o c 二n a m e ( p a r a m e t e r s ) = s a t e m e n t s 】 w h e r e ( c o n s t r a i n t ) 其中p r o en a m e 表示过程t 进程名( 对于函数，还需要定义返回直的类型) ， s t a t e m e n t s 为实现该过程的语句序列，在此表示e l e m e n t s ( 条件元) 序列， e l e m e n t s 的定义为： e l e m e n t s = l b = d e f i n i t i o n a l l a b e l c o n d i t i o nj $ d ( 变量序列) = ( 值序列) $ o l b = f o r w a r d l a b e l 】 或e l e m e n t s = 【l b = d e f i n i t i o n a l l a b e l c o n d i t i o nj o ( 一阶公式 l b = f o r w a r d l a b e l ) 】 ( 3 ) 包块，是由一组运算围绕一数据结构封装而成的模块，其描述如下： p a c k p a c k n a m e = 【d a 敬s t r u c m r e ；c o m p i $ v $ v c o m p i 】 w h e r e ( c o n s t r a i n t ) 其中p a c kn a m e 表示包块名，此处“s v $ v ”可以写成“v v ”。 ( 4 ) 选择结构，即表示不确定性的命令( 语句) ，描述如下： l b = y r j ! l 【c d 耐il e x e a c t l 一，c o n d k 睁e x e a c t i 】 或l b = y r $ o ( c o n d l e x e a c t l s v $ v c o n d e x e a c t ) 其中，c o n d i 与e x e a c t i ( i 一1 ，k ) 分另表示条件与动作，都是一阶逻辑 公式，这里的符号“i ”应理解为“ ”。这两个式子的含义是：在前置条件 r 满足的情况下，当外界环境中出现事件c o n d i 时，执行动作e x e a e t i 。 1 5 硕士学位论文 m a s t e k st h e s i s 2 4x y z 图 x y z 图是状态图同p e t r i 网的结合。它能够表示抽象的规范 ( s p e c i f i c a t i o n ) ，也能表示具体的可实现的过程。使用x y z j c f c 还能够实现 x y z 图和x y z e 程序之间自动地相互转换。利用x y z 图的基本图元可以将 五种形式的条件元与一定的图形对应起来： 基本条件元：l b = y a p j $ d l b = z ，对应的x y z 图如图2 1 ( a ) 所示。 行为描述：l b = y p j ( q l b = z ) ，对应的x y z 图如图2 1 所示。 等待语句：上b = y a p j $ d ( q a l b = y ) $ s u ( s a l b = z ) ，对应的x y z 图如图2 1 ( c ) 所示。 并行结构：l b = y p j $ d ( aa p 2 p i ) w h e r ei i 【p i ，p 2 ，p t 】 对应的x y z 图如图2 1 ( d ) 所示。 选择结构：l b = y a 尸j ! ! 【s i $ d o $ d l b ，= = ， ，s 。i $ d qa $ o l b 。= z 。】 对应的x y z 图如图2 1 ( c ) 所示。 e 一旦g 兮寸目一o 1 6 硕士学位论文 m a s t e r st h e s i s 面 图2 1 条件元与x y z 图的对应 由于各条件元之间是合取关系，只要将程序中所有条件元所对应的图形 组合在一起，就得到了程序所对应的x y z 图。 2 5 本章小结 本章首先介绍了时序逻辑语言x y z e ，包括x y z e 语言的特性、常见连 接词、状态转换与单元、控制结构等。然后介绍了使用x y z e 语言描述代码 级构件的方法。最后简单介绍了使用x y z 图描述条件元的方法。 我们采用x y z e 语言和x y z 图