面向对象软件的形式规格说明技术

本文介绍四种面向对象形式规格语言。Object-Z是Z语言的一种扩充,可用于面向对象软件需求规格的形式说明。为研究软件维护和逆向工程,提出了Z~(++),是Z的另一种扩充,其中引入了过程式描述机制。COLD-K是基于代数规格说明技术的面向对象软件设计语言,是一种核心语言,可设计面向用户的形式规格语言,JOOSL是基于COLD-K和Z语言的一种面向对象设计语言,可用于软件自动化的研究。     

基于Object-Z的形式化验证方法

定理证明是一种形式化验证技术,也是形式化方法的重要组成部分,它能从形式规格说明中推理出应具备的性质与属性,从而可以对规格说明进行形式验证。Obiect-Z是形式规格说明语言Z的面向对象扩充,基于集合论与数理逻辑,具有严密的逻辑性,适合精确地描述大型软件系统,并且可以对其形式规格说明进行推理。本文首先给出了基于Object—Z规格说明的定理证明验证方法,接着用Object-Z描述了一个电梯操作系统的实例,在此基础上给出了其形式规格说明的定理证明方法来进行形式化验证。     

关于Z规格说明语言中模式的剖析

1.引言形式规格说明语言一般是提供一套称为语法域的记号系统和一个称为语义域的对象集合,以及一组精确地定义哪些对象满足哪个规格说明的规则。规格说明是语法域中的句子。它用数学表示法精确地描述了软件系统必须具备的性质。 Z是目前比较流行的一种形式规格说明语言,它以一阶谓词逻     

两种形式语言:RSL与Z的分析比较

RSL(RAISE规格说明语言)和Z是目前广泛应用的软件规格说明语言,本文从软件开发生命周期的角度对两种语言进行了比较,提出了将不同规格说明语言结合形式地描述系统的设想。     

用带时钟变量的线性时态逻辑扩充Object-Z*

Object-Z是形式规格说明语言Z的面向对象扩充,适合描述大型面向对象软件规格说明,但它不能很好地描述连续性实时变量和时间限制。线性时态逻辑能够描述实时系统,但不能很好地处理连续时间关系,也不能很好地模块化描述形式规格说明。首先用时钟变量扩充线性时态逻辑,接着提出了一个方法——用带时钟变量的时态逻辑(LTLC)来扩充Object-Z。用LTLC扩充的Object-Z是一个模块化规格说明语言,是Object-Z语法和语义的最小扩充,其最大优点在于它能方便地描述和验证复杂的实时软件规格说明。     

以XML文档发布关系数据

本文对以XML文档发布关系数据的新技术进行了综述，主要分析了两种发布关系数据到XML文档的语言描述及其实现技术，以及它们的优缺点，一种是利用并扩展SQL的功能来描述这种转换，嵌套的SQL表达式被利用来描述嵌套，扩展的SQL标量及聚集函数被利用来描述XML元素构造，实现将关系数据转换为XML文档，另一种是利用RXL（Relational to XML Transformation Language)语言来定义一个关系数据库的XML视图，该XML视图是虚的，其它应用可再利用XML查询语言XML－QL在虚拟的视图上构造一个查询，抽取XML视图中的数据片断并对抽取的部分进行物化，实现将关系数据转换为XML文档。     

面向服务的软件体系结构的形式化

用形式规格说明语言Z对面向服务这样一种新出现的分布式软件体系结构进行形式化，克服了原先面向服务体系结构的非形式化描述中的限制，为更好地进行面向服务的分布式软件开发提供了指导模型。     

一种基于Z规格说明的测试用例复用机制

测试用例的复用对于提高测试工作的效率极为重要。提出一种测试用例复用机制,减少测试用例对环境的依赖,提高复用的程度。用Z规格说明对用户需求进行描述,实例化后生成测试用例,然后对测试用例进行可复用描述,得到形式统一的可复用测试用例。建立测试用例库系统存储和管理用例,实现多种方式的复用。     

一个Object-Z规格说明的证明责任产生器

定理证明是一种形式化验证技术,也是形式化方法的重要组成部分,它能从形式规格说明中推理出应具备的性质与属性,从而可以对规格说明进行形式验证。Object-Z是形式规格说明语言Z的面向对象扩充,基于集合论与数理逻辑,具有严密的逻辑性,适合于精确地描述大型软件系统,并且可以对其形式规格说明进行推理。设计一个证明责任产生器,从Object-Z形式规格说明出发,按照相关规则自动抽取相应的证明责任,这些证明责任可以直接输入到已有的定理证明器Z/EVES中进行证明之。证明责任产生器起着Object-Z规格说明编辑器与证明器Z/EVES之间的桥梁作用,方便于Object-Z形式规格说明的验证。     

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

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

