Publications in Verification

Articles in Refereed Journals:

1. L. Baresi, D. Bianculli, C. Ghezzi, S. Guinea, P. Spoletini. Validation of web service compositions. IET Software, Vol. 1, Num. 6, pages 219-232, December 2007.
   Abstract: Web services support software architectures that can evolve dynamically. In particular, in this paper the focus is on architectures where services are composed (orchestrated) through a workflow described in the business process execution language (BPEL). It is assumed that the resulting composite service refers to external services through assertions that specify their expected functional and non-functional properties. On the basis of these assertions, the composite service may be verified at design time by checking that it ensures certain relevant properties. Because of the dynamic nature of web services and the multiple stakeholders involved in their provision, however, the external services may evolve dynamically, and even unexpectedly. They may become inconsistent with respect to the assertions against which the workflow was verified during development. As a consequence, validation of the composition must extend to run time. In this work, an assertion language, called assertion language for BPEL process interactions (ALBERT), is introduced; it can be used to specify both functional and non-functional properties. An environment which supports design-time verification of ALBERT assertions for BPEL workflows via model checking is also described. At run time, the assertions can be turned into checks that a software monitor performs on the composite system to verify that it continues to guarantee its required properties. A TeleAssistance application is provided as a running example to illustrate our validation framework.

2. Bianculli, D., Ghezzi, C., Spoletini, P.. A Model Checking Approach to Verify BPEL4WS Workflows. Service-Oriented Computing and Applications, 2007. SOCA '07. IEEE International Conference on, To Appear, June 2007.
   Abstract: The increasing diffusion of service oriented computing in critical business transactions demands reliability and correctness of the workflow logic representing web service orchestrations. We present an approach for the formal verification of workflow-based compositions of web services, described in BPEL4WS. Workflow processes can be verified in isolation, assuming that the external services invoked are known only through their interface. It is also possible to verify that the actual composition of two or more processes behaves correctly. We can verify deadlock freedom, properties expressed as data-bound assertions written in WS-CoL, a specification language for web services, and LTL temporal properties. Our approach is based on the software model checker Bogor, whose language supports the modeling of all BPEL4WS constructs. We provide an empirical evaluation of our approach and we compare the results with other BPEL4WS model checking tools.

3. Chun Ouyanga, Eric Verbeekb, Wil M.P. van der Aalst, Stephan Breutel, Marlon Dumas, Arthur H.M. ter Hofstede. Formal semantics and analysis of control flow in WS-BPEL. Science of Computer Programming, Vol. 67, Num. 2-3, pages 162-198, April 2007.
   Abstract: Web service composition refers to the creation of new (Web) services by combining functionalities provided by existing ones. A number of domain-specific languages for service composition have been proposed, with consensus being formed around a process-oriented language known as WS-BPEL (or BPEL). The kernel of BPEL consists of simple communication primitives that may be combined using control-flow constructs expressing sequence, branching, parallelism, synchronization, etc. We present a comprehensive and rigorously defined mapping of BPEL constructs onto Petri net structures, and use this for the analysis of various dynamic properties related to unreachable activities, conflicting messages, garbage collection, conformance checking, and deadlocks and lifelocks in interaction processes. We use a mapping onto Petri nets because this allows us to use existing theoretical results and analysis tools. Unlike approaches based on finite state machines, we do not need to construct the state space, and can use structural analysis (e.g., transition invariants) instead. We have implemented a tool that translates BPEL processes into Petri nets and then applies Petri-net-based analysis techniques. This tool has been tested on different examples, and has been used to answer a variety of questions.

