【作者】 孙军梅；

【导师】 缪淮扣；

【作者基本信息】 上海大学 ， 控制理论与控制工程， 2008， 博士

【摘要】 网络技术的飞速发展,给人们的工作、生活方式带来了极大的变化,人们对网络的需求与依赖也越来越明显,对Web软件的需求也越来越多,例如电子政(商)务等。Web环境的开放性、分布性等特点使得Web软件开发方法不同于传统的软件开发方法。目前还没有很完善的Web软件开发方法。开发Web软件的方法基本上还是沿用传统的软件开发方法。传统的软件系统被开发为封闭的系统。虽然其构件可以来自外部,但合并到系统运行时,它们就在系统设计者控制之下。根据这一基本思想所开发的软件都具有这一特点。但在网络上,系统可能没有这样的集中控制,它们只在协议、地址和站点的交互上有统一标准,只在需要时动态绑定,所以需要一种允许用户利用网上自治的资源实现他们自己的组合,并能自动或人机互动进行服务的动态组装方法。基于Web的软件系统的建立和维护需要软件工程方法的进一步支持。为降低Web软件系统的设计开发难度,已经研究提出了基于软件体系结构、模型驱动等设计方法。这些方法的核心是模型的构造、模型的转换和精化。但目前软件体系结构以及模型驱动体系结构的建模语言主要是以UML作为标准建模语言。UML具有可视化、容易理解等特点,但缺乏严格的语义,而模型的转换必须建立在严格语义的基础上。本文提出基于形式方法面向服务的Web软件开发方法,围绕此问题分别从形式方法在面向服务构件的软件开发中的作用出发,对面向服务的软件体系结构的形式建模、基于模型的服务组合验证、基于形式本体的服务构件的发现、基于角色的设计模式形式建模及演化进行了研究。提出了基于面向服务软件体系结构的自顶向下的服务构件的组装理论。鉴于目前的面向服务软件体系结构的表示主要采用W3C给出的非形式化图形表示,不能精确表示软件结构的内涵,基于面向服务软件体系结构的服务构件自动化组装存在一定的难度。本文用形式规格说明语言Z对面向服务的软件体系结构进行了形式化,并提出把面向服务的软件体系结构作为一种风格来研究。面向服务的软件体系结构风格的形式化可以更为准确和方便地在体系结构的层次上进行交流。对不同的体系结构风格进行形式化描述,有利于系统的形式化验证和不同风格之间的比较。本文还分析定义了面向服务这样一种新出现的分布式软件体系结构风格的一些性质并给出了证明,并据此风格给出了一个应用实例,并对实例的活性进行了分析。服务组合是面向服务的Web软件开发的关键技术之一。如何有效地验证组合服务的功能及性能是服务组合研究中必须要解决的关键问题。为了能够自动地验证组合服务的各种属性,如组合服务是否能实现用户需求的功能,以及组合服务在运行过程中是否会出现用户不期望的行为,本文使用标签状态自动机建立组合服务的形式模型,将与用户的功能需求及期望的行为相关的性质表示为CTL公式,然后用形式验证工具SMV对服务组合进行了形式化验证。发现服务是面向服务Web软件开发中的另一关键技术。本文通过建立一个领域本体来扩展用户查询端查询的语义精确性,这种方法一方面可以提高服务构件的查准率和查全率。另一个好处是克服了其它基于语义的方法在实际服务查询中的可操作性方面的难度。我们的方法可以很好地利用已有的搜索引擎来达到对服务查询效能方面的提高,本文给出了一个服务搜索引擎的原型系统。体系结构反映系统的本质,由一些抽象的概念,以及概念间的关系来表示。但体系结构过于空泛,缺乏延伸性。设计模式正好可以弥补体系结构的这一缺陷,通过对体系结构的分析、分解,寻找和我们要解决问题匹配的模式可以使抽象的体系结构更接近用户熟悉的代码。本文提出了基于设计原则的设计模式选择方法,并给出了该方法的示例。针对目前的设计模式模型主要采用UML模型,缺乏明确语义,有些语义信息在UML图中难以反映出来的问题,本文利用形式规格说明语言Object-Z对设计模式建模,给出了基于角色的设计模式形式建模及演化方法与步骤,该方法可以避免模式在实例化时模式重叠、可追踪性差以及模式代码难于重用等问题,方便模式的自动化演化。最后,本文给出了面向服务的Web软件——BBS系统的开发实例,并就在面向服务的软件开发中如何使用设计模式进行了实践。更多还原