A Formal Object Approach to the Design of ZML

This paper addresses two issues: how formal object modeling techniques facilitate the XML application development and how XML technology helps formal/graphical software design process. In particular, the paper presents a XML/XSL approach to the development of a web environment for Z family languages (Z/Object-Z/TCOZ). The projection techniques and tools from object-oriented Z (in XML) to UML (in XMI) are developed using XSL Transformations (XSLT). Furthermore, object-oriented Z is used to specify and design the essential functionalities of the web environment and the projection tools to UML. In a sense, the paper also demonstrates a formal object approach to modeling XML applications.     

XQuery语言的形式化语义

XQuery语言用于查询XML文档。目前，该语言规范还是W3C的工作草稿。语言的形式化语义有助于语言的标准化，本文通过重用XML家族语言通用语义构件的方法，形式化建模XQuery语言的语义，语义的描述采用Object—Z规范语言。这种面向对象的语义描述不仅具有简洁性、可扩展性和可组合性，而且有助于规范之间的一致性和协调性。     

一种XML解析器技术的研究与实现

介绍了XML解析的详细过程,设计并实现了一个特定Schema的XML解析器的自动生成工具。该生成工具以一个XML Schema文件作为输入,输出一个JavaCC词法和语法规格说明文件,然后在JavaCC工具的帮助下,生成一个基于特定XML Schema的XML解析器。实验证明,这个生成解析器能够对XML文档进行解析的同时,验证其有效性。     

Z规格说明自动生成器

形式化Z语言采用严格的数学理论可以有效提高软件的可靠性和鲁棒性,但是由于其包含的数学理论使得只有少数人能够熟练应用Z语言进行形式化规格说明书的编写.目前,多数对于Z语言的研究集中在理论阶段,还没有相应的工具支持Z规格说明的自动生成.本文中对于Z规格说明自动生成器的研究有助于降低Z规格说明书的编写难度,降低了形式化开发的难度及成本,对于形式化Z语言的推广具有重要的意义.     

Studying the XML Web: Gathering Statistics from an XML Sample

XML has emerged as the language for exchanging data on the web and has attracted considerable interest both in industry and in academia. Nevertheless, to date, little is known about the XML documents published on the web. This paper presents a comprehensive analysis of a sample of about 200,000 XML documents on the web, and is the first study of its kind. We study the distribution of XML documents across the web in several ways; moreover, we provided a detailed characterization of the structure of real XML documents. Our results provide valuable input to the design of algorithms, tools and systems that use XML in one form or another. An erratum to this article is available at .     

一种改进的XML签名技术的研究及其实现

在深入分析XML签名规范的基础上,针对XML签名规范在解决业务链的多方通信过程中XML敏感数据安全问题的不足,提出了一种改进的XML签名技术,研究实现它们的工作原理。同时设计了基于XML改进签名技术的XMLSchema,并给出了发送方XML整体签名和各接收方分别验证的实现过程,可以很好地满足业务链中一方对所要提供给其它各方的多个XML敏感数据进行整体签名、部分验证的要求,保证了这些数据在多方通信过程中的确认性、完整性和不可否认性。     

XML联合签名

首先分析了目前Web服务架构中XML多方通信业务链的典型应用,并建立了相应的研究模型.基于此模型,提出了联合签名加密技术,以解决传统签名技术在此类应用中存在的重复签名、信息关联不严格等问题.同时,分析了通过现有XML签名规范实现该技术的局限性,进而提出了新的XML联合签名实现方案.最后给出了XML联合签名的语法定义.     

XML技术分析

ＸＭＬ是在ＳＧＭＬ和ＨＴＭＬ基础上发展起来的新一代通用 性的标记语言,是一个一代Ｗｅｂ平台的关键技术。ＸＭＬ包括标记语言定义ＸＭＬ、格式语言定义ＸＳＬ和多边 接语言定义ＸＬＬ三个部分组成,文中对ＸＭＬ的整体技术结构以及三个基本组成部分的技术进行了深入的分析,可作为今后利用ＸＭＬ技术开发Ｗｅｂ应用的参考。