4. Wil M. P. van der Aalst. Business alignment: using process mining as a tool for Delta analysis and conformance testing. Requir. Eng., Vol. 10, Num. 3, pages 198-211, 2005.
   Abstract: Increasingly, business processes are being controlled and/or monitored by information systems. As a result, many business processes leave their "footprints" in transactional information systems, i.e., business events are recorded in so-called event logs. Process mining aims at improving this by providing techniques and tools for discovering process, control, data, organizational, and social structures from event logs, i.e., the basic idea of process mining is to diagnose business processes by mining event logs for knowledge. In this paper we focus on the potential use of process mining for measuring business alignment, i.e., comparing the real behavior of an information system or its users with the intended or expected behavior. We identify two ways to create and/or maintain the fit between business processes and supporting information systems: Delta analysis and conformance testing. Delta analysis compares the discovered model (i.e., an abstraction derived from the actual process) with some predefined processes model (e.g., the workflow model or reference model used to configure the system). Conformance testing attempts to quantify the "fit" between the event log and some predefined processes model. In this paper, we show that Delta analysis and conformance testing can be used to analyze business alignment as long as the actual events are logged and users have some control over the process.

5. Mariya Koshkina, Franck van Breugel. Modelling and verifying web service orchestration by means of the concurrency workbench. SIGSOFT Softw. Eng. Notes, Vol. 29, Num. 5, pages 1-10, ACM, 2004.
   Abstract: Verification techniques like model checking, preorder checking and equivalence checking are shown to be relevant to web service orchestration. The Concurrency Workbench of the New Century (CWB) is a verification tool that supports these verification techniques. By means of the Process Algebra Compiler (PAC), the CWB is modified to support the BPE-calculus. The BPE-calculus is a small language, based on BPEL4WS, to express web service orchestration. Both the syntax and the semantics of the BPE-calculus are formally defined. These are subsequently used as input for the PAC. As output, the PAC produces modules that are incorporated into the CWB so that it supports the BPE-calculus and, hence, provides a verification tool for web service orchestration.

6. Marco Pistore, Marco Roveri, Paolo Busetta. Requirements-Driven Verification of Web Services. Electr. Notes Theor. Comput. Sci., Vol. 105, pages 95-108, 2004.
   Abstract: We propose a requirements-driven approach to the design and verification of Web services. The proposed methodology starts from a requirements model, which defines a business domain at a "strategic" level, describing the participating actors, their mutual dependencies, goals, requirements, and expectations. This business requirements model is then refined into a business process model. In this refinement, definitions of the processes carried out by the actors of the domain are added to the model in the form of BPEL4WS code. We show how to exploit model checking techniques for the verification of the specification, both at the requirements and at the process level. At the requirements level, model checking is used to validate the specification against a set of queries specified by the designer; at the process level, it is used to verify if the BPEL4WS processes satisfy the constraints described in the requirements model.

7. Gian Luigi Ferrari, Stefania Gnesi, Ugo Montanari, Marco Pistore. A model-checking verification environment for mobile processes. ACM Trans. Softw. Eng. Methodol., Vol. 12, Num. 4, pages 440-473, 2003.
   Abstract: This article presents a semantic-based environment for reasoning about the behavior of mobile systems. The verification environment, called HAL, exploits a novel automata-like model that allows finite-state verification of systems specified in the $\pi$-calculus. The HAL system is able to interface with several efficient toolkits (e.g. model-checkers) to determine whether or not certain properties hold for a given specification. We report experimental results on some case studies.

Articles in Refereed Conferences:

1. A. Rozinat, W.M.P. van der Aalst. Conformance Testing: Measuring the Fit and Appropriateness of Event Logs and Process Models. Business Process Management Workshops, Lecture Notes in Computer Science, Vol. 3812, pages 163-176, February 2006.
   Abstract: Most information systems log events (e.g., transaction logs, audit trails) to audit and monitor the processes they support. At the same time, many of these processes have been explicitly modeled. For example, SAP R/3 logs events in transaction logs and there are EPCs (Event-driven Process Chains) describing the so-called reference models. These reference models describe how the system should be used. The coexistence of event logs and process models raises an interesting question: "Does the event log conform to the process model and vice versa?". This paper demonstrates that there is not a simple answer to this question. To tackle the problem, we distinguish two dimensions of conformance: fitness (the event log may be the result of the process modeled) and appropriateness (the model is a likely candidate from a structural and behavioral point of view). Different metrics have been defined and a Conformance Checker has been implemented within the ProM Framework.

