Formal specification and verification of asynchronously communicating Web services.
详细信息
文摘
As web services are paving the way to the next generation of electronic commerce, how to ensure design correctness for critical web services has been an important issue. This dissertation develops various automatic verification and analysis techniques for the validation of asynchronously communicating web services.;The formal verification of web services faces several special challenges: (1) lack of a formal model to characterize a composition of web services, (2) the undecidability of LTL verification due to the asynchronous communication, and (3) the expressive XPath based XML data manipulation, which is not supported directly by model checkers.;We establish a simple automata-theoretic model to study the global behaviors of a web service composition. Each individual web service (a peer) is specified using a finite state automaton, and is equipped with an unbounded FIFO queue to store incoming messages. The notion of conversations is developed to characterize global behaviors. Each conversation is a sequence of messages that are exchanged among peers, recorded in the order in which they are sent. Linear Temporal Logic (LTL) is naturally extended to specify desired properties on conversations. We show that, due to the asynchronous communication, LTL verification for an arbitrary web service composition is undecidable.;To avoid the complexity caused by asynchrony, a synchronizability analysis is developed for web service compositions. Sufficient conditions are proposed to identify synchronizable web service compositions which generate the same set of conversations under both the synchronous and asynchronous communication semantics. Obviously, the LTL verification for synchronizable web service compositions can be conducted using the synchronous communication semantics. A similar realizability analysis is developed for a top-down specification approach based on conversation protocols.;A Guarded Automata (GA) model is developed to specify web services with XML data. Algorithms are developed to translate Guarded Automata to Promela (the input language of model checker SPIN), including the handling of XPath based data manipulation operations. This allows verification of web services at a great level of detail. Analyses and verification algorithms presented in this dissertation are implemented in the Web Service Analysis Tool (WSAT).