Research On The Formalization Of Semantic Features And Behavior Composition For Real-Time Service Component

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.