2. Wil M. P. van der Aalst, Marlon Dumas, Chun Ouyang, Anne Rozinat, H. M. W. Verbeek. Choreography Conformance Checking: An Approach based on BPEL and Petri Nets. The Role of Business Processes in Service Oriented Architectures, 2006.
   Abstract: Recently, languages such as BPEL and CDL have been proposed to describe the way services can interact from a behavioral perspective. The emergence of these languages heralds an era where richer service descriptions, going beyond WSDL-like interfaces, will be available. However, what can these richer service descriptions serve for? This paper investigates a possible usage of behavioral service descriptions, namely as input for conformance checking. Conformance checking is the act of verifying whether one or more parties stick to the agreed-upon behavior by observing the actual behavior, e.g., the exchange of messages between all parties. This paper shows that it is possible to translate BPEL business protocols to Petri nets and to relate SOAP messages to transitions in the Petri net. As a result, Petri net-based conformance checking techniques can be used to quantify fitness (whether the observed behavior is possible in the business protocol) and appropriateness (whether the observed behavior "overfits" or "underfits" the business protocol). Moreover, non-conformance can be visualized to pinpoint deviations. The approach has been implemented in the context of the ProM n framework.

3. Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello, Marco Montali, Sergio Storari, Paolo Torroni. Computational Logic for Run-Time Verification of Web Services Choreographies: Exploiting the OCS-SI Tool. WS-FM, pages 58-72, 2006.
   Abstract: In this work, we investigate the feasibility of using a framework based on computational logic, and mainly defined in the context of Multi-Agent Systems for Global Computing (SOCS UE Project), for modeling choreographies of Web Services with respect to the conversational aspect. One of the fundamental motivations of using computational logic, beside its declarative and highly expressive nature, is given by its operational counterpart, that can provide a proof-theoretic framework able to verify the consistency of services designed in a cooperative and incremental manner. In particular, in this paper we show that suitable "Social Integrity Constraints", introduced in the SOCS social model, can be used for specifying global protocols at the choreography level. In this way, we can use a suitable tool, derived from the proof-procedure defined in the context of the SOCS project, to check at run-time whether a set of existing services behave in a conformant manner w.r.t. the defined choreography.

4. Howard Foster, Sebastian Uchitel, Jeff Magee, Jeff Kramer. LTSA-WS: a tool for model-based verification of web service compositions and choreography. ICSE '06: Proceedings of the 28th international conference on Software engineering, pages 771-774, ACM, 2006.
   Abstract: In this paper we describe a tool for a model-based approach to verifying compositions of web service implementations. The tool supports verification of properties created from design specifications and implementation models to confirm expected results from the viewpoints of both the designer and implementer. Scenarios are modeled in UML, in the form of Message Sequence Charts (MSCs), and then compiled into the Finite State Process (FSP) process algebra to concisely model the required behavior. BPEL4WS implementations are mechanically translated to FSP to allow an equivalence trace verification process to be performed. By providing early design verification and validation, the implementation, testing and deployment of web service compositions can be eased through the understanding of the behavior exhibited by the composition. The approach is implemented as a plug-in for the Eclipse development environment providing cooperating tools for specification, formal modeling, verification and validation of the composition process.

5. Raman Kazhamiakin, Paritosh K. Pandya, Marco Pistore. Representation, Verification, and Computation of Timed Properties in Web Service Compositions. ICWS, pages 497-504, 2006.
   Abstract: In this paper we address the problem of qualitative and quantitative analysis of timing aspects of Web service compositions defined as a set of BPEL4WS processes. We introduce a formalism, called Web Service Timed State Transition Systems (WSTTS), to capture the timed behavior of the composite web services. We also exploit an interval temporal logic to express complex timed assumptions and requirements on the system's behavior. Building on top of this formalization, we provide techniques and tools for modelchecking BPEL4WS compositions against time-related requirements. We also present a symbolic algorithm that can be used to compute duration bounds of behavioral intervals that satisfy such requirements. We perform a preliminary experimental evaluation of our approach and tools with the help of an e-Government case study.

