Object-oriented MSVL And Its Application To Verification Of Composite Web Services

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.