【Abstract】 With the development of Internet, it brings people many changes for the work and life. People depend on the Internet and require the Web software( for example e-commerce or e-government) more and more. Web software development technology is different from the traditional software development technology with the opending distributing characteristic. Traditional software system is close. The component may come from external system and is under the control of designer when comes into the system. But Web system has not the center control, and only there are uniform standards in protocol, address and the interactions. It binds when requirement. So it is necessary to compose resource autocephalous and dynamic.The Web software development and maintenance require the support of software engineering approach. It proposed the development approach of software architecture and MDA. The core of these approaches is the construct, transform and refinement of model. But UML is the main modeling language now. UML is visiual, easy understanding, but lacks the rigorous semantic. The model transform must base on the rigorous semantic.This paper proposes the approaches to service-oriented Web software development based on formal methods. Surrounded with which we researched on the formal modeling of service oriented software architecture, model-based service composition verification, formal ontology- based service component finding, formal modeling and evolution of design pattern based on role.This paper proposes the service component composition theory based on service oriented software architecture. Since existing service oriented software architecture model is described in graphics provided by W3C, lacks rigor semantics and reasoning, can not show the value of architecture, we formalize the service oriented software architecture, and research the service oriented software architecture as a architecture style. Through the research of software architecture style, we can direct the software development well using software architecture. Formalizing software architecture style made the communication more precise and convenient at the level of software architecture. Formalizing software architecture style will be beneficial to formal verification and comparison of different style.This paper formalizes the new service oriented software architecture style using formal specification notation Z, analyses and defines the properties of architecture style. Finally, we give an application, and analyse the liveness of application.Service composition is a key technology of service oriented Web software development. Verifying the functions and properties are important of service composition. To automate the verification of composite web services, a method based on labeled deterministic finite automata is presented. The behavior model of composite web services is presented. User’s function requirement and anticipant behavior are presented as CTL formula. Whether the service solves user’s requirements or existes logic errors in the interactions between the service and its user can be verified. Then it formally verifies the composite web services properties using model checking tool SMV.Retrieving reusable service components that satisfy the user’s requirements is another key technology in service oriented Web software development. This paper builds a domain ontology of computer, and proposes an approach to domain ontology-based software component retrieval. Different from the approach to keyword based retrieval, this approach can refine and extend the user’s initial query by query reasoning and provide fuzzy retrieval based on component similarity and relatedness. The whole approach extends the software reusable library to the World Wide Web. In the retrieval process, a user query in natural language is translated into RDF representation formats in order to augment retrieval recall and precision by deploying the same semantic representation technologies on both the user query side and the component side.Architecture can present the system nature, represented by concept and the relation between concepts. But architecture is barren and lack extension. Design pattern can make up the shortage. Through the analyse, decomposition of architecture, finding the pattern matching with problem, which make the architecture is close to code. This paper gives the approaches of finding design pattern based on object oriented design principle.Existing Design pattern model mainly is UML model, lack unambiguous semantic information. Semantic information is difficult to present in UML graphics. There are still many barriers when instantiating the design patterns, such as pattern overlapping, traceability, and difficulties in reusing the pattern code. This paper models the design pattern with Object-Z, and gives a rose-based approach to design pattern formal modeling. The approach can avoid the problems and facilitate the design pattern automatic evolution.Finally, this paper gives a service oriented Web software development example——BBS system, practices using design pattern in service oriented Web software development.更多还原