【作者】 金仙力；

【导师】 马华东；

【作者基本信息】 北京邮电大学 ， 计算机应用技术， 2008， 博士

【摘要】 在面向服务的架构中,如何根据系统资源环境的变化以及构件的功能和实时性等QoS属性动态组合已有的功能构件以满足应用需求,成为当前此领域的一个研究热点。由于采用非形式化(自然语言)和半形式化(图表)方法描述实时服务系统均存在不精确、歧义的及不易验证等缺陷,而形式化方法能较好地克服上述不足,可充分表述系统的各种特性,并为系统的验证、实现等提供良好的基础。本文提出了一种结合OCL与HTA的实时服务构件(Real-Time ServiceComponent)形式化描述方法:用OCL描述构件的静态语义特征,用HTA描述构件的动态抽象行为;前者为后者的正确性提供属性约束,后者提供前者所描述需求的具体实现,两者语义互补。主要内容及其贡献包括:(1)提出一种基于特征的构件语义描述模型,首先分别给出特征、特征空间和构件特征空间表示模型的定义。接着将构件特征间的各种关联和依赖关系分成自身约束、父子关系约束、显性约束和隐性约束四类,并采用对象约束语言对这些关系进行形式化描述,从而为模型提供了精确的语义支持。面向电子商务的构件特征子树的实例研究及其模型验证和实验结果证明了该模型的正确性与有效性。(2)采用HTA形式化描述实时服务构件的动态抽象行为。给出实时服务构件的HTA模型,系统阐述构件间的各种组装方式及其形式模型,分析构件组装的语法可组合性和语义可组合性问题。采用HTA可层次地构造实时系统集成框架,较高层次的实时服务构件的行为可通过由较低层次的构件组成的HTA来定义。该模型的显著特点是简单容易理解,能在一个统一的框架中表示构件的组装、行为和分析系统性能,适用于不同粒度的实时服务构件集成,有效降低了实时服务系统的复杂度,从而使模型验证工具能够处理更为复杂的服务系统。(3)提出一种基于MLTS的实时服务构件HTA模型组装验证算法。给出(层次)自动机到标号迁移系统的转换过程,在标号迁移系统的扩展模型—多集标号迁移系统基础上,给出其组装算法,利用共享动作是否转换为内部动作来判定模型的组装兼容性。该算法能够有效降低状态空间爆炸给模型实例检测带来的难度,同时利用了MLTS能够描述系统同步、异步动作的特点,不仅可以跟踪构件组装前后的状态变化,而且能够刻画构件的接口行为动作变化,因此,它在基于HTA的实时服务构件模型组装兼容性验证方面具有较强的表达能力。(4)描述一个较简单但又具有典型实时服务系统特征的小额支付视频点播实例应用系统。首先采用自顶向下的方法构建系统,接着采用本文的描述方法对系统级的构件及其组装进行建模、分析和验证,并简单分析了系统的时间属性。更多还原

【Abstract】 How to composite a service from its components is a hot-topic in service-oriented architecture. Since non-formal methods, such as nature languages, and half-formal methods, such as graph, can not specify service-oriented systems exactly, formal methods can do it well and provide the bases for model checking and implementation.This thesis proposes a formal description method of real-time service component which is combined with OCL and HTA. In detail, it describes the static characteristic of the component by using OCL and the dynamic behaviour of the component by using HTA. The OCL description provides the property constraints for the HTA description while the latter description provides the detailed implementation of the former description. The two descriptions are mutually beneficial to each other. The main contributions of this thesis are as follows:(1) This thesis proposes a feature-based semantic description model for component. First, the presentation models of the feature, the feature space and the component feature space are defined respectively. Then, the association and dependency relations among the features of the components are classified into four types: self constraint, paternity constraint, dominant constraint and recessive constraint. The four kinds of constraints are formally described by the object constraint language, which provides an accurate semantic support for such model. Also, it presents a case study based on a component sub-tree of features for e-business. The results of the model checking and experiments in the object constraint language environment prove that this model is correct and valid.(2) This thesis employs the HTA to formally describe the dynamic behaviour of the service component. It defines the HTA model of the real-time service component, systematically describes the various composition manners and formal models between different components, and analyzes the syntax compatibility and semantics compatibility of the component composition. By HTA, the integrated system framework can be constructed hierarchically and the behaviour of the high level real-time service component can be defined by the low level components. The obvious advantage of this model is that it can be easily to be understood and it can specify the component composition and its behaviour in a hierarchical and unified framework, which can be applied to the integration of service component with different granularities. As a result, it can efficiently decrease the complexity of the real-time service system, and make possible for applying the model validation tools for more complex service system.(3) This thesis provides a validation algorithm for the MLTS based HTA model of the real-time service component. It provides conversion process from (hierarchical) automaton to LTS. Based on the extension model of the LTS - the MLTS, we provide the composition algorithm, which determines the composition compatibility according to whether the shared actions are transformed into the internal actions. The proposed algorithm can decrease the difficulties of model instance tests, which is caused by explosion of the state space. Meanwhile, it can not only trace the state variations before and after component composition, but also describe the behavior variations of the component interfaces. Therefore, it is more suitable for the compatibility validation of real-time component composition.(4) This thesis also presents a case study based on a mobile micro-payment for video-on-demand application system. It first builds the system in a top-down manner, and then uses the methods mentioned above to model, analyze and verify the components and their composition in the system level. Also, the timing properties of the system are analysied.更多还原