6. Marina Mongiello, Daniela Castelluccia. Modelling and verification of BPEL business processes. Fourth Workshop on Model-Based Development of Computer-Based Systems, 2006.
   Abstract: A business process is a complex Web service with functions provided by different Web services, which are already existing in Web and are dynamically integrated for granting a more complex business task. For this reason, business processes have become more and more diffuse in B2B and B2C domains, so that the importance of their activities asks for a high-level of reliability. Methods and tools for supporting automatic system verification and validation could be useful. Among the techniques of automatic verification, we choose model checking method, because we applied it efficiently for verification of a single Web service and in this paper we extend the area of application also in business processes. Descriptions of the behavior of a business process are coded using a standard language, BPEL4WS, that has broadly spread because it is able to describe a business process as both an executable process and an abstract process. Therefore, we model a BPEL description of a generic business process with a formal model and we formalize correctness properties about the reliability of the business process design. Also, we build a framework that performs automatic verification of formal models of business processes through NuSMV model checker. If there is a violation of correctness specifications, NuSMV provides counter-examples, so we can locate errors and effect right changes for correcting business process design.

7. Mohsen Rouached, Olivier Perrin, Claude Godart. Towards Formal Verification of Web Service Composition. Business Process Management, pages 257-273, 2006.
   Abstract: Web services composition is an emerging paradigm for enabling application integration within and across organizational boundaries. Current Web services composition proposals, such as BPML, WSBPEL, WSCI, and OWL-S, provide solutions for describing the control and data flows in Web service composition. However, such proposals remain at the descriptive level, without providing any kind of mechanisms or tool support for analysis and verification. Therefore, there is a growing interest for the verification techniques which enable designers to test and repair design errors even before actual running of the service, or allow designers to detect erroneous properties and formally verify whether the service process design does have certain desired properties. In this paper, we propose to verify Web services composition using an event driven approach. We assume Web services that are coordinated by a composition process expressed in WSBPEL and we use Event Calculus to specify the properties and requirements to be monitored.

8. Huang, H., Tsai, W.-T., Paul, R.. Automated model checking and testing for composite Web services. pages 300-307, May 2005.
   Abstract: Web services form a new distributed computing paradigm. Collaborative verification and validation are important when Web services from different vendors are integrated together to carry out a coherent task. This paper presents a new approach to verify Web services by model checking the process model of OWL-S (Web ontology language for Web services) and to validate them by the test cases automatically generated in the model checking process. We extend the BLAST, a model checker that handles control flow model naturally, to handle the concurrency in OWL-S. We also propose enhancement in OWL-S and PDDL (Planning Domain Definition Language) to facilitate the automated test case generation. Experiments on realistic examples are provided to illustrate the process.

9. Bernd-Holger Schlingloff, Axel Martens, Karsten Schmidt. Modeling and Model Checking Web Services. Vol. 126, pages 3-26, Elsevier, March 2005.
   Abstract: We give an overview on web services and the web service technology stack. We then show how to build Petri net models of web services formulated in the specification language BPEL4WS. We define an abstract correctness criterion for these models and study the automated verification according to this criterion. Finally, we relate correctness of web service models to the model checking problem for alternating temporal logics.

10. Aysu Betin-Can, Tevfik Bultan, Xiang Fu. Design for verification for asynchronously communicating Web services. WWW, pages 750-759, 2005.
    Abstract: We present a design for verification approach to developing reliable web services. We focus on composite web services which consist of asynchronously communicating peers. Our goal is to automatically verify properties of interactions among such peers. We propose a design pattern that eases the development of such web services and enables a modular, assume-guarantee style verification strategy. In the proposed design pattern, each peer is associated with a behavioral interface description which specifies how that peer will interact with other peers. Using these peer interfaces we automatically generate BPEL specifications to publish for interoperability. Assuming that the participating peers behave according to their interfaces, we verify safety and liveness properties about the global behavior of the composite web service during behavior verification. During interface verification, we check that each peer implementation conforms to its interface. Using the modularity in the proposed design pattern, we are able to perform the interface verification of each peer and the behavior verification as separate steps. Our experiments show that, using this modular approach, one can automatically and efficiently verify web service implementations.

