面向对象MSVL语言及其在组合Web服务验证中的应用
|
摘要
时序逻辑是一种规范语言,适合于并发系统的规范与验证,已经广泛的应用于数字电路、软件工程等领域的形式化验证中。时序逻辑程序设计语言是时序逻辑的一个可执行子集,可以将程序的书写、性质描述和验证统一在时序逻辑的框架中进行。对软硬件系统使用时序逻辑程序设计语言进行建模,对系统期望的性质采用时序逻辑公式来描述,将模型和性质统一在时序逻辑的框架中,从而实现对软硬件系统的形式化验证。
现有的时序逻辑程序设计语言与传统的高级程序设计语言相比,存在形式化程度过高、缺少指针数据结构和面向对象机制等不足之处,使用这些语言进行程序设计较为不便。另外,组合Web服务的形式化验证是目前研究的一个热点,使用时序逻辑程序设计语言对组合Web服务进行建模和验证,能够将模型和性质统一在时序逻辑的框架中,给形式化验证带来了方便。
本文以框架时序逻辑语言MSVL为研究对象,提出了指针数据结构的形式化方法和实现方案,给出了对象、类和继承等面向对象概念的形式化定义,并在MSVL解释器中实现了指针数据结构和面向对象机制。为了应用MSVL,研究了以OWL-S为过程描述模型的组合Web服务,提出了组合Web服务的基于MSVL的建模方法和验证方法。
本文的主要贡献如下:
(1)以框架时序逻辑语言MSVL为研究对象,从逻辑语言的角度出发,提出了基于名字常量的指针形式化方法和实现方案;从命令式语言的角度出发,提出了基于内容变量的指针形式化方法和实现方案。
(2)在MSVL解释器中实现了基于内容变量的指针,使用指针模拟实现了引用调用的参数传递方式,使用指针实现了原地逆置单链表的程序,并使用解释器对该程序进行了基于模型检测的形式化验证。
(3)对投影时序逻辑进行扩展,基于变量集合的层次化和谓词的分组,给了对象、类和继承等面向对象概念的形式化定义,并将扩展投影时序逻辑的一个可执行子集定义为面向对象MSVL。
(4)提出了面向对象MSVL的解释器基本框架和实现方案,使用VisualC++/Flex/Bison实现了该解释器;使用面向对象MSVL编写数字信号处理程序,使用面向对象MSVL的解释器在仿真模式下执行该程序,从而实现了数字信号处理的仿真。
(5)使用面向对象MSVL语言描述以OWL-S为过程描述模型的组合Web服务,使用命题投影时序逻辑描述期望的性质,使用面向对象MSVL的解释器在验证模式下执行带性质描述的程序,从而实现了组合Web服务基于模型检测的形式化验证。
Temporal logic is a specification language which is suitable for specification andverification of concurrent systems, and it has been widely used in the formalverification of digital circuits and software engineering. A temporal logic programminglanguage is an executable subset of temporal logic, and it provides a framework inwhich writing of programs, properties of programs, and verification of programs canall be treated within temporal logic. The temporal logic programming languages areused to model software and hardware, and temporal logic formulas are used to describedesired properties, thus the model and properties are both in temporal logic, and thenthe formal verification of software and hardware can be performed.
Compared with traditional high-level programming languages, the existingtemporal logic programming languages have some shortages such as highformalization, lack of the pointers and object-oriented mechanisms, and it isinconvenience to program in these languages. In addition, the formal verification ofcomposite Web Services is a research focus at present. The temporal logicprogramming languages can be used to model and verify composite Web Services, thusthe model and properties are both in temporal logic which brings conveniences to theformal verification.
This dissertation mainly focuses on the framed temporal logic programminglanguage MSVL, and proposes the formalization and implementation of pointers. Theformal definitions of object-oriented concepts such as objects, classes and inheritancesare given. Then an interpreter for MSVL has been developed to support pointers andobject-oriented mechanisms. In order to apply MSVL, the composite Web Servicesbased on the OWL-S process model are analyzed, and a modeling and verificationmethod of composite Web Services based on MSVL is proposed.
The main contributions of this dissertation are as follows:
(1) The framed temporal logic programming language MSVL is analyzed, and theformalization and implementation of pointers based on name constants are proposedfrom the point of view of logic languages, then the formalization and implementation ofpointers based on content variables are also proposed from the point of view ofimperative languages.
(2) The pointers based on content variables are implemented in the interpreter forMSVL. Pointers are used to simulate parameter passing by reference and are used in theprogram for in place reversal of singly linked list, and then the program is verified via model checking with the interpreter.
(3) Projection Temporal Logic is extended, and then formal definitions ofobject-oriented concepts such as objects, classes and inheritances are given based on thehierarchical variable sets and grouping predicates. Object-oriented MSVL is defined asan executable subset of Extended Projection Temporal Logic.
(4) The basic framework and design plan of the interpreter for object-orientedMSVL are proposed, and the interpreter has been developed in Visual C++/Flex/Bison.A program for digital signal processing is written in object-oriented MSVL, and theinterpreter for object-oriented MSVL is used to execute it in simulation mode tosimulate digital signal processing.
(5) Object-oriented MSVL is used to model the composite Web Services based onthe OWL-S process model, and Propositional Projection Temporal Logic is used todescribe desired properties, thus the interpreter for object-oriented MSVL executes theprograms with properties in verification mode to verify the composite Web Servicesvia model checking.
现有的时序逻辑程序设计语言与传统的高级程序设计语言相比,存在形式化程度过高、缺少指针数据结构和面向对象机制等不足之处,使用这些语言进行程序设计较为不便。另外,组合Web服务的形式化验证是目前研究的一个热点,使用时序逻辑程序设计语言对组合Web服务进行建模和验证,能够将模型和性质统一在时序逻辑的框架中,给形式化验证带来了方便。
本文以框架时序逻辑语言MSVL为研究对象,提出了指针数据结构的形式化方法和实现方案,给出了对象、类和继承等面向对象概念的形式化定义,并在MSVL解释器中实现了指针数据结构和面向对象机制。为了应用MSVL,研究了以OWL-S为过程描述模型的组合Web服务,提出了组合Web服务的基于MSVL的建模方法和验证方法。
本文的主要贡献如下:
(1)以框架时序逻辑语言MSVL为研究对象,从逻辑语言的角度出发,提出了基于名字常量的指针形式化方法和实现方案;从命令式语言的角度出发,提出了基于内容变量的指针形式化方法和实现方案。
(2)在MSVL解释器中实现了基于内容变量的指针,使用指针模拟实现了引用调用的参数传递方式,使用指针实现了原地逆置单链表的程序,并使用解释器对该程序进行了基于模型检测的形式化验证。
(3)对投影时序逻辑进行扩展,基于变量集合的层次化和谓词的分组,给了对象、类和继承等面向对象概念的形式化定义,并将扩展投影时序逻辑的一个可执行子集定义为面向对象MSVL。
(4)提出了面向对象MSVL的解释器基本框架和实现方案,使用VisualC++/Flex/Bison实现了该解释器;使用面向对象MSVL编写数字信号处理程序,使用面向对象MSVL的解释器在仿真模式下执行该程序,从而实现了数字信号处理的仿真。
(5)使用面向对象MSVL语言描述以OWL-S为过程描述模型的组合Web服务,使用命题投影时序逻辑描述期望的性质,使用面向对象MSVL的解释器在验证模式下执行带性质描述的程序,从而实现了组合Web服务基于模型检测的形式化验证。
Temporal logic is a specification language which is suitable for specification andverification of concurrent systems, and it has been widely used in the formalverification of digital circuits and software engineering. A temporal logic programminglanguage is an executable subset of temporal logic, and it provides a framework inwhich writing of programs, properties of programs, and verification of programs canall be treated within temporal logic. The temporal logic programming languages areused to model software and hardware, and temporal logic formulas are used to describedesired properties, thus the model and properties are both in temporal logic, and thenthe formal verification of software and hardware can be performed.
Compared with traditional high-level programming languages, the existingtemporal logic programming languages have some shortages such as highformalization, lack of the pointers and object-oriented mechanisms, and it isinconvenience to program in these languages. In addition, the formal verification ofcomposite Web Services is a research focus at present. The temporal logicprogramming languages can be used to model and verify composite Web Services, thusthe model and properties are both in temporal logic which brings conveniences to theformal verification.
This dissertation mainly focuses on the framed temporal logic programminglanguage MSVL, and proposes the formalization and implementation of pointers. Theformal definitions of object-oriented concepts such as objects, classes and inheritancesare given. Then an interpreter for MSVL has been developed to support pointers andobject-oriented mechanisms. In order to apply MSVL, the composite Web Servicesbased on the OWL-S process model are analyzed, and a modeling and verificationmethod of composite Web Services based on MSVL is proposed.
The main contributions of this dissertation are as follows:
(1) The framed temporal logic programming language MSVL is analyzed, and theformalization and implementation of pointers based on name constants are proposedfrom the point of view of logic languages, then the formalization and implementation ofpointers based on content variables are also proposed from the point of view ofimperative languages.
(2) The pointers based on content variables are implemented in the interpreter forMSVL. Pointers are used to simulate parameter passing by reference and are used in theprogram for in place reversal of singly linked list, and then the program is verified via model checking with the interpreter.
(3) Projection Temporal Logic is extended, and then formal definitions ofobject-oriented concepts such as objects, classes and inheritances are given based on thehierarchical variable sets and grouping predicates. Object-oriented MSVL is defined asan executable subset of Extended Projection Temporal Logic.
(4) The basic framework and design plan of the interpreter for object-orientedMSVL are proposed, and the interpreter has been developed in Visual C++/Flex/Bison.A program for digital signal processing is written in object-oriented MSVL, and theinterpreter for object-oriented MSVL is used to execute it in simulation mode tosimulate digital signal processing.
(5) Object-oriented MSVL is used to model the composite Web Services based onthe OWL-S process model, and Propositional Projection Temporal Logic is used todescribe desired properties, thus the interpreter for object-oriented MSVL executes theprograms with properties in verification mode to verify the composite Web Servicesvia model checking.
引文
[1]古天龙.软件开发的形式化方法[M].北京:高等教育出版社, 2005.
[2] Hoare C. A. R. An Axiomatic Basis for Computer Programming[J].Communication of ACM, 1969, 12(10): 576-580.
[3] Floyd Robert W. Assigning Meanings to Programs[C]. Proceedings of theAmerican Mathematical Society Symposia in Applied Mathematics. 1967: 19-31.
[4] Pnueli Amir. Temporal Verification of Reactive Systems: Safety[M].Springer-Verlag, 1995.
[5] Pnueli Amir. The Temporal Logic of Reactive and ConcurrentSystems:Specification[M]. Springer-Verlag, 1992.
[6] Clarke E. M., Emerson E. A., Sistla A. P. Automatic Verification of Finite-StateConcurrent Systems Using Temporal Logic Specifications[J]. ACM Transactionson Programming Languages and Systems, 1986, 8(2): 244-263.
[7] Gallier Jean. Logic for Computer Science: Foundations of Automatic TheoremProving[M]. John Wiley & Sons Inc, 1986.
[8] Merz Stephan. Model Checking: A Tutorial Overview[M]. Modeling andverification of parallel processes, Springer-Verlag New York, Inc., 2001, 3-38.
[9] Huth Michael, Ryan Mark. Logic in Computer Science: Modelling and ReasoningAbout Systems[M]. Cambridge University Press, 2004.
[10]唐稚松. XYZ系统的目的、意义、作用与应用[J].软件学报, 1999, 10(04):337-341.
[11] Tang C. S. A Unified Formal Basis for the Case Tools System[J]. Journal ofSystems Integration, 1993, 3(2): 103-132.
[12] Xie Hongliang, Gong Jie, Tang C. A Structured Temporal Logic Language:Xyz/Se[J]. Journal of Computer Science and Technology, 1991, 6(1): 1-10.
[13] Liu Tong, Tang C. Semantic Specification and Verification of Data FlowDiagrams[J]. Journal of Computer Science and Technology, 1991, 6(1): 21-31.
[14] Hale Roger. Programming in Temporal Logic[D]. Cambridge University, 1989.
[15] Moszkowski Ben C. Executing Temporal Logic Programs[M]. Cambridge:Cambridge University Press, 1986.
[16] Duan Zhenhua, Yang Xiaoxiao, Koutny Maciej. Framed Temporal LogicProgramming[J]. Science of Computer Programming, 2008, 70(1): 31-61.
[17] Fujita M., Kono S., Tanaka H., et al. Tokio: Logic Programming Language BasedOn Temporal Logic and its Compilation to Prolog[C]. Proceedings on Thirdinternational conference on logic programming. London,UK: Springer-Verlag,1986: 695-709.
[18] Aoyagi T., Fujita M., Moto-oka T. Temporal Logic Programming LanguageTokio Programming in Tokio[C]. Proceedings of 4th Conference on LogicProgramming '85. Berlin: Springer-Verlag, 1985: 128-137.
[19] Fisher Michael. Metatem : The Story so Far[C]. Proceedings of ProMAS 2005.Berlin: Springer-Verlag, 2006: 3-22.
[20] Barringer H., Fisher M., Gabbay D., et al. Metatem: An Introduction[J]. FormalAspects of Computing, 1995, 7(5): 533-549.
[21] Engberg Urban, Gronning Peter, Lamport Leslie. Mechanical Verification ofConcurrent Systems with Tla[C]. Larch. 1992: 86-97.
[22]唐稚松.时序逻辑程序设计与软件工程[M].北京:科学出版社, 1999.
[23]沈武威,唐稚松. XYZ系统在电信领域中的应用[J].软件学报, 1996, 7(06):321-330.
[24]唐小平,唐稚松,马华东,等. XYZ系统在动画设计中的应用[J].软件学报,1998, 9(01): 1-6.
[25] Liu W., Ma H. Modeling Video-On-Demand System in Temporal Logic[J].Advances in Multimedia Information Processing—PCM 2001, 2001: 983-988.
[26] Ma Huadong, Liu Shenquan. Multimedia Data Modeling Based On TemporalLogic and Xyz System[J]. Journal of Computer Science and Technology, 1999,14(2): 188-193.
[27] Ma Huadong. Temporal Logic Based Workflow Service Modeling and itsApplication[J]. Computer Supported Cooperative Work in Design, 2005: 349-358.
[28] Rao Yuan. Temporal Logical-Based Web Services Architecture Description[J].Grid and Cooperative Computing - GCC 2005, 2005: 214-219.
[29] Interval Temporal Logic. http://www.cse.dmu.ac.uk/STRL/ITL.
[30] Hayes John Mccarthy And Patrick J. Some Philosophical Problems From theStandpoint of Artificial Intelligence[M]. Machine Intelligence 4, EdinburghUniversity Press, 1969, 463-502.
[31] Hira M., Sarkar, D. Verification of Tempura Specification of SequentialCircuits[J]. IEEE Trans. on CAD of Integrated Circuits and Systems, 1997, 16(4):362-375.
[32] Moszkowski Ben C. Compositional Reasoning Using Interval Temporal Logicand Tempura[C]. Proceeding of Compositionality: The Significant Difference,International Symposium. 1997: 439-464.
[33] Cau Antonio, Zedan Hussein, Coleman Nick, et al. Using Itl and Tempura forLarge Scale Specification and Simulation[C]. Proceeding of 4th EuromicroWorkshop on Parallel and Distributed Processing. IEEE Computer Society Press,1996: 493-500.
[34] Solanki Monika. Tesco-S a Framework for Defining Temporal Semantics in OwlEnabled Services[C]. Proceeding of W3C Workshop on Frameworks for Semanticsin Web Services. 2005: 1-6.
[35] Monika Solanki, Antonio Cau And Hussein Zedan. Semantically AnnotatingReactive Web Services with Temporal Specifications[C]. Proceedings of the IEEEICWS 2005, Second International Workshop on Semantic and Dynamic WebProcesses. 2005.
[36] Duan zhenhua, Tian cong. A Unified Model Checking Approach with ProjectionTemporal Logic[C]. Proceedings of ICFEM 2008. Berlin: Springer-Verlag, 2008:167-186.
[37] Ma Yongtao, Duan Zhenhua, Wang Xiaobing, et al. An Interpreter for FramedTempura and its Application[C]. Proceedings of First Joint IEEE/IFIP Symposiumon Theoretical Aspects of Software Engineering. Shanghai: IEEE Press, 2007:251-260.
[38] Duan Zhenhua, Tian Cong, Zhang Li. A Decision Procedure for PropositionalProjection Temporal Logic with Infinite Models[J]. Acta Informatica, 2008, 45(1):43-78.
[39] Duan Zhenhua, Zhang Nan. A Complete Axiomatization of PropositionalProjection Temporal Logic[C]. Proceedings of the 2008 2nd IFIP/IEEEInternational Symposium on Theoretical Aspects of Software Engineering.Washington, DC, USA: IEEE Computer Society, 2008: 271-278.
[40] Duan Zhenhua, Tian Cong. Decidability of Propositional Projection TemporalLogic with Infinite Models[C]. Proceedings of TAMC 2007. Berlin:Springer-Verlag, 2007: 521-532.
[41] Duan Zhenhua. An Extended Interval Temporal Logic and a Framing Techniquefor Temporal Logic Programming[D]. University of Newcastle upon Tyne, 1996.
[42]雷丽晖,段振华.使用扩展区间时序逻辑为并发工作流建模[J].西安电子科技大学学报(自然科学版), 2007, 34(4): 673-680.
[43]雷丽晖,段振华.基于扩展投影时序逻辑的组合Web服务描述与验证[J].西安交通大学学报, 2007, 41(10): 1155-1159.
[44]张海宾,段振华.混合投影时序逻辑与混合系统的形式化验证[J].计算机科学, 2007, 34(11): 279-282.
[45] Kono Shinji. A Combination of Clausal and Non Clausal Temporal LogicPrograms[C]. Proceedings of the Workshop on Executable Modal and TemporalLogics. Berlin: Springer-Verlag, 1993: 40-57.
[46] Fisher Michael, Owens Richard. An Introduction to Executable Modal andTemporal Logics[C]. IJCAI '93: Proceedings of the Workshop on ExecutableModal and Temporal Logics. London, UK: Springer-Verlag, 1995: 1-20.
[47] Barringer Howard, Fisher Michael, Gabbay Dov M., et al. Metatem: AFramework for Programming in Temporal Logic[C]. REX Workshop. 1989:94-129.
[48] Fisher Michael, Owens Richard. From the Past to the Future: Executing TemporalLogic Programs[C]. Proceedings of Logic Programming and Automated Reasoning.Springer Verlag, 1992: 369-380.
[49] Lamport Leslie. Tla+[R]. DEC Digital Systems, 1995.
[50] Lamport Leslie. Specifying Systems : The Tla+ Language and Tools forHardware and Software Engineers[M]. 75 Arlington Street, Suite 300 Boston, MAUSA: Addison-Wesley Longman Publishing Co., Inc., 2002.
[51] Yu Yuan, Manolios Panagiotis, Lamport Leslie. Model Checking Tla+Specifications[C]. London, UK: Springer-Verlag, 1999: 54-66.
[52] Tla+ Tools. https://research.microsoft.com/en-us/um/people/lamport/tla/tools.html.
[53]岳昆,王晓玲,周傲英. Web服务核心支撑技术:研究综述[J].软件学报, 2004,15(03): 428-442.
[54]廖军,谭浩,刘锦德.基于Pi-演算的Web服务组合的描述和验证[J].计算机学报, 2005, 28(04): 635-643.
[55]侯丽珊,金芝,吴步丹.需求驱动的Web服务建模及其验证:一个基于本体的方法[J].中国科学(E辑:信息科学), 2006, 36(10): 1189-1219.
[56] Narayanan Srini, Mc Sheila A. Simulation, Verification and AutomatedComposition of Web Services[C]. Proceedings of the 11th international conferenceon World Wide Web. New York, NY, USA: ACM, 2002: 77-88.
[57]雷丽晖,段振华.一种基于扩展有限自动机验证组合Web服务的方法[J].软件学报, 2007, 18(12): 2981-2990.
[58]饶元,李尊朝.基于XYZ/ADL的Web服务体系结构形式描述[J].系统工程理论与实践, 2006, 26(03): 53-60.
[59]黄正宝,张广泉. UML 2.0顺序图的XYZ/E时序逻辑语义研究[J].计算机科学2006, 33(8): 249-251.
[60]朱雪阳,唐稚松. UML活动图的时序逻辑语义[J].计算机研究与发展, 2005,42(9): 1478-1484.
[61] Duan Zhenhua. Temporal Logic and Temporal Logic Programming[M]. Beijing:Science Press, 2006.
[62] Yang Xiaoxiao, Duan Zhenhua. Operational Semantics of Framed TemporalLogic Programs[C]. Proceedings of SOFSEM 2007. Berlin: Springer-Verlag, 2007:566-578.
[63] Holzmann Gerard J. The Model Checker Spin[J]. IEEE Transactions on SoftwareEngineering, 1997, 23(5): 279-295.
[64] Tian Cong, Duan Zhenhua. Model Checking Propositional Projection TemporalLogic Based On Spin[C]. Proceedings of the 9th international Annual Conf. onFormal Enginnering Method. Berlin: Springer-Verlag, 2007: 246-265.
[65] Zhuo Huang, Jian Zhang. Generating Sat Instances From First-Order Formulas[J].Journal of Software, 2005, 16(03): 327-335.
[66] Jian Zhan. Deciding the Satisfiability of Logical Formulas—Methods, Tools andApplications[M]. Beijing: Science Press, 2000.
[67] Scott Michael L. Programming Language Pragmatics(2nd Edition)[M]. ElsevierInc., 2006.
[68] Sebesta Robert W. Concepts of Programming Languages(7th Edition)[M].Addison-Wesley Longman Publishing Co., Inc., 2006.
[69] Cormen Thomas H., Stein Clifford, Rivest Ronald L., et al. Introduction toAlgorithms[M]. MIT Press, 2001.
[70] Zhang Jian. Symbolic Execution of Program Paths Involving Pointer andStructure Variables[C]. Proceeding of 4th International Conference on QualitySoftware. 2004: 87-92.
[71] Distefano Dino, Katoen Joost- Pieter, Rensink Arend. Safety and Liveness inConcurrent Pointer Programs[J]. Formal Methods for Components and Objects,2006: 280-312.
[72] Distefano Dino, Katoen Joost- Pieter, Rensink Arend. Who is Pointing When toWhom?[C]. Proceedings of FSTTCS 2004. Berlin: Springer-Verlag, 2005:250-262.
[73] Distefano Dino. On Model Checking the Dynamics of Object-Based Software: AFoundational Approach[D]. University of Twente, 2003.
[74] Reynolds J. C. Separation Logic: A Logic for Shared Mutable Data Structures[C].Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science.Washington, DC, USA: IEEE Computer Society, 2002: 55-74.
[75]陈意云,华保健,葛琳,等.一种用于指针程序安全性证明的指针逻辑[J].计算机学报, 2008, 31(3): 372-380.
[76] Wang Zhifang, Chen Yiyun, Wang Zhenming, et al. An Extension to PointerLogic for Verification[C]. TASE '08: Proceedings of the 2008 2nd IFIP/IEEEInternational Symposium on Theoretical Aspects of Software Engineering.Washington, DC, USA: IEEE Computer Society, 2008: 49-56.
[77] Marti Nicolas, Affeldt Reynald, Yonezawa Akinori. Formal Verification of theHeap Manager of an Operating System Using Separation Logic[J]. FormalMethods and Software Engineering, 2006: 400-419.
[78] Li Guang-yuan, Tang Zhi-song. Formalization and Verification of Pointers in theTemporal Logic Language Xyz/E Programs[J]. Journal of Software, 2000, 11(3):285-292.
[79]王小兵,段振华.框架投影时序逻辑程序设计语言中的指针[J].西安电子科技大学学报(自然科学版), 2008, 35(06): 1069-1074.
[80] Zhenhua Duan, Xiaobing Wang. Implementing Pointer in Temporal LogicProgramming Languages[C]. Proceedings of Brazilian Symposium on FormalMethods. Natal, Brazil: The Brazilian Symposium on Formal Methods, 2006:171-184.
[81]苏云霖.编译原理[M].机械工业出版社, 2008.
[82] Zhu, H. And Zhou M. c. Object-Oriented Programming with C++: AProject-Based Approach[M]. Beijing: Tsinghua University Press, 2006.
[83] Hoare C. a. r., Jifeng He. Unified Theories of Programming[M]. Prentice Hall,1998.
[84] Santos Thiago, Cavalcanti Ana, Sampaio Augusto. Object-Orientation in theUtp[C]. Proceedings of UTP 2006. Berlin: Springer-Verlag, 2006: 18-37.
[85] Jifeng He, Li Xiaoshan, Liu Zhiming. Rcos: A Refinement Calculus of ObjectSystems[J]. Theoretical Computer Science, 2006, 365(1): 109-142.
[86] Morgan Carroll. Programming From Specifications[M]. Upper Saddle River, NJ,USA: Prentice-Hall, 1990.
[87] Quan Long, Zongyan Qiu, Zhiming Liu, Lingshuang Shao And He Jifeng. Post: ACase Study for Rcos Incremental Development[R]. Macau: United NationsUniversity International Institute for Software Technology, 2005.
[88] Abadi Mart, Leino K. Rustan. A Logic of Object-Oriented Programs[C].Proceedings of TAPSOFT 1997. Berlin: Springer-Verlag, 1997: 11-41.
[89] Spivey J. M. An Introduction to Z and Formal Specifications[J]. SoftwareEngineering Journal, 1989, 4(1): 40-50.
[90]缪淮扣,李刚,朱关铭.软件工程语言—Z[M].上海:上海科学技术文献出版社, 1999.
[91] Smith Graeme. The Object-Z Specification Language[M]. Kluwer AcademicPublishers, 2000.
[92] Duke Roger, Rose Gordon. Formal Object-Oriented Specification UsingObject-Z[M]. MacMillan, 2000.
[93] D Eug, Van Katwijk Jan. Vdm++: A Formal Specification Language forObject-Oriented Designs[C]. Hertfordshire, UK: Prentice Hall International Ltd.,1992: 63-77.
[94]吴哲辉. Petri网导论[M].北京:机械工业出版社, 2006.
[95] Coleman Derek, Hayes Fiona, Bear Stephen. Introducing Objectcharts Or How toUse Statecharts in Object-Oriented Design[J]. IEEE Transactions on SoftwareEngineering, 1992, 18(1): 9-18.
[96] Wang Li-chih. Object-Oriented Petri Nets for Modelling and Analysis ofAutomated Manufacturing Systems[J]. Computer Integrated ManufacturingSystems, 1996, 9(2): 111-125.
[97]熊毅,左志宏,周明天.面向对象的命题逻辑和分布式推理[J].计算机科学,2004, 31(2): 104-108.
[98] Amir Eyal. Object-Oriented First-Order Logic[C]. Proceedings of the IJCAI 1999.Murray Hill, New Jersey: International Joint Conference on Artificial Intelligence,1999: 1-8.
[99]李平福,陈冬火,张广泉.面向对象系统的时序逻辑描述[J].苏州大学学报(工科版), 2008, 28(04): 12-19.
[100]郭亮,唐稚松. XYZ/E面向对象程序语义概述[J].软件学报, 2003, 14(3):356-361.
[101]王小兵,段振华.面向对象的时序逻辑语言[J].电子科技大学学报(自然科学版), 2009, 38(01): 97-101.
[102] The Lex & Yacc Page. http://dinosaur.compilertools.net/.
[103] Ruby. http://www.ruby-lang.org/en/.
[104] Python. http://www.python.org/.
[105] Liu Shaoying. Formal Engineering for Industrial Software Development[M].SpringerVerlag, 2004.
[106]林惠民,张文辉.模型检测:理论、方法与应用[J].电子学报, 2002(S1):1907-1912.
[107] Pierce Benjamin C. Types and Programming Languages[M]. Cambridge: MITPress, 2002.
[108] Web Services Description Language (Wsdl) 1.1[EB/OL]. 2001.
[109] Oasis Uddi Specifications Tc - Committee Specifications[EB/OL]. http://www.oasis-open.org/committees/uddi-spec/doc/tcspecs.htm,
[110] Web Services Business Process Execution Language Version 2.0[EB/OL]. http://docs.oasis-open.org/wsbpel/2.0/CS01/wsbpel-v2.0-CS01.html, 2007.
[111] Web Service Choreography Interface (Wsci) 1.0[EB/OL]. http://www.w3.org/TR/wsci/, 2002.
[112] Owl-S: Semantic Markup for Web Services[EB/OL]. http://www.w3.org/Submission/OWL-S/, 2004.
[113]刘如娟,戴桂兰,胡长军,等. Web服务的模型检测技术探讨[J].小型微型计算机系统, 2007, 28(11): 1921-1927.
[114] Ankolekar Anupriya, Paolucci Massimo, Sycara Katia. Towards a FormalVerification of Owl-S Process Models[C]. Proceedings of ISWC 2005. Berlin:Springer-Verlag, 2005: 37-51.
[115] Clarke E., Grumberg O., Long D. Verification Tools for Finite-State ConcurrentSystems[J]. A Decade of Concurrency Reflections and Perspectives, 1994:124-175.
[116] M. Panti,l. Spalazzi s. Tacconi. Using the Nusmv Model Checker to Verify theKerberos Protocol[C]. Proceeding of the 3rd Collaborative TechnologiesSymposium. 2002: 27-31.
[117] Pettersson Paul, Larsen Kim G. Uppaal2k[J]. Bulletin of the EuropeanAssociation for Theoretical Computer Science (EATCS), 2000, 70: 40-44.
[118] Schmidt Karsten. Lola: A Low Level Analyser[C]. Proceedings of 21stInternational Conference on Application and Theory of Petri Nets(ICATPN 2000).Springer-Verlag, 2000: 465-474.
[119] Cleaveland Rance, Sims Steve. The Ncsu Concurrency Workbench[C]. CAV '96:Proceedings of the 8th International Conference on Computer Aided Verification.London, UK: Springer-Verlag, 1996: 394-397.
[120] Sala Gwen, Bordeaux Lucas, Schaerf Marco. Describing and Reasoning On WebServices Using Process Algebra[C]. ICWS '04: Proceedings of the IEEEInternational Conference on Web Services. Washington, DC, USA: IEEEComputer Society, 2004: 43-50.
[121] Hinz Sebastian, Schmidt Karsten, Stahl Christian. Transforming Bpel to PetriNets[C]. Proceedings of 3rd International Conference BPM. Springer Verlag, 2005:220-235.
[122] Schmidt Karsten, Stahl Christian. A Petri Net Semantic for Bpel4ws - Validationand Application[C]. Proceedings of the 11th Workshop on Algorithms and Toolsfor Petri Nets (AWPN'04),. University Paderborn, 2004: 1-6.
[123] Fu Xiang, Bultan Tevfik, Su Jianwen. Wsat: A Tool for Formal Analysis of WebServices[C]. Proceedings of 16th International Conference on Computer AidedVerification (CAV 2004). Springer, 2004: 510-514.
[124]蒋运承,史忠植. OWL-S的形式语义[J].计算机科学, 2005, 34(07): 5-7.
[125]王杰生,李舟军,李梦君.用描述逻辑进行语义Web服务组合[J].软件学报,2008, 19(04): 967-980.
[126] Solanki Monika, Cau Antonio, Zedan Hussein. Asdl: A Wide Spectrum Languagefor Designing Web Services[C]. Proceedings of the 15th international conferenceon World Wide Web(WWW 2006). New York, NY, USA: ACM, 2006: 687-696.
[127] Solanki Monika. A Compositional Framework for the Specification, Verificationand Runtime Validation of Reactive Web Services[D]. De Montfort University,Leicester, UK, 2005.
[128] An Ontology for Itl and Tempura. http://www.cse.dmu.ac.uk/~monika/Pages/Ontologies/OntoITL.owl.
[129]王小兵,段振华.面向投影时序逻辑的Web服务模型检测[J].西安交通大学学报, 2009, 43(04): 39-43.
[130] Pvs. http://pvs.csl.sri.com/.
[131] The Hol System. http://www.cl.cam.ac.uk/research/hvg/HOL/.
[2] Hoare C. A. R. An Axiomatic Basis for Computer Programming[J].Communication of ACM, 1969, 12(10): 576-580.
[3] Floyd Robert W. Assigning Meanings to Programs[C]. Proceedings of theAmerican Mathematical Society Symposia in Applied Mathematics. 1967: 19-31.
[4] Pnueli Amir. Temporal Verification of Reactive Systems: Safety[M].Springer-Verlag, 1995.
[5] Pnueli Amir. The Temporal Logic of Reactive and ConcurrentSystems:Specification[M]. Springer-Verlag, 1992.
[6] Clarke E. M., Emerson E. A., Sistla A. P. Automatic Verification of Finite-StateConcurrent Systems Using Temporal Logic Specifications[J]. ACM Transactionson Programming Languages and Systems, 1986, 8(2): 244-263.
[7] Gallier Jean. Logic for Computer Science: Foundations of Automatic TheoremProving[M]. John Wiley & Sons Inc, 1986.
[8] Merz Stephan. Model Checking: A Tutorial Overview[M]. Modeling andverification of parallel processes, Springer-Verlag New York, Inc., 2001, 3-38.
[9] Huth Michael, Ryan Mark. Logic in Computer Science: Modelling and ReasoningAbout Systems[M]. Cambridge University Press, 2004.
[10]唐稚松. XYZ系统的目的、意义、作用与应用[J].软件学报, 1999, 10(04):337-341.
[11] Tang C. S. A Unified Formal Basis for the Case Tools System[J]. Journal ofSystems Integration, 1993, 3(2): 103-132.
[12] Xie Hongliang, Gong Jie, Tang C. A Structured Temporal Logic Language:Xyz/Se[J]. Journal of Computer Science and Technology, 1991, 6(1): 1-10.
[13] Liu Tong, Tang C. Semantic Specification and Verification of Data FlowDiagrams[J]. Journal of Computer Science and Technology, 1991, 6(1): 21-31.
[14] Hale Roger. Programming in Temporal Logic[D]. Cambridge University, 1989.
[15] Moszkowski Ben C. Executing Temporal Logic Programs[M]. Cambridge:Cambridge University Press, 1986.
[16] Duan Zhenhua, Yang Xiaoxiao, Koutny Maciej. Framed Temporal LogicProgramming[J]. Science of Computer Programming, 2008, 70(1): 31-61.
[17] Fujita M., Kono S., Tanaka H., et al. Tokio: Logic Programming Language BasedOn Temporal Logic and its Compilation to Prolog[C]. Proceedings on Thirdinternational conference on logic programming. London,UK: Springer-Verlag,1986: 695-709.
[18] Aoyagi T., Fujita M., Moto-oka T. Temporal Logic Programming LanguageTokio Programming in Tokio[C]. Proceedings of 4th Conference on LogicProgramming '85. Berlin: Springer-Verlag, 1985: 128-137.
[19] Fisher Michael. Metatem : The Story so Far[C]. Proceedings of ProMAS 2005.Berlin: Springer-Verlag, 2006: 3-22.
[20] Barringer H., Fisher M., Gabbay D., et al. Metatem: An Introduction[J]. FormalAspects of Computing, 1995, 7(5): 533-549.
[21] Engberg Urban, Gronning Peter, Lamport Leslie. Mechanical Verification ofConcurrent Systems with Tla[C]. Larch. 1992: 86-97.
[22]唐稚松.时序逻辑程序设计与软件工程[M].北京:科学出版社, 1999.
[23]沈武威,唐稚松. XYZ系统在电信领域中的应用[J].软件学报, 1996, 7(06):321-330.
[24]唐小平,唐稚松,马华东,等. XYZ系统在动画设计中的应用[J].软件学报,1998, 9(01): 1-6.
[25] Liu W., Ma H. Modeling Video-On-Demand System in Temporal Logic[J].Advances in Multimedia Information Processing—PCM 2001, 2001: 983-988.
[26] Ma Huadong, Liu Shenquan. Multimedia Data Modeling Based On TemporalLogic and Xyz System[J]. Journal of Computer Science and Technology, 1999,14(2): 188-193.
[27] Ma Huadong. Temporal Logic Based Workflow Service Modeling and itsApplication[J]. Computer Supported Cooperative Work in Design, 2005: 349-358.
[28] Rao Yuan. Temporal Logical-Based Web Services Architecture Description[J].Grid and Cooperative Computing - GCC 2005, 2005: 214-219.
[29] Interval Temporal Logic. http://www.cse.dmu.ac.uk/STRL/ITL.
[30] Hayes John Mccarthy And Patrick J. Some Philosophical Problems From theStandpoint of Artificial Intelligence[M]. Machine Intelligence 4, EdinburghUniversity Press, 1969, 463-502.
[31] Hira M., Sarkar, D. Verification of Tempura Specification of SequentialCircuits[J]. IEEE Trans. on CAD of Integrated Circuits and Systems, 1997, 16(4):362-375.
[32] Moszkowski Ben C. Compositional Reasoning Using Interval Temporal Logicand Tempura[C]. Proceeding of Compositionality: The Significant Difference,International Symposium. 1997: 439-464.
[33] Cau Antonio, Zedan Hussein, Coleman Nick, et al. Using Itl and Tempura forLarge Scale Specification and Simulation[C]. Proceeding of 4th EuromicroWorkshop on Parallel and Distributed Processing. IEEE Computer Society Press,1996: 493-500.
[34] Solanki Monika. Tesco-S a Framework for Defining Temporal Semantics in OwlEnabled Services[C]. Proceeding of W3C Workshop on Frameworks for Semanticsin Web Services. 2005: 1-6.
[35] Monika Solanki, Antonio Cau And Hussein Zedan. Semantically AnnotatingReactive Web Services with Temporal Specifications[C]. Proceedings of the IEEEICWS 2005, Second International Workshop on Semantic and Dynamic WebProcesses. 2005.
[36] Duan zhenhua, Tian cong. A Unified Model Checking Approach with ProjectionTemporal Logic[C]. Proceedings of ICFEM 2008. Berlin: Springer-Verlag, 2008:167-186.
[37] Ma Yongtao, Duan Zhenhua, Wang Xiaobing, et al. An Interpreter for FramedTempura and its Application[C]. Proceedings of First Joint IEEE/IFIP Symposiumon Theoretical Aspects of Software Engineering. Shanghai: IEEE Press, 2007:251-260.
[38] Duan Zhenhua, Tian Cong, Zhang Li. A Decision Procedure for PropositionalProjection Temporal Logic with Infinite Models[J]. Acta Informatica, 2008, 45(1):43-78.
[39] Duan Zhenhua, Zhang Nan. A Complete Axiomatization of PropositionalProjection Temporal Logic[C]. Proceedings of the 2008 2nd IFIP/IEEEInternational Symposium on Theoretical Aspects of Software Engineering.Washington, DC, USA: IEEE Computer Society, 2008: 271-278.
[40] Duan Zhenhua, Tian Cong. Decidability of Propositional Projection TemporalLogic with Infinite Models[C]. Proceedings of TAMC 2007. Berlin:Springer-Verlag, 2007: 521-532.
[41] Duan Zhenhua. An Extended Interval Temporal Logic and a Framing Techniquefor Temporal Logic Programming[D]. University of Newcastle upon Tyne, 1996.
[42]雷丽晖,段振华.使用扩展区间时序逻辑为并发工作流建模[J].西安电子科技大学学报(自然科学版), 2007, 34(4): 673-680.
[43]雷丽晖,段振华.基于扩展投影时序逻辑的组合Web服务描述与验证[J].西安交通大学学报, 2007, 41(10): 1155-1159.
[44]张海宾,段振华.混合投影时序逻辑与混合系统的形式化验证[J].计算机科学, 2007, 34(11): 279-282.
[45] Kono Shinji. A Combination of Clausal and Non Clausal Temporal LogicPrograms[C]. Proceedings of the Workshop on Executable Modal and TemporalLogics. Berlin: Springer-Verlag, 1993: 40-57.
[46] Fisher Michael, Owens Richard. An Introduction to Executable Modal andTemporal Logics[C]. IJCAI '93: Proceedings of the Workshop on ExecutableModal and Temporal Logics. London, UK: Springer-Verlag, 1995: 1-20.
[47] Barringer Howard, Fisher Michael, Gabbay Dov M., et al. Metatem: AFramework for Programming in Temporal Logic[C]. REX Workshop. 1989:94-129.
[48] Fisher Michael, Owens Richard. From the Past to the Future: Executing TemporalLogic Programs[C]. Proceedings of Logic Programming and Automated Reasoning.Springer Verlag, 1992: 369-380.
[49] Lamport Leslie. Tla+[R]. DEC Digital Systems, 1995.
[50] Lamport Leslie. Specifying Systems : The Tla+ Language and Tools forHardware and Software Engineers[M]. 75 Arlington Street, Suite 300 Boston, MAUSA: Addison-Wesley Longman Publishing Co., Inc., 2002.
[51] Yu Yuan, Manolios Panagiotis, Lamport Leslie. Model Checking Tla+Specifications[C]. London, UK: Springer-Verlag, 1999: 54-66.
[52] Tla+ Tools. https://research.microsoft.com/en-us/um/people/lamport/tla/tools.html.
[53]岳昆,王晓玲,周傲英. Web服务核心支撑技术:研究综述[J].软件学报, 2004,15(03): 428-442.
[54]廖军,谭浩,刘锦德.基于Pi-演算的Web服务组合的描述和验证[J].计算机学报, 2005, 28(04): 635-643.
[55]侯丽珊,金芝,吴步丹.需求驱动的Web服务建模及其验证:一个基于本体的方法[J].中国科学(E辑:信息科学), 2006, 36(10): 1189-1219.
[56] Narayanan Srini, Mc Sheila A. Simulation, Verification and AutomatedComposition of Web Services[C]. Proceedings of the 11th international conferenceon World Wide Web. New York, NY, USA: ACM, 2002: 77-88.
[57]雷丽晖,段振华.一种基于扩展有限自动机验证组合Web服务的方法[J].软件学报, 2007, 18(12): 2981-2990.
[58]饶元,李尊朝.基于XYZ/ADL的Web服务体系结构形式描述[J].系统工程理论与实践, 2006, 26(03): 53-60.
[59]黄正宝,张广泉. UML 2.0顺序图的XYZ/E时序逻辑语义研究[J].计算机科学2006, 33(8): 249-251.
[60]朱雪阳,唐稚松. UML活动图的时序逻辑语义[J].计算机研究与发展, 2005,42(9): 1478-1484.
[61] Duan Zhenhua. Temporal Logic and Temporal Logic Programming[M]. Beijing:Science Press, 2006.
[62] Yang Xiaoxiao, Duan Zhenhua. Operational Semantics of Framed TemporalLogic Programs[C]. Proceedings of SOFSEM 2007. Berlin: Springer-Verlag, 2007:566-578.
[63] Holzmann Gerard J. The Model Checker Spin[J]. IEEE Transactions on SoftwareEngineering, 1997, 23(5): 279-295.
[64] Tian Cong, Duan Zhenhua. Model Checking Propositional Projection TemporalLogic Based On Spin[C]. Proceedings of the 9th international Annual Conf. onFormal Enginnering Method. Berlin: Springer-Verlag, 2007: 246-265.
[65] Zhuo Huang, Jian Zhang. Generating Sat Instances From First-Order Formulas[J].Journal of Software, 2005, 16(03): 327-335.
[66] Jian Zhan. Deciding the Satisfiability of Logical Formulas—Methods, Tools andApplications[M]. Beijing: Science Press, 2000.
[67] Scott Michael L. Programming Language Pragmatics(2nd Edition)[M]. ElsevierInc., 2006.
[68] Sebesta Robert W. Concepts of Programming Languages(7th Edition)[M].Addison-Wesley Longman Publishing Co., Inc., 2006.
[69] Cormen Thomas H., Stein Clifford, Rivest Ronald L., et al. Introduction toAlgorithms[M]. MIT Press, 2001.
[70] Zhang Jian. Symbolic Execution of Program Paths Involving Pointer andStructure Variables[C]. Proceeding of 4th International Conference on QualitySoftware. 2004: 87-92.
[71] Distefano Dino, Katoen Joost- Pieter, Rensink Arend. Safety and Liveness inConcurrent Pointer Programs[J]. Formal Methods for Components and Objects,2006: 280-312.
[72] Distefano Dino, Katoen Joost- Pieter, Rensink Arend. Who is Pointing When toWhom?[C]. Proceedings of FSTTCS 2004. Berlin: Springer-Verlag, 2005:250-262.
[73] Distefano Dino. On Model Checking the Dynamics of Object-Based Software: AFoundational Approach[D]. University of Twente, 2003.
[74] Reynolds J. C. Separation Logic: A Logic for Shared Mutable Data Structures[C].Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science.Washington, DC, USA: IEEE Computer Society, 2002: 55-74.
[75]陈意云,华保健,葛琳,等.一种用于指针程序安全性证明的指针逻辑[J].计算机学报, 2008, 31(3): 372-380.
[76] Wang Zhifang, Chen Yiyun, Wang Zhenming, et al. An Extension to PointerLogic for Verification[C]. TASE '08: Proceedings of the 2008 2nd IFIP/IEEEInternational Symposium on Theoretical Aspects of Software Engineering.Washington, DC, USA: IEEE Computer Society, 2008: 49-56.
[77] Marti Nicolas, Affeldt Reynald, Yonezawa Akinori. Formal Verification of theHeap Manager of an Operating System Using Separation Logic[J]. FormalMethods and Software Engineering, 2006: 400-419.
[78] Li Guang-yuan, Tang Zhi-song. Formalization and Verification of Pointers in theTemporal Logic Language Xyz/E Programs[J]. Journal of Software, 2000, 11(3):285-292.
[79]王小兵,段振华.框架投影时序逻辑程序设计语言中的指针[J].西安电子科技大学学报(自然科学版), 2008, 35(06): 1069-1074.
[80] Zhenhua Duan, Xiaobing Wang. Implementing Pointer in Temporal LogicProgramming Languages[C]. Proceedings of Brazilian Symposium on FormalMethods. Natal, Brazil: The Brazilian Symposium on Formal Methods, 2006:171-184.
[81]苏云霖.编译原理[M].机械工业出版社, 2008.
[82] Zhu, H. And Zhou M. c. Object-Oriented Programming with C++: AProject-Based Approach[M]. Beijing: Tsinghua University Press, 2006.
[83] Hoare C. a. r., Jifeng He. Unified Theories of Programming[M]. Prentice Hall,1998.
[84] Santos Thiago, Cavalcanti Ana, Sampaio Augusto. Object-Orientation in theUtp[C]. Proceedings of UTP 2006. Berlin: Springer-Verlag, 2006: 18-37.
[85] Jifeng He, Li Xiaoshan, Liu Zhiming. Rcos: A Refinement Calculus of ObjectSystems[J]. Theoretical Computer Science, 2006, 365(1): 109-142.
[86] Morgan Carroll. Programming From Specifications[M]. Upper Saddle River, NJ,USA: Prentice-Hall, 1990.
[87] Quan Long, Zongyan Qiu, Zhiming Liu, Lingshuang Shao And He Jifeng. Post: ACase Study for Rcos Incremental Development[R]. Macau: United NationsUniversity International Institute for Software Technology, 2005.
[88] Abadi Mart, Leino K. Rustan. A Logic of Object-Oriented Programs[C].Proceedings of TAPSOFT 1997. Berlin: Springer-Verlag, 1997: 11-41.
[89] Spivey J. M. An Introduction to Z and Formal Specifications[J]. SoftwareEngineering Journal, 1989, 4(1): 40-50.
[90]缪淮扣,李刚,朱关铭.软件工程语言—Z[M].上海:上海科学技术文献出版社, 1999.
[91] Smith Graeme. The Object-Z Specification Language[M]. Kluwer AcademicPublishers, 2000.
[92] Duke Roger, Rose Gordon. Formal Object-Oriented Specification UsingObject-Z[M]. MacMillan, 2000.
[93] D Eug, Van Katwijk Jan. Vdm++: A Formal Specification Language forObject-Oriented Designs[C]. Hertfordshire, UK: Prentice Hall International Ltd.,1992: 63-77.
[94]吴哲辉. Petri网导论[M].北京:机械工业出版社, 2006.
[95] Coleman Derek, Hayes Fiona, Bear Stephen. Introducing Objectcharts Or How toUse Statecharts in Object-Oriented Design[J]. IEEE Transactions on SoftwareEngineering, 1992, 18(1): 9-18.
[96] Wang Li-chih. Object-Oriented Petri Nets for Modelling and Analysis ofAutomated Manufacturing Systems[J]. Computer Integrated ManufacturingSystems, 1996, 9(2): 111-125.
[97]熊毅,左志宏,周明天.面向对象的命题逻辑和分布式推理[J].计算机科学,2004, 31(2): 104-108.
[98] Amir Eyal. Object-Oriented First-Order Logic[C]. Proceedings of the IJCAI 1999.Murray Hill, New Jersey: International Joint Conference on Artificial Intelligence,1999: 1-8.
[99]李平福,陈冬火,张广泉.面向对象系统的时序逻辑描述[J].苏州大学学报(工科版), 2008, 28(04): 12-19.
[100]郭亮,唐稚松. XYZ/E面向对象程序语义概述[J].软件学报, 2003, 14(3):356-361.
[101]王小兵,段振华.面向对象的时序逻辑语言[J].电子科技大学学报(自然科学版), 2009, 38(01): 97-101.
[102] The Lex & Yacc Page. http://dinosaur.compilertools.net/.
[103] Ruby. http://www.ruby-lang.org/en/.
[104] Python. http://www.python.org/.
[105] Liu Shaoying. Formal Engineering for Industrial Software Development[M].SpringerVerlag, 2004.
[106]林惠民,张文辉.模型检测:理论、方法与应用[J].电子学报, 2002(S1):1907-1912.
[107] Pierce Benjamin C. Types and Programming Languages[M]. Cambridge: MITPress, 2002.
[108] Web Services Description Language (Wsdl) 1.1[EB/OL]. 2001.
[109] Oasis Uddi Specifications Tc - Committee Specifications[EB/OL]. http://www.oasis-open.org/committees/uddi-spec/doc/tcspecs.htm,
[110] Web Services Business Process Execution Language Version 2.0[EB/OL]. http://docs.oasis-open.org/wsbpel/2.0/CS01/wsbpel-v2.0-CS01.html, 2007.
[111] Web Service Choreography Interface (Wsci) 1.0[EB/OL]. http://www.w3.org/TR/wsci/, 2002.
[112] Owl-S: Semantic Markup for Web Services[EB/OL]. http://www.w3.org/Submission/OWL-S/, 2004.
[113]刘如娟,戴桂兰,胡长军,等. Web服务的模型检测技术探讨[J].小型微型计算机系统, 2007, 28(11): 1921-1927.
[114] Ankolekar Anupriya, Paolucci Massimo, Sycara Katia. Towards a FormalVerification of Owl-S Process Models[C]. Proceedings of ISWC 2005. Berlin:Springer-Verlag, 2005: 37-51.
[115] Clarke E., Grumberg O., Long D. Verification Tools for Finite-State ConcurrentSystems[J]. A Decade of Concurrency Reflections and Perspectives, 1994:124-175.
[116] M. Panti,l. Spalazzi s. Tacconi. Using the Nusmv Model Checker to Verify theKerberos Protocol[C]. Proceeding of the 3rd Collaborative TechnologiesSymposium. 2002: 27-31.
[117] Pettersson Paul, Larsen Kim G. Uppaal2k[J]. Bulletin of the EuropeanAssociation for Theoretical Computer Science (EATCS), 2000, 70: 40-44.
[118] Schmidt Karsten. Lola: A Low Level Analyser[C]. Proceedings of 21stInternational Conference on Application and Theory of Petri Nets(ICATPN 2000).Springer-Verlag, 2000: 465-474.
[119] Cleaveland Rance, Sims Steve. The Ncsu Concurrency Workbench[C]. CAV '96:Proceedings of the 8th International Conference on Computer Aided Verification.London, UK: Springer-Verlag, 1996: 394-397.
[120] Sala Gwen, Bordeaux Lucas, Schaerf Marco. Describing and Reasoning On WebServices Using Process Algebra[C]. ICWS '04: Proceedings of the IEEEInternational Conference on Web Services. Washington, DC, USA: IEEEComputer Society, 2004: 43-50.
[121] Hinz Sebastian, Schmidt Karsten, Stahl Christian. Transforming Bpel to PetriNets[C]. Proceedings of 3rd International Conference BPM. Springer Verlag, 2005:220-235.
[122] Schmidt Karsten, Stahl Christian. A Petri Net Semantic for Bpel4ws - Validationand Application[C]. Proceedings of the 11th Workshop on Algorithms and Toolsfor Petri Nets (AWPN'04),. University Paderborn, 2004: 1-6.
[123] Fu Xiang, Bultan Tevfik, Su Jianwen. Wsat: A Tool for Formal Analysis of WebServices[C]. Proceedings of 16th International Conference on Computer AidedVerification (CAV 2004). Springer, 2004: 510-514.
[124]蒋运承,史忠植. OWL-S的形式语义[J].计算机科学, 2005, 34(07): 5-7.
[125]王杰生,李舟军,李梦君.用描述逻辑进行语义Web服务组合[J].软件学报,2008, 19(04): 967-980.
[126] Solanki Monika, Cau Antonio, Zedan Hussein. Asdl: A Wide Spectrum Languagefor Designing Web Services[C]. Proceedings of the 15th international conferenceon World Wide Web(WWW 2006). New York, NY, USA: ACM, 2006: 687-696.
[127] Solanki Monika. A Compositional Framework for the Specification, Verificationand Runtime Validation of Reactive Web Services[D]. De Montfort University,Leicester, UK, 2005.
[128] An Ontology for Itl and Tempura. http://www.cse.dmu.ac.uk/~monika/Pages/Ontologies/OntoITL.owl.
[129]王小兵,段振华.面向投影时序逻辑的Web服务模型检测[J].西安交通大学学报, 2009, 43(04): 39-43.
[130] Pvs. http://pvs.csl.sri.com/.
[131] The Hol System. http://www.cl.cam.ac.uk/research/hvg/HOL/.