Publications in Formal Methods

Articles in Refereed Journals:

1. 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.

2. Roberto Lucchi, Manuel Mazzara. A pi-calculus based semantics for WS-BPEL . Journal of Logic and Algebraic Programming, Vol. 70, Num. 1, pages 96-118, January 2007.
   Abstract: Recently, the term Web services orchestration has been introduced to address some issues related to Web services composition, that is the way of defining a complex service out of simpler ones. Several proposals for describing orchestration for business processes have been presented in the last years and many of these languages make use of concepts as long-running transactions and compensations for coping with error handling. WS-BPEL 2.0, the most credited candidate for becoming a standard, provides three different mechanisms allowing to cope with abnormal situations: exception, event and compensation handling. This complexity makes it difficult to formally define the framework, thus limiting the formal reasoning about the designed applications. In this paper we advocate that three different mechanisms for error handling are not necessary and we formalize a novel orchestration language based on the idea of event notification as the unique error handling mechanism. To this end, we formally define the three BPEL mechanisms in terms of our calculus. It is possible to take advantages of this formal description in two ways. Firstly, this language represents by itself a proposal of simplification for WS-BPEL 2.0 including an unambiguous specification. Secondly, an implementor of an actual WS-BPEL 2.0 orchestration engine could implement simply this single mechanism providing all the remaining ones by compilation. With this attempt we intend to give a concrete contribute towards the improvement of the quality of the BPEL specification, the applicability of BPEL itself and the implementation of real orchestration engines. Finally, as a case study we consider some of the hundreds of open issues met by the WS-BPEL designers and we propose a solution making use of the experience gained developing our algebra.

3. Christel Baier, Marjan Sirjani, Farhad Arbab, Jan J. M. M. Rutten. Modeling component connectors in Reo by constraint automata. Sci. Comput. Program., Vol. 61, Num. 2, pages 75-113, 2006.
   Abstract: In this paper we introduce constraint automata and propose them as an operational model for Reo, an exogenous coordination language for compositional construction of component connectors based on a calculus of channels. By providing composition operators for constraint automata and defining notions of equivalence and refinement relations for them, this paper covers the foundations for building tools to address concerns such as the automated construction of the automaton for a given component connector, equivalence checking or containment checking of the behavior of two given connectors, and verification of coordination mechanisms.

4. 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.

5. 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.

6. 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. 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.

3. Patricia Bouyer, Pierre-Alain Reynier, Serge Haddad. Extended Timed Automata and Time Petri Nets. ACSD, pages 91-100, 2006.
   Abstract: Timed Automata (TA) and Time Petri Nets (TPN) are two well-established formal models for real-time systems. Recently, a linear transformation of TA to TPNs preserving reachability properties and timed languages has been proposed, which does however not extend to larger classes of TA which would allow diagonal constraints or more general resets of clocks. Though these features do not add expressiveness, they yield exponentially more concise models. In this work, we propose two translations: one from extended TA to TPNs whose size is either linear or quadratic in the size of the original TA, depending on the features which are allowed; another one from a parallel composition of TA to TPNs, which is also linear. As a consequence, we get that TPNs are exponentially more concise than TA.

4. Gero Decker, Johannes Maria Zaha, Marlon Dumas. Execution Semantics for Service Choreographies. WS-FM, pages 163-177, 2006.
   Abstract: A service choreography is a model of interactions in which a set of services engage to achieve a goal, seen from the perspective of an ideal observer that records all messages exchanged between these services. Choreographies have been put forward as a starting point for building service-oriented systems since they provide a global picture of the system's behavior. In previous work we presented a language for service choreography modeling targeting the early phases of the development lifecycle. This paper provides an execution semantics for this language in terms of a mapping to PI-calculus. This formal semantics provides a basis for analyzing choreographies. The paper reports on experiences using the semantics to detect unreachable interactions.

5. 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.

6. 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.

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. Rocco De Nicola, Gianluigi Ferrari, Ugo Montanari, Rosario Pugliese, Emilio Tuosto. A Basic Calculus for Modelling Service Level Agreements. International Conference on Coordination Models and Languages, LNCS, Vol. 3454, pages 33-48, Springer Verlag, April 2005.
   Abstract: The definition of suitable abstractions and models for identifying, understanding and managing Quality of Service (QoS) constraints is a challenging issue of the Service Oriented Computing paradigm. In this paper we introduce a process calculus where QoS attributes are first class objects. We identify a minimal set of primitives that allow capturing in an abstract way the ability to control and coordinate services in presence of QoS constraints.

10. 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.

11. Rocco De Nicola, Daniele Gorla, Rosario Pugliese. Basic Observables for a Calculus for Global Computing. ICALP, pages 1226-1238, 2005.
    Abstract: We introduce a foundational language for modelling applications over global computers whose interconnection structure can be explicitly manipulated. Together with process distribution, mobility, remote operations and asynchronous communication through distributed data spaces, the language provides constructs for explicitly modelling inter-node connections and for dynamically establishing and removing them. For the proposed language, we define natural notions of extensional observations and study their closure under operational reductions and/or language contexts to obtain barbed congruence and may testing equivalence. For such equivalences, we provide alternative characterizations in terms of a labelled bisimulation and a trace equivalence that can be used for actual proofs.

