基于形式方法面向服务的Web软件开发技术研究
详细信息    本馆镜像全文|  推荐本文 |  |   获取CNKI官网全文
摘要
网络技术的飞速发展,给人们的工作、生活方式带来了极大的变化,人们对网络的需求与依赖也越来越明显,对Web软件的需求也越来越多,例如电子政(商)务等。Web环境的开放性、分布性等特点使得Web软件开发方法不同于传统的软件开发方法。目前还没有很完善的Web软件开发方法。开发Web软件的方法基本上还是沿用传统的软件开发方法。传统的软件系统被开发为封闭的系统。虽然其构件可以来自外部,但合并到系统运行时,它们就在系统设计者控制之下。根据这一基本思想所开发的软件都具有这一特点。但在网络上,系统可能没有这样的集中控制,它们只在协议、地址和站点的交互上有统一标准,只在需要时动态绑定,所以需要一种允许用户利用网上自治的资源实现他们自己的组合,并能自动或人机互动进行服务的动态组装方法。
     基于Web的软件系统的建立和维护需要软件工程方法的进一步支持。为降低Web软件系统的设计开发难度,已经研究提出了基于软件体系结构、模型驱动等设计方法。这些方法的核心是模型的构造、模型的转换和精化。但目前软件体系结构以及模型驱动体系结构的建模语言主要是以UML作为标准建模语言。UML具有可视化、容易理解等特点,但缺乏严格的语义,而模型的转换必须建立在严格语义的基础上。
     本文提出基于形式方法面向服务的Web软件开发方法,围绕此问题分别从形式方法在面向服务构件的软件开发中的作用出发,对面向服务的软件体系结构的形式建模、基于模型的服务组合验证、基于形式本体的服务构件的发现、基于角色的设计模式形式建模及演化进行了研究。
     提出了基于面向服务软件体系结构的自顶向下的服务构件的组装理论。鉴于目前的面向服务软件体系结构的表示主要采用W3C给出的非形式化图形表示,不能精确表示软件结构的内涵,基于面向服务软件体系结构的服务构件自动化组装存在一定的难度。本文用形式规格说明语言Z对面向服务的软件体系结构进行了形式化,并提出把面向服务的软件体系结构作为一种风格来研究。面向服务的软件体系结构风格的形式化可以更为准确和方便地在体系结构的层次上进行交流。对不同的体系结构风格进行形式化描述,有利于系统的形式化验证和不同风格之间的比较。本文还分析定义了面向服务这样一种新出现的分布式软件体系结构风格的一些性质并给出了证明,并据此风格给出了一个应用实例,并对实例的活性进行了分析。
     服务组合是面向服务的Web软件开发的关键技术之一。如何有效地验证组合服务的功能及性能是服务组合研究中必须要解决的关键问题。为了能够自动地验证组合服务的各种属性,如组合服务是否能实现用户需求的功能,以及组合服务在运行过程中是否会出现用户不期望的行为,本文使用标签状态自动机建立组合服务的形式模型,将与用户的功能需求及期望的行为相关的性质表示为CTL公式,然后用形式验证工具SMV对服务组合进行了形式化验证。
     发现服务是面向服务Web软件开发中的另一关键技术。本文通过建立一个领域本体来扩展用户查询端查询的语义精确性,这种方法一方面可以提高服务构件的查准率和查全率。另一个好处是克服了其它基于语义的方法在实际服务查询中的可操作性方面的难度。我们的方法可以很好地利用已有的搜索引擎来达到对服务查询效能方面的提高,本文给出了一个服务搜索引擎的原型系统。
     体系结构反映系统的本质,由一些抽象的概念,以及概念间的关系来表示。但体系结构过于空泛,缺乏延伸性。设计模式正好可以弥补体系结构的这一缺陷,通过对体系结构的分析、分解,寻找和我们要解决问题匹配的模式可以使抽象的体系结构更接近用户熟悉的代码。本文提出了基于设计原则的设计模式选择方法,并给出了该方法的示例。
     针对目前的设计模式模型主要采用UML模型,缺乏明确语义,有些语义信息在UML图中难以反映出来的问题,本文利用形式规格说明语言Object-Z对设计模式建模,给出了基于角色的设计模式形式建模及演化方法与步骤,该方法可以避免模式在实例化时模式重叠、可追踪性差以及模式代码难于重用等问题,方便模式的自动化演化。
     最后,本文给出了面向服务的Web软件——BBS系统的开发实例,并就在面向服务的软件开发中如何使用设计模式进行了实践。
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.
引文
[1]Baclawski,Kokar,Kogut,Hart,Smith,Holmes,Letkowski,and Aronson."Extending UML to Support Ontology Engineering for the Semantic Web." UML2001,October 2001b
    [2]Carlson.D.,Modeling XML Applications with UML.Addison-Wesley 2001
    [3]Craig Dewalt,Business Process Modeling with UML.Johns Hopkins University,7 December 1999
    [4]Pan and Horrocks."Metamodeling Architecture of Web Ontology Languages," Semantic Web Working Symposium,August 2001
    [5]楚旺,钱德沛,以体系结构为中心的构件模型的形式化语义,软件学报,2006 Vol.17No.6 P1287-1297
    [6]Rothenberger MA,Dooley KJ,Kulkarni UR.,and Nada N.Strategies for software reuse:A principal component analysis of reuse practices.IEEE Trans.on Software Engineering,2003,29(9):825-837.
    [7]Baum L,Becker M,Geyer L,Molter G.Using software architecture as a catalyst for reuse.1998.http://www.agss.informatik,uni-kl.de/mitarbeiter//baum/publications/papers
    [8]Hart J.An approach to software component specification.In:Proc.of the Int'l Workshop on Component-Based Software Engineering.1999.97-102.http://www.it.swin.edu.au/personal/jhan/jhanPapers/cbse99.pdf
    [9]Clements PC,Northrop LM.Software architecture:An executive overview.Technical Report,CMU/SEI-96-TR-003,Carnegie Mellon University,1996.
    [10]Baum L,Becker M,Geyer L,Molter G.A process view on architecture-based software development.1999.http://www.ece.utexas.edu/~perry/prof/wiesal/final
    [11]Guo J.Using category theory to model software component dependencies.In:Proe.of the 9th Annual IEEE Int'l Conf.and Workshop on the Engineering of Computer-Based Systems (ECBS 2002).IEEE Computer Society,2002.185-192.
    [12]http://www.omg.org/mda/
    [13]http://www.ibm.com/developerworks/cn/java/1-ArchUseDP/index.html面向模式构建软件系统架构
    [14]梅宏,陈锋,冯耀东,杨杰,ABC:基于体系结构、面向构件的软件开发方法.2003,14(4):721-732.
    [15]杨芙清,梅宏等,浅论软件技术发展,电子学报VOL30,N12A
    [16]孙昌爱,金茂忠,刘超,软件体系结构研究综述,软件学报,2002,13(7):1228-1237
    [17]Bass L,Clements P,Kazman R.Software Architecture in Practice.Boston,MA: Addison-Wesley,1998.
    [18]UDDI Project.UDDI Technical White Paper,September 2000.http://www.uddi.org.
    [19]http://www.w3.org/TR/rdf-primer/
    [20]C.Alexander:.The Timeless Way of Building,Oxford UniversityPress.1979
    [21]Dirk Riehle and Heinz Zullighoven's "Understanding and Using Patterns in Software Development" http://www.riehle.org/1996/TAPOS-96-Survey.html
    [22]Brad Appleton,Patterns and Software:Essential Concepts and Terminology,http://www.cmcrossroads.com/bradapp/docs/pattems-intro.html
    [23]The Patterns Home Page http://hillside.net/patterns/definition.html
    [24]Frank Buschmann,Regine Meunier,面向模式的软件体系结构卷1:模式系统 机械工业出版社,2005
    [25]http://www.omg.org/mda
    [26]张世琨,张文娟,常欣,王立福,杨芙清,基于软件体系结构的可复用构件制作和组装.软件学报.2000,12(9):1351-1359.
    [27]J.Magee,N.Dulay,S.Eisenbach,and J.Kramer.Specifying distributed software architectures.In Proceedings of the Fifth European Software Engineering Conference,ESEC'95,September 1995.
    [28]Mary Shaw,Robert Deline,Daniel V.Klein,Theodore L.Ross,David M.Young,and Gregory Zelesnik.Abstractions for software architecture and tools to support them.IEEE Transaction on Software Engineering,21(4):314-335,April 1995.
    [29]Luchham DC,Vera J.An event-based architecture definition language.IEEE Transactions on Software Engineering,1995,21(9):717-734
    [30]R.Allen.A formal approach to software architecture.PhD thesis,Carnegie Mellon Univ.,CMU Technical Report CMU-CS-97-114,May 1997.
    [31]David Garlan,Robert T.Monroe,and David Wile.ACMEE:An architecture description interchange language.Submitted for publication,January 1997.
    [32]David Garlan,Robert Allen,and John Ockerbloom.Exploiting style in architectural design environment.In Proceedings of SIGSOFT'94:2nd ACM SIGSOFT Symposium on the Foundations of Software Engineering,pages 175-188,New Orleans,LA,December 1994.ACM Press.
    [33]Talor R N,Medvidovic N,Anderson K M et al.A component-and message-based architectural style for GUI software.IEEE Transaction on Software Engineering,1996,22(6):390-406
    [34]Dewayne E.Perry and Alexander L.Wolf.Foundations for the study of software architecture.ACM SIGSOFT Software Engineering Notes,17(4):40-52,October 1992.
    [35]M.Moriconi,X.Qian and R.Riemenschneider.Correct architecture refinement.IEEE Transactions on Software Engineering,21(4):356-372,April 1995.
    [36]GailC.Murphy,David Notkin,and Kevin Sullivan.Software reflection models:Bridging the gap between source and high-level models.In Proceedings of SIGSOFT '95:Third ACM SIGSOFT Symposium on Foundations of Software Engineering,Software Engineering Notes 20(4),pages 18-28,Washington,DC,October 1995.ACM Press.
    [37]Robert Allen and David Garlan.A formal approach to software architecture.In Jan van Leeuwen,editor,Proceedings of IFIP'92,pages 134-141.Elsevier Science Publishers B.V.,September 1992.
    [38]Bass L,Clements P,Kazman R.Software Architecture in Practice.Boston,MA:Addison-Wesley,1998.
    [39]G.Abowd,R.Allen,and D.Garlan.Formalizing Style to Understand Description of Software Architecture.ACM Transactions on Software Engineering and Methodology,4(4):319-364,October 1995
    [40]P.Ciancarini,C.Mascolo.Analyzing and Refining an Architectural Style.10th international conference of Z users(ZUM97),Reading,UK.April 1997.Lecture notes in Computer Science,pages 349-368,April 1997.
    [41]焦文品,史忠植,用XYZ/E形式化体系结构风格.软件学报,2000,11(3):410-415
    [42]L.Baresi,R.Heckel,S.Th"one,and D.Varr'o.Modeling and validation of service-oriented architectures:Application vs.style.In Proc.ESEC/FSE 2003,Helsinki,Finland,September 2003.
    [43]缪淮扣,李刚,朱关铭,软件工程语言——Z.上海:上海科学技术文献出版社,1999
    [44]缪淮扣,Z User Studio研制报告,上海大学计算机学院技术报告,2000,12
    [45]Mark Saaltink.The Z/EVES system.In J.P.Bowen,M.G.Hinchey,and D.Till,editors,ZUM'97:Z Formal Specification Notation,volume 1212 of Lecture Notes in Computer Science,pages 72-85,Springer-Verlag,1997.
    [46]Ciancarini,P.and Cimato,S.and Mascolo,C.Engineering formal requirements:an analysis and testing method for Z documents.Annals of Software Engineering,1997,pp.189-220.ISSN 10227091
    [47]Dustdar S,Schreiner W,Schreiner W.A survey on Web services composition.Int'l Journal of Web and Grid Services,2005,1(1):1-30.
    [48]Narayanan S,Mcllraith SA.Simulation,verification and automated composition of web services.In:Proc.of the 11th Int'l Conf.on World Wide Web.New York:ACM Press,2002.77-88.
    [49]Koshkina M,van Breugel F.Modeling and verifying Web service orchestration by means of the concurrency workbench.ACM SIGSOFT Software Engine Notes,2004,29(5):1-10.
    [50]Qian ZZ,Lu SL,Xie L.Automatic composition of Petri net based Web services.Chinese Journal of Computers,2006,29(7):1057-1066(in Chinese with English abstract).
    [51]Hou LS,Jin Z,Wu BD.需求驱动的Web服务建模及其验证:一个基于本体的方法.Science in China(Series E),2006,36(10):1189-1219(in Chinese with English abstract).
    [52]Fu X,Bultan T,Su JW.Analysis of interacting BPEL Web services.In:Proc.of the13th Int'l Conf.on World Wide Web.New York:ACM Press,2004.621-630.
    [53]Fu X,Bultan T,Su JW.WSAT:A tool for formal analysis of Web services.In:Alur R,Peled D,eds.Proe.of the 16th Int'l Conf.on Computer Aided Verification.2004.510-514.
    [54]Fu X,Bultan T,Su JW.Synchronizability of conversations among Web services.IEEE Trans.on Software Engineering,2005,31(12):1042-1055.
    [55]Wombaeher A,Fankhauser P,Mahleko B.Matchmaking for business processes based on choreographies.In:Proe.of the IEEE Int'l Conf.on e-Technology,e-Commerce and e-Service.2004.359-368.
    [56]雷丽晖,一种基于扩展有限自动机验证组合Web服务的方法,软件学报,2007(12)
    [57]G.J.Holzmann,"The Model Checker SPIN",IEEE Transactions on Software Engineering,23(5),May 1997,pp.279-295..
    [58]K.L.McMillan,"The SMV System for SMV version 2.5.4",http://www.es.emu.edu/~modelcheck/smv/smvmanual.ps,October,2006.
    [59]Sugumaran,Vijayan;Storey,Veda C.(2003)."A Semantic-Based Approach to Component Retrieval," The DATA BASE for Advances in Information Systems-Summer 2003,Vol.34,No.3,p.8-24
    [60]Dipanjan Chakraborty,Filip Perich,Sasikanth Avancha et al.DReggie.Semantic service discovery for M-Commerce applications.In:Proceedings of the Workshop on Reliable and Secure Applications in Mobile Environment,20th Symposium on Reliable Distributed Systems,New Orleans,USA,2001,10:28-31
    [61]Terry R Payne,Massimo Paolucci,Katia Sycara.Advertising and matching DAML-S service descriptions.In:Proceedings of the International Semantic Web Working Symposium(SWWS).Amsterdam:lOS Press,2001,411-430
    [62]Klein M.,Bernstein A..Searching services on the semantic Web using process ontologies.In:Proceedings of the International Semantic Web Working Symposium(SWWS).Amsterdam:IOS Press,2001,159-172
    [63]David Trastour,Claudio Bartolini,Javier Gonzalez-Castillo.A semantic Web approach to service description for matchmaking of services.In:Proceedings of the International Semantic Web Working Symposium(SWWS).Amsterdam:IOS Press,2001,447-461
    [64]Gonzalez-Castillo J.,Trastour D.,Bartolini C..Description logics for matchmaking of services.In:Proceedings of Workshop on Application of Description Logics(KI 2001),Vienna,Austria,2001,582-586
    [65]Sycara K.,Klusch M.,Widoff S.,Lu J.,Dynamic service matchmaking among agents in open information environments.SIGMOD Record.A.Ouksel and A.Sheth,1999,47-53
    [66]吴健,基于本体论和词汇语义相似度的Web服务发现 计算机学报2005,4
    [67]T.R.Gruber,Towards Principles for the Design of Ontologies Used for Knowledge Sharing,Proceeding of the International Workshop on Formal Ontology,Padova,Italy,1993.
    [68]Gruber TR.Towards Principles for the Design of Ontologies Used for Knowledge Sharing.International Journal of H-umanComputerStudies,1995,43:907-928
    [69]Thomas R Gruber.Ontolingua:A Translation Approach to Potable Ontology Specification[J].Knowledge Acquisition,1993,5(2):199-200.
    [70]MacGregor,Inside the loom classifier.SIGART Bulletin[J].1991,2(3):70-76
    [71]Dan Brickley,Guha R V.Resource description framework(RDF) schema specification 1.0.[EB/OL].http://www.w3.org/TR/rdf-schema.
    [72]Heflin J,Hendler J.Dynamic ontologies on the web[A].Proceedings of the Seventeenth National Conference on Artificial Intelligence(AAAI-2000)[C].Menlo Park(CA):AAAI/MIT Press,2000.443-449
    [73]Ian Horrocks.DAML+OIL:a description logic for the semantic web[C].Bull.of the IEEE Computer Society Technical Committee on Data Engineering,25(1):4-9,March 2002.
    [74]Dean M,Schreiber G.OWL web ontology language reference[EB/OL],http://www.w3c.rg /TR/owl-ref,2OO4-02-10
    [75]Fridman Noy and CD Hafner.The State of the Art in Ontology Design[J].A Survey and Comparative Review.AI Magazine,pages 53-74,1997.
    [76]Resnik,P.,1995,"Using Information Content to Evaluate Semantic Similarity in a Taxonomy",Proceedings of the 14th International Joint Conference on Artificial Intelligence,Vol.1,448-453,Montreal,August 1995.
    [77]V.Cross and T.Sudkamp,Similarity and Compatibility in Fuzzy Set Theory:Assessment and Applications,New York:Physica-Verlag,ISBN 3-7908-1458,2002.
    [78]G.Smith,The Object-Z Specification Language.Kluwer Academic Publishers,Boston,2000.
    [79]Gamma,et.al.,设计模式——可复用的面向对象软件的基础,机械工业出版社,2005
    [80]http://www.junit.org
    [81]Elisabeth Freeman,Eric Freeman,BertBates,Kathy Sierra,《深入浅出设计模式》(英文影印版),东南大学出版社,2005
    [82]Hannemann J,Kiczales G.Design pattern implementation in Java and Aspect J.ACM SIGPLAN Notices,2002,37(11):161-173.
    [83]何成万,何克清,基于角色的设计模式建模和实现方法,软件学报,2006,4
    [84]Kim SK,Carrington D.Using integrated metamodeling to define OO design patterns with object-Z and UML.In:Proc.of the 11th Asia-Pacific Software Engineering Conf.(APSEC 2004).Los Alamitos:IEEE Computer Society,2004.257-264.
    [85]Jing Dong,UML Extensions for Design Pattern Compositions,in Journal of Object Technology,vol.1,no.5,pages 149-161.http://www.jot.fm/issues/issue_2002_11/article3
    [86]J.Dong,S.Yang,and K.Zhang,"A Model Transformation Approach for Design Pattern Evolutions",Proceedings of the 13th Annual IEEE International Symposium and Workshop on Engineering of Computer Based Systems,pp.80-92,2006.
    [87]France,R.,D.-K.Kim,G.Sudipto and E.Song.A UML-Based Pattern Specification Technique.IEEE Transactions on Software Engineering,Vol.30(3),2004,pp.193-206.
    [88]Lauder A.and S.Kent.Precise Visual Specification of Design Patterns,in Proc.of ECOOP'98,LNCS 1445,1998,Springer-Verlag,pp.114-134.
    [89]OMG.UML 2.0 superstructure specification,http://www.omg.org/uml/
    [90]Riehle D.Describing and Composing Patterns Using Role Diagrams,in Proc.of the Ubilab Conference' 96,1996,pp.137-152.
    [91]沈毅,缪淮扣,文志诚,陈怡海,一个Z的证明责任产生器,上海大学学报,自然科学版,2005/11
    [92]文志诚,面向对象软件的形式验证技术,博士论文,2006
    [93]I.Meisels and Mark Saaltink,The Z/EVES 2.0 reference manual.Technical Report TR-99-5493-03e,ORA Canada,Canada,1999
    [94]Dan Craigen,Irwin Meisels,and Mark Saaltink,Analysing Z Specifications with Z/EVES,In J.P.Bowen and M.Hinchey(eds.) Industrial Strength Formal Methods Springer Verlag FACIT series,1999.

© 2004-2018 中国地质图书馆版权所有 京ICP备05064691号 京公网安备11010802017129号

地址:北京市海淀区学院路29号 邮编:100083

电话:办公室:(+86 10)66554848;文献借阅、咨询服务、科技查新:66554700