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

Formal Model of Web Component Based on Object-Z Specification

作　　者：严吉皞[1] 缪淮扣[2] 

机构地区：[1]上海大学计算机工程与科学学院,上海200072 [2]上海市计算机软件评测重点实验室,上海201112

出　　处：《计算机科学》2012年第B06期383-388,407,共7页Computer Science

基　　金：国家自然科学基金项目(60970007);上海市科学技术委员会(10510704900);上海市重点学科建设项目(J50103)资助

摘　　要：Web组件技术是一种解决Web服务再利用和扩展问题的方法。Object-Z是Z语言的面向对象补充,它们是基于一阶谓词逻辑和集合论的形式规格说明语言。用形式规格说明语言Object-Z对Web组件建模,能够保证Web组件在异构平台、松散耦合、封装等特性下的一致性和精确性。以Web组件为研究对象,以Object-Z为形式规格说明语言建立模型,提出了Web组件及其组合的建模方法。该方法对包括接口、组件操作在内的Web组件静态行为进行了建模,定义了接口、消息的匹配方法。构造了基本组合结构的形式化框架,利用组件的逻辑分解方法将该框架应用于复杂的组件组合过程,并提出了需求驱动的组件组合方法。在此基础上,结合实例对组件的交互、组合进行了建模分析。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.This 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 requirements.On this basis,a case study for demonstrating our proposed approach,modeling the interactions and compositions is shown.

关 键 词：WEB组件 组件组合 OBJECT-Z 定理证明 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]