基于Object-Z的Web组件形式化建模

Web组件技术是一种解决Web服务再利用和扩展问题的方法。Objcct Z是Z语言的面向对象补充，它们是基于一阶谓词逻辑和集合论的形式规格说明语言。用形式规格说明语言Object Z对Web组件建模，能够保证Web组件在异构平台、松散藕合、封装等特性下的一致性和精确性。以Web组件为研究对象，以Object Z为形式规格说明语言建立模型，提出了Web组件及其组合的建模方法。该方法对包括接口、组件操作在内的Wcb组件静态行为进行了建模，定义了接口、消息的匹配方法。构造了基本组合结构的形式化框架，利用组件的逻辑分解方法将该框架应用于复杂的组件组合过程，并提出了需求驱动的组件组合方法。在此基础上，结合实例对组件的交互、组合进行了建模分析。

Formal Model of Web Component Based on Object-Z Specification

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.