11. Hai Huang, Wei-Tek Tsai, Raymond Paul, Yinong Chen. Automated Model Checking and Testing for Composite Web Services.. 8th IEEE International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC 2005), pages 300-307, IEEE Computer Society, 2005.
    Abstract: Web Services form a new distributed computing paradigm. Collaborative verification and validation are important when Web Services from differen vendors are integrated together to carry out a coherent task. This paper presents a new approach to verify Web Services by model checking the proces model of OWL-S (Web Ontology Language for Web Services) and to validate them by the test cases automatically generated in the model checking process. We extend the BLAST, a model checker tha handles control flow model naturally, to handle the concurrency in OWL-S. We also propose enhancement in OWL-S and PDDL (Planning Domain Definition Language) to facilitate the automated test case generation. Experiments on realistic examples are provided to illustrate the process.

12. Wei-Tek Tsai, Yinong Chen, Raymond A. Paul. Specification-Based Verification and Validation of Web Services and Service-Oriented Operating Systems. WORDS, pages 139-147, 2005.
    Abstract: Service-Oriented Architecture (SOA) and Web Services (WS) have received significant attention recently. Even though WS are based on open standards and support software interoperability, but the trustworthy issues of WS has actually limited the growth of WS applications as organizations do not trust those WS developed by other vendors and at the same time they do not have access to the source code. This paper addressed this issue by proposing several solutions including specification-based verification and validation, collaborative testing, and group testing. The key concept is that it is possible to provide a comprehensive evaluation of WS even if their source code is not available.

13. Foster, H., Uchitel, S., Magee, J., Kramer, J.. Compatibility verification for Web service choreography. pages 738-741, July 2004.
    Abstract: In this paper we discuss a model-based approach to verifying process interactions for coordinated Web service compositions. The approach uses finite state machine representations of Web service orchestrations and assigns semantics to the distributed process interactions. The move towards implementing Web service compositions by multiple interested parties as a form of distributed system architecture motivates the need for supporting compatibility verification of activities and transactions in all the processes. The described approach is supported by a suite of cooperating tools for specification, formal modeling and providing verification results from orchestrated Web service interactions.

14. Jesus Arias-Fisteus, Luis Sanchez Fernandez, Carlos Delgado Kloos. Formal Verification of BPEL4WS Business Collaborations. E-Commerce and Web Technologies, 5th International Conference, EC-Web 2004, Proceedings, Lecture Notes in Computer Science, Vol. 3182, pages 76-85, Springer Verlag, 2004.
    Abstract: Web services are a very appropriate communication mechanism to perform distributed business processes among several organisations. These processes should be reliable, because a failure in them can cause high economic losses. To increase their reliability at design time, we have developed VERBUS, a framework for the formal verification of business processes. VERBUS can automatically translate business process definitions to specifications verifiable in several available tools. It is based on a modular and extensible architecture: new process definition languages and verification tools can be added easily to the framework. The prototype of VERBUS presented in this work can verify BPEL4WS process specifications, by translating them to Promela. The Promela specifications are verified with the well known model checker Spin. In this paper we describe the general architecture of VERBUS and how BPEL4WS specifications are translated and verified. The explanation is completed by describing what types of properties can be verified and providing an overview of the implementation.

15. Tevfik Bultan, Xiang Fu, Jianwen Su. Tools for Automated Verification of Web Services. ATVA, pages 8-10, 2004.

