中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
组件语义约束的动态模型检测方法和技术研究
作者: 倪彬
答辩日期: 1998
专业: 计算机软件
授予单位: 中国科学院软件研究所
授予地点: 中国科学院软件研究所
学位: 博士
关键词: 组件 ; 语义约束 ; 模型检查 ; 动态检测 ; 规范 ; 组合软件开发方法
摘要: 随着网络技术的发展,特别是因特网(Internet)的应用,信息系统的规模不断扩大,网络计算(Network Computing)模型成为主流,系统结构逐渐演化为三层客户/服务器结构。如何开发基于网络计算模型和三层结构的大规模应用软件是目前学术界和工业界共同关注的问题。另一方面,对象技术是当今软件工程发展的主流技术。在对象技术的基础上,组合软件开发方法和技术正在成为支持网络计算模型和三层客户/服务器结构的一种热点方法。可复用的组件是组合软件开发方法的基本单元和核心。组件的规范和实现通常依据一定的标准。组件标准提供了支持组件构造的系统结构和API。但是,这些标准目前都采用非形式的方法来刻画组件的语义。组件的高质量是复用和支持分布式计算的关键。为了开发高质量的组件,我们希望对组件的语义进行形式化地描述和验证。在很多情况下,这样的描述和验证是必要的。在组件的制造过程中,往往需要进行多层次的分析、设计和实现。组件语义精确和严格的形式描述,使各层次开发人员对组件语义不会产生理解上的歧义。对组件、调整组件、组合构造以及系统进化的重要依据和正确性检验手段。我们选定Java Beans组件标准作为研究的具体对象。论文工作主要包括下面几个方面的内容:1)设计了一个形式化的规范语言JBDL(Java Beans Description Language)来刻画Java Beans组件--Bean的语义约束。JBDL是基于多类一阶谓词分支时序逻辑的描述语言,包括四种约束。静态约束刻画了Bean的状态空间。行为约束刻画了Bean各个操作应该满足的前后条件。生命期约束刻画了Bean在创建之后,由事件驱动的整个生命期过程中自身状态和行为应该满足的时序性质。协作约束刻画了由低层Bean协作完成高层Bean的操作时应该满足的时序性质。JBDL语言设计的创新特色及所解决的关键技术难点是:(1)单个Bean语义和协作语义的统一约束。(2)用以支持表达Java Beans对象特性的逻辑语言扩充。(3)用以支持统一地、混合地表达Bean状态和操作时序关系的逻辑语言语义上的扩充。JBDL具有较强的表达能力。它全面地描述了Bean的语义约束,统一地约束了单个Bean的语义和协作的语义。为完备地、严格地规范Bean提供了必要条件。对支持组合软件开发过程,特别是组合构造的过程,以及支持组件的复用和提高组件的质量都具有重要的意义。2)为了检测Bean的JBDL规范与其实现的一致性,我们提出了一种基于抽象和符号化的动态模型检查方法。这种方法通过在Bean的运行过程中,动态地建立和演化Bean的检测模型,并对该模型的抽象和符号化表示进行模型检查来完成一致性检测的任务。动态模型检查方法的创新特色及所解决的关键技术难点是:(1)模型的建立、演化以及检测的进行。我们设计了检测点事件机制、检测点选取策略和检测Bean生成方案,使得待检测Bean在运行过程度中需要被检测的时候能够激发检测点事件,也使得根据JBDL规范生成的检测Bean能够在检测点事件驱动下建立、演化检测模型,并进行检测。(2)时序公式的三值语义。由于检测模型是不断演化扩充的,在一个检测点某些时序公式的值按照JBDL的语义虽然是为假,但随着检测的继续,在进一步演化后的检测模型上它们的值可能为真。这就要求我们区分两种情况,a)公式目前不满足,但随着检测模型的演化,公式可能在将来满足;b)公式在从现在开始的检测模型上不可能满足,我们把第一种情况下公式的值定义为不确定(unknown)。这样,时序公式在检测模型下的语义就有三种取值。针对这个问题,我们给出了JBDL时序公式在检测模型下的三值语义解释。(3)空间耗尽问题。由于Bean每个状态占用的空间较多,同时状态数目在动态检测中不断增长,直接在检测模型上进行模型检查很容易空间耗尽。为此,我们提出了一种基于抽象划分的模型检查方法。特别地,抽象是根据要检测的约束而来的,避免了在抽象空间上进行操作和谓词的抽象计算。抽象模型的每个状态只需用布尔向量来表达,同时总的状态数目是有限的。这样,空间耗尽的问题可以通过直接构造抽象模型来有效解决。(4)抽象的保守性。保守性要求检测模型上能够检测到的错误一定可以在抽象模型上检测到。根据时序公式的三值语义,我们证明了抽象方法对正时序公式是保守性的。(5)模型检查算法。利用BDD进行符号化的表示可以提高模型检查的有效性。为了能够在抽象模型上对具有三值语义的时序公式进行模型检查,我们对BDD进行了扩充。使用T~3BDD对抽象模型和约束公式进行符号化的表示。同时给出了基于T~3BDD的模型检查算法,提高了检测的有效性。(6)对并发的影响。Bean通过多线程实现了多层次的并发。我们的动态检测方法给出了同步控制策略,使得检测对Bean的并发活动--特别是同步活动不产生影响或尽量少地产生影响。(7)自动检测。我们的抽象方法和模型检测方法支持检测Bean的自动生成,同时检测点事件包装也可以自动完成,因此检测可以自动地进行。一致性检测的方法是形式化模型检查和软件测试相结合的方法,使得检测可以机械和自动的进行。检测中动态建摸有效地支持了Bean独立发布的特性。时序公式的三值语义适应了检测模型的动态演化。基于抽象的模型检查有效地解决了检测中空间耗尽的问题。保证了正时序公式的保守性。T~3BDD的使用提高了模型检查的效率和有效性。动态检测方法也是基于状态的检测和基于外部行为的检测相结合的方法,支持检测Bean的并发特性和容错特性。它通过检测点机制提供了全局的、外挂的检测方案。也为Bean的测试结果提供了预言。整个方法自动化程度高,具有较好的实用性。3)根据JBDL规范和动态模型检查方法,我们设计和实现了检测的支撑框架和工具--MChecker。检测方法支撑框架是通过Java Beans的类实现的,包括检测点事件支撑框架,T~3BDD支撑框架,模型检查支撑框架和动态检测支撑框架。MChecker的工具包含检测Bean自动生成器和检测点事件包装器。利用MChecker,我们对JavaSoft提供的分布对象计算实例--股票报价监测器,和动画实例--杂耍者进行了研究。实验结果与理论结果完全一致,表明了动态检测在时间和空间上都是有效的。如何在虚拟机的层次上进行检测;如何把检测方法运用于分析、设计等高层次的开发阶段;如何把检测方法应用于其他的组件标准;如何从规范生成测试用例是值得进一步研究的几个方面。
英文摘要: With the development of the network technology, especially the Internet technology, the scale of the information system is becoming larger. The compute model of the information system is becoming network computing model and its architecture is evolving to 3-tier client/server architecture. It is a hot point for industry and academy to research how to develop such large-scale applications. Moreover, object technology is now the mainstream technology in software engineering field. Based on it, component software engineering is the hot point method supporting the development of such kind of application. Reusable Components are the basic and core units of the application. They could be specified and implemented conveniently complied with some component standards. These standards provide the architecture and the APIs to build the components. However, they describe the semantics of components informally. High quality of the components is quite important in component reusing and distributed computing. For building high quality component, we need to describe and verify the component semantics in formal way. Formal description and verification makes the component semantics rigid and strict. They have a great help on understanding components consistently in different levels of development, include analysis, design and implementation. They are also important warranty and approach in component selection, qualification, adaptation, combination and system evolution. Our research is based on Java Beans standard and consists of following contents: 1) We design a formal language - Java Beans Description Language (JBDL) for specifying the semantic constraints of the bean. The JBDL is based on many sorted first order branch time temporal logic. The static constraints describe the legal state space for beans. The behavior constraints describe the pre and post condition of an operation. The lifecycle constraints describe the temporal properties be satisfied by the inner states and the behaviors of the bean in its evolution process. The cooperation constraints describe the temporal properties should be satisfied when the low-level beans cooperate to implement a high level bean's operation. The new ideas and critical problems solved in JBDL designation is: (1) Specify the semantics of a single bean and semantics of cooperation consolidated. (2) Extend on the logic for describing the object features of beans. (3) Extend on the semantics of logic for describing the temporal relations among the operations and states together. The expressiveness of JBDL is quite powerful. It can describe the semantic constraints of the bean roundly, completely and strictly. It consolidates the expression of the semantics of a single bean and the semantic of cooperation. It is quite useful in developing process, especially combination process. It also has great help on component reusability and quality. 2) We contribute a dynamic model checking method for consistency checking between JBDL specification and bean's implementation. The timing model is established and evolved dynamically while the bean running. The model checking method is based on abstracted and symbolized timing model. The new ideas and critical problems solved in this method is: (1) The mechanism for establishing and evolving the timing model and the mechanism for consistency checking. We design and implement the checkpoint event support mechanism, checkpoint selecting policy and the scheme for generating the checker. They support the source firing the checkpoint event when check is required. They also support the checker, generated in terms of JBDL, establishing and evolving the timing model and making model checking. (2) The 3-valued semantics of temporal formulas. The timing model is evolving while checking. A temporal formula may be false at a checkpoint, but be true later under the original semantics of JBDL. Thus if we find the constraints is broken, we wander if it is really broken. We need distinguish two kinds of false: 1) the formula is false currently, but it may be true while the model evolving; 2) the formula is false forever from now on. We called the former as unknown. Therefor, the temporal formulas are 3-valued semantics. We illustrate the 3-valued semantics explanation of JBDL temporal formula on timing model for solving this problem. (3) Space exhausting problem. IN timing model, each state cast large memory and the number of the states is growing fast while the check process going. It is impractical to check the temporal constraints directly on the timing model. We exploit abstraction and symbolization to reduce the size of timing model. The abstraction is in terms of the JBDL temporal formula. The states of the abstract model could be expressed as boolean vectors. Its state numbers are less than the timing model and bounded. The space exhausted problem is solved by constructing the abstract model directly while checking. (4) The conservation of the abstraction. The conservation requires all the inconsistency on the timing model will be detected on the abstract model. In terms of 3-valued semantics of temporal formula, we proof the conservation of abstraction on positive formulas. (5) Model checking algorithm. For improving the model checking efficiency, we use the extension of BDD -- T~3BDD to express the model and formula symbolically. A model checking approach based on T~3BDD is also contributed. (6) Effect on Concurrency. Bean's multi-level concurrency is supported by thread mechanism. By the synchronization policy in our approach, the check has least effect on the concurrency activities of beans. (7) Automation. By our dynamic checking method and model checking method based on abstraction and T~3BDD, both the checker generated and the source wrapped automatically. The consistency checking approach is the combination of model checking method and software testing method. It is a mechanically and automatically approach. The independent delivery of bean is supported by dynamically model construction while checking. The 3-valued semantics of temporal formula is fit for dynamical evolution of the model. The abstraction solves the space-exhausting problem effectively and guarantees the conservation of the positive formulas. T~3BDD improves the checking efficiency. The dynamic checking method is the combination of inner state-based checking and external behavior checking. It supports checking the concurrent and fault tolerant properties. It provides a global and outside solution by checkpoint mechanism. The approach provides the oracles of the testing and quite practical. 3) In terms of JBDL and dynamic model checking approach, we design and implement the check support framework and tool - MChecker. The check support framework is implemented by Java Beans classes, and consists of checkpoint event support framework, T~3BDD support framework, model checking framework and dynamic checking framework. The tool includes the checker automatic generator and checkpoint event wrapper. Several case studies provided by JavaSoft are applied, such as distributed computing demo - Quote Monitor and animation demo - Juggler. The result is consistent with the theoretical result. It shows the dynamic model checking approach is efficient both on space and on time. How to check on the virtual machine level, how to migrate the approach to high level analysis and design development phase, how to bridge the approach to other component standard and how to generate the check case from the specification are worthy for further research.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/6348
Appears in Collections:中科院软件所

Files in This Item:

There are no files associated with this item.


Recommended Citation:
倪彬. 组件语义约束的动态模型检测方法和技术研究[D]. 中国科学院软件研究所. 中国科学院软件研究所. 1998-01-01.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[倪彬]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[倪彬]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2017  中国科学院软件研究所 - Feedback
Powered by CSpace