Tevfik Bultan, Tools for Automated Verification of Web Services
Web Services Analysis Tool home page
Web Service Analysis Tool (WSAT) analyzes interactions of web services that communicate with asynchronous messages. We model the interactions in such a system as a conversation, the global sequence of messages that are exchanged among the web services. A conversation protocol is an automaton which specifies a set of conversations.
There are two interesting questions that arise within this framework: realizability and synchronizability. A conversation protocol is realizable if the corresponding conversation set can be generated by a set of asynchronously communicating web services. On the other hand, a set of asynchronously communicating web services are synchronizable if their conversation set does not change when asynchronous communication is replaced with synchronous communication.
WSAT verifies LTL properties of conversation protocols and checks sufficient conditions for realizability and synchronizability. In order to model XML data, WSAT uses a guarded automata model where the guards of the transitions are written as XPath expressions. Currently, WSAT uses the explicit-state model checker SPIN for LTL model checking by translating the guarded automata model to Promela. In the future, we plan to investigate symbolic analysis and verification of web services.
Bio: Tevfik Bultan received his B.S. in electrical and electronics engineering in 1989 from the Middle East Technical University, and his M.S. in computer engineering and information science in 1992 from the Bilkent University, both in Ankara, Turkey. He received his Ph.D. in computer science in 1998 from the University of Maryland, College Park. He joined the Computer Science Department of the University of California, Santa Barbara in September 1998.
Tevfik Bultan received a NATO Science Fellowship from the Scientific and Technical Research Council of Turkey (TUBITAK) in 1993, a Regents' Junior Faculty Fellowship from the University of California, Santa Barbara in 1999, and a Faculty Early Career Development (CAREER) Award from the National Science Foundation in 2000.
Tevfik Bultan's current research interests are: web services, concurrency, model checking, static analysis, and software engineering.