16. Xiang Fu, Tevfik Bultan, Jianwen Su. Analysis of Interacting BPEL Web Services. WWW'04: Proceedings of the 13th International Conference on World Wide Web, pages 621-630, ACM Press, 2004.
    Abstract: This paper presents a set of tools and techniques for analyzing interactions of composite web services which are specified in BPEL and communicate through asynchronous XML messages. We model the interactions of composite web services as conversations, the global sequence of messages ex- changed by the web services. As opposed to earlier work, our tool-set handles rich data manipulation via XPath expressions. This allows us to verify designs at a more detailed level and check properties about message content. We present a framework where BPEL specifications of web ser- vices are translated to an intermediate representation, followed by the translation of the intermediate representation to a verification language. As an intermediate representation we use guarded automata augmented with unbounded queues for incoming messages, where the guards are expressed as XPath expressions. As the target verification language we use Promela, input language of the model checker SPIN. Since SPIN model checker is a finite-state verification tool we can only achieve partial verification by fixing the sizes of the input queues in the translation. We propose the concept of synchronizability to address this problem. We show that if a composite web service is synchronizable, then its conversation set remains same when asynchronous communication is replaced with synchronous communication. We give a set of sufficient conditions that guarantee synchronizability and that can be checked statically. Based on our synchronizability results, we show that a large class of composite web services with unbounded input queues can be completely verified using a finite state model checker such as SPIN.

17. Xiang Fu, Tevfik Bultan, Jianwen Su. Model checking XML manipulating software. ISSTA, pages 252-262, 2004.
    Abstract: The use of XML as the de facto data exchange standard has allowed integration of heterogeneous web based software systems regardless of implementation platforms and programming languages. On the other hand, the rich tree-structured data representation, and the expressive XML query languages (such as XPath) make formal specification and verification of software systems that manipulate XML data a challenge. In this paper, we present our initial efforts in automated verification of XML data manipulation operations using the SPIN model checker. We present algorithms for translating (bounded) XML data and XPath expressions to Promela, the input language of SPIN. The techniques presented in this paper constitute the basis of our Web Service Analysis Tool (WSAT) which verifies LTL properties of composite web services.

18. Howard Foster, Sebastián Uchitel, Jeff Magee, Jeff Kramer. Model-based Verification of Web Service Compositions.. 18th IEEE International Conference on Automated Software Engineering (ASE 2003) , pages 152-163, IEEE Computer Society, 2003.
    Abstract: In this paper we discuss a model-based approach to verifying web service compositions for web service implementations. The approach supports verification against specification models and assigns semantics to the behavior of implementation models so as to confirm expected results for both the designer and implementer. Specifications of the design are modeled in UML, in the form of Message Sequence Charts (MSCs), and mechanically compiled into the Finite State Process notation (FSP) to concisely describe and reason about the concurrent programs. Implementations are mechanically translated to FSP to allow a trace equivalence verification process to be performed. By providing early design verification, the implementation, testing and deployment of web service compositions can be eased through the understanding of the differences, limitations and undesirable traces allowed by the composition. The approach is supported by a suite of cooperating tools for specification, formal modeling and trace animation of the composition workflow.

19. Srini Narayanan, Sheila A. McIlraith. Simulation, verification and automated composition of web services. WWW '02: Proceedings of the 11th international conference on World Wide Web, pages 77-88, ACM, 2002.
    Abstract: Web services - Web-accessible programs and devices - are a key application area for the Semantic Web. With the proliferation of Web services and the evolution towards the Semantic Web comes the opportunity to automate various Web services tasks. Our objective is to enable markup and automated reasoning technology to describe, simulate, compose, test, and verify compositions of Web services. We take as our starting point the DAML-S DAML+OIL ontology for describing the capabilities of Web services. We define the semantics for a relevant subset of DAML-S in terms of a first-order logical language. With the semantics in hand, we encode our service descriptions in a Petri Net formalism and provide decision procedures for Web service simulation, verification and composition. We also provide an analysis of the complexity of these tasks under different restrictions to the DAML-S composite services we can describe. Finally, we present an implementation of our analysis techniques. This implementation takes as input a DAML-S description of a Web service, automatically generates a Petri Net and performs the desired analysis. Such a tool has broad applicability both as a back end to existing manual Web service composition tools, and as a stand-alone tool for Web service developers.

