关键词: Web组件，组件组合，Object Z，定理证明

Abstract: Web component is a solution to reuse and extend Web service. Object-Z is the object oriented complement of the language Z which is based on set theorem and first order predicate logic. Modeling with a formal specification language Object Z could ensure the consistency and accuracy of the Web component which work in heterogeneous, loose coupling and encapsulation conditions. hhis thesis concentrates on studying Web component based on Object Z,and poses the related approach to modeling Web component and its compositions. The approach models static behaviors of component including interface and operation, defines the matching methods between interface and message, builds the formal frame of basic composite structure, applies the frame with component decomposition, and describes the composite method based on the rectuirements. On this basis, a case study for demonstrating our proposed approach, modeling the interactions and compositions is shown.

Key words: Web component, Component composition, Object Z, Theorem proving