The Research On Service Oriented Web Software Development Technology Based On Formal Method

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.