20. Wil M. P. van der Aalst. Workflow Verification: Finding Control-Flow Errors Using Petri-Net-Based Techniques. Business Process Management, pages 161-183, 2000.
    Abstract: Workflow management systems facilitate the everyday operation of business processes by taking care of the logistic control of work. In contrast to traditional information systems, they attempt to support frequent changes of the workflows at hand. Therefore, the need for analysis methods to verify the correctness of workflows is becoming more prominent. In this chapter we present a method based on Petri nets. This analysis method exploits the structure of the Petri net to find potential errors in the design of the workflow. Moreover, the analysis method allows for the compositional verification of workflows.

Books and Monographs:

1. Mariya Koshkina. Verification of Business Processes for Web Services. Ms. Thesis, York University - Department of Computer Science, October 2003.
   Abstract: The Business Process Execution Language for Web Services (BPEL4WS or simply BPEL) is a recently developed language, which is used to specify interactions between web services. Among its features it allows specification of concurrent behavior. Erroneous specification can lead to such problems as deadlock. In our research we focus on the concurrency mechanism in BPEL. Our main goal is to analyze processes in order to detect possible deadlocks. To achieve this we introduce a process algebra called the BPE-calculus. It is a small language which captures all the BPEL features relevant to the analysis. This process algebra is modelled using a labeled transition system. An existing verification tool called the Concurrency Workbench is customized to use our BPE-calculus. This tool allows us to verify many properties of BPE-calculus processes specified in a logic called the mu-calculus, including deadlock freedom.

Articles in Books and Other Collections:

1. Natasha Sharygina, Daniel Kröning. Model Checking with Abstraction for Web Services. Test and Analysis of Web Services, pages 121-145, 2007.
   Abstract: Web services are highly distributed programs and, thus, are prone to concurrency-related errors. Model checking is a powerful technique to identify flaws in concurrent systems. However, the existing model checkers have only very limited support for the programming languages and communication mechanisms used by typical implementations of web services. This chapter presents a formalization of communication semantics geared for web services, and an automated way to extract formal models from programs implementing web services for automatic formal analysis. The formal models are analyzed by means of a symbolic model checker that implements automatic abstraction refinement. Our implementation takes one or more PHP5 programs as input, and is able to verify joint properties of these programs running concurrently.

Publications in Refereed Workshops:

1. S. Nakajima. Model-Checking Behavioral Specification of BPEL Applications. Proceedings of the International Workshop on Web Languages and Formal Methods, WLFM 2005, 2005.
   Abstract: To provide a framework to compose lots of specialised services flexibly, BPEL is proposed to describe Web service flows. Since the Web service flow description is basically a distributed collaboration, writing correct programs in BPEL is not easy. Verifying BPEL program prior to its execution is essential. This paper proposes a method to extract the behavioral specification from a BPEL appliation program and to analyze it by using the SPIN model checker. With the adequate abstraction method and support for DPE, the method can analyze all the four example cases in the BPEL standard document.

2. S. Nakajima. Model-Checking Verification for Reliable Web Service. OOPSLA Workshop on Object-Oriented Web Services, 2002.
   Abstract: Model-checking is a promising technique for the verification and validation of software systems. Web service, an emerging technology in the Internet, is an autonomous server that may offer an individual service. It sometimes requires to combine more than one to meet our requirements. WSFL(Web Services Flow Language) is proposed as a language to provide means to describe Web service aggregation. We are interested in how much the software model-checking technique can be used as a basis for raising reliability of Web service, Web service flow descriptions in particular. Our experience shows that faulty flow descriptions can be identified with the proposed method. The method is also very helpful in studying an alternative semantics of the WSFL in regard to the handling of dataflows.