Publications in Automaton-Based Techniques

Articles in Refereed Journals:

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

2. George A. Papadopoulos, Farhad Arbab. Coordination Models and Languages. Advances in Computers, Vol. 46, pages 330-401, 1998.
   Abstract: A new class of models, formalisms and mechanisms has recently evolved for describing concurrent and distributed computations based on the concept of "coordination". The purpose of a coordination model and associated language is to provide a means of integrating a number of possibly heterogeneous components together, by interfacing with each component in such a way that the collective set forms a single application that can execute on and take advantage of parallel and distributed systems. In this chapter we initially define and present in sufficient detail the fundamental concepts of what constitutes a coordination model or language. We then go on to classify these models and languages as either "data-driven" or "control-driven" (also called "process-" or "task-oriented"). Next, the main existing coordination models and languages are described in sufficient detail to let the reader appreciate their features and put them into perspective with respect to each other. The chapter ends with a discussion comparing the various models and some conclusions.

Articles in Refereed Conferences:

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

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

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

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

5. Xiang Fu, Tevfik Bultan, Jianwen Su. Realizability of Conversation Protocols With Message Contents. ICWS, 2004.
   Abstract: A conversation protocol is a top-down specification framework which specifies desired global behaviors of a web service composition. In our earlier work [A formalism for specification and verification of reactive electronic services] we studied the problem of realizability, i.e., given a conversation protocol, can a web service composition be synthesized to generate behaviors as specified by the protocol. Several sufficient realizability conditions were proposed in [A formalism for specification and verification of reactive electronic services] to ensure realizability. Conversation protocols studied in [A formalism for specification and verification of reactive electronic services], however, are essentially abstract control flows without data semantics. This paper extends the work in [A formalism for specification and verification of reactive electronic services] and achieves more accurate analysis by considering data semantics. To overcome the state-space explosion caused by the data content, we propose a symbolic analysis technique for each realizability condition. In addition, we show that the analysis of the autonomy condition can be done using an iterative refinement approach.

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

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

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.