12. Dan Hirsch, Emilio Tuosto. SHReQ: Coordinating Application Level QoS. SEFM, pages 425-434, 2005.
    Abstract: We present SHReQ, a formal framework for specifying systems that handle abstract high-level QoS requirements which are becoming more and more important for service oriented computing. SHReQ combines Synchronised Hyperedge Replacement (SHR) with constraint-semirings. SHR is a (hyper)graph rewriting mechanism for modelling evolution of systems. The novelty of the approach relies on the synchronisation mechanism which is based on constraint-semirings, algebraic structures that provide both the mathematics for multi-criteria QoS and the synchronisation policies underlying the SHR mechanism.

13. Khaled Mahbub, George Spanoudakis. Run-time Monitoring of Requirements for Systems Composed of Web-Services: Initial Implementation and Evaluation Experience. ICWS, pages 257-265, 2005.
    Abstract: This paper describes a framework supporting the runtime monitoring of requirements for systems implemented as compositions of Web-services specified in BPEL. The requirements that can be monitored are specified in event calculus. The paper presents an overview of the framework and describes the architecture and implementation of a tool that we have developed to operationalise it. It also presents the results of a preliminary experimental evaluation of the framework.

14. 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.

15. 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.

16. Roozbeh Farahbod, Uwe Glässer, Mona Vajihollahi. Specification and Validation of the Business Process Execution Language for Web Services. Abstract State Machines, pages 78-94, 2004.
    Abstract: We formally define an abstract executable semantics for the Business Process Execution Language for Web Services in terms of a distributed ASM. The goal of this work is to support the design and standardization of the language. There is a need for formalism. It will allow us to not only reason about the current specification and related issues, but also uncover issues that would otherwise go unnoticed. Empirical deduction is not sufficient. - Issue 42, OASIS WSBPEL TC. The language definition assumes an infrastructure for running Web services on some asynchronous communication architecture. A business process is built on top of a collection of Web services performing continuous interactions with the outside world by sending and receiving messages over a communication network. The underlying execution model is characterized by its concurrent and reactive behavior making it particularly difficult to predict dynamic system properties with a sufficient degree of detail and precision under all circumstances.

17. Gwen Salaün, Lucas Bordeaux, Marco Schaerf. Describing and Reasoning on Web Services using Process Algebra. ICWS, 2004.
    Abstract: We argue that essential facets of web services, and especially those useful to understand their interaction, can be described using process-algebraic notations. Web service description and execution languages such as BPEL are essentially process description languages; they are based on primitives for behaviour description and message exchange which can also be found in more abstract process algebras. One legitimate question is therefore whether the formal approach and the sophisticated tools introduced for process algebra can be used to improve the effectiveness and the reliability of web service development. Our investigations suggest a positive answer, and we claim that process algebras provide a very complete and satisfactory assistance to the whole process of web service development. We show on a case study that readily available tools based on process algebra are effective at verifying that web services conform their requirements and respect properties. We advocate their use both at the design stage and for reverse engineering issues. More prospectively, we discuss how they can be helpful to tackle choreography issues.

18. Andreas Wombacher, Peter Fankhauser, Erich J. Neuhold. Transforming BPEL into Annotated Deterministic Finite State Automata for Service Discovery. ICWS, pages 316-323, 2004.
    Abstract: Web services advocate loosely coupled systems, although current loosely coupled applications are limited to stateless services. The reason for this limitation is the lack of a method supporting matchmaking of state dependent services exemplarily specified in BPEL. In particular, the sender's requirement that the receiver must support all possible messages sent at a certain state are not captured by models currently used for service discovery. Annotated deterministic finite state automata provide this expressiveness. In this paper the transformation of a local process specification given in BPEL to annotated deterministic finite state automata is presented.

19. Wil M. P. van der Aalst, Arthur H. M. ter Hofstede, Mathias Weske. Business Process Management: A Survey . International Conference on Business Process Management (BPM), Lecture Notes in Computer Science, Vol. 2678, Springer Verlag, 2003.
    Abstract: Business Process Management (BPM) includes methods, techniques, and tools to support the design, enactment, management, and analysis of operational business processes. It can be considered as an extension of classical Workflow Management (WFM) systems and approaches. Although the practical relevance of BPM is undisputed, a clear definition of BPM and related acronyms such as BAM, BPA, and STP are missing. Moreover, a clear scientific foundation is missing. In this paper, we try to demystify the acronyms in this domain, describe the state-of-the-art technology, and argue that BPM could benefit from formal methods/languages (cf. Petri nets, process algebras, etc.).

20. Massimo Mecella, Francesco Parisi Presicce an Barbara Pernici. Modeling E -service Orchestration through Petri Nets . Technologies for E-Services, Lecture Notes in Computer Science, Vol. 2444, pages 109-134, Springer Verlag, July 2002.
    Abstract: B2B interaction requires new forms of coordination between participating organizations. Indeed, the main requirement is that the autonomy of each participating partner is preserved during the interaction, guaranteeing at the same time that the overall goals of the common process are reached. Mechanisms for regulating distributed workflow evolution when the workflow is composed of the invocation of E-services of different organizations are needed. The E-service orchestration model proposed in this paper provides a mechanism for supporting control of process evolution in terms both of control and data flows, and for distributing and assigning process responsibilities.

21. 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.

22. 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.

23. Laurent Fribourg, Marcos Veloso Peixoto. Concurrent Constraint Automata. International Logic Programming Symposium, 1993.
    Abstract: We address the problem of the specification and the proof of properties of concurrent systems which manipulate an unbounded number of data. We propose an approach based on an extended notion of automata, called "Concurrent Constraint Automata (CCA)". A CCA is an automaton with constraints and synchronous communication. By automata with constraints, we mean a state machine whose actions and states contain parameters that take their value in the set of natural numbers. (...)

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 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.