Title :
FSM4WSR: A Formal Model for Verifiable Web Service Runtime
Author :
Li, Zhuqing ; Ma, Dianfu ; Zhao, Yongwang ; Li, Jing ; Yang, Qing
Author_Institution :
Inst. of Adv. Comput. Technol., Beihang Univ., Beijing, China
Abstract :
Web service runtime is an important infrastructure middleware for service-based applications. It processes exchanged messages according to web service protocols. Correct implementation of web service protocols is critical for ensuring the reliability of web service runtime. In this paper, we first introduce a Service-Oriented Description Language (SODL) to precisely and concisely describe message processing logics for web service protocol implementations. Then, we propose a formal model for verifiable web service runtime, named FSM4WSR, based on Estelle (an ISO formal description standard). FSM4WSR uses module and channel to capture the essential components of the runtime architecture. Furthermore, the internal behaviors in each module are formally described by using a combination of the extended finite-state machine and SODL. Based on FSM4WSR, we automatically generate the web service protocol implementations and construct a verifiable web service runtime system, named XServices SODL Runtime.
Keywords :
Web services; finite state machines; formal verification; middleware; service-oriented architecture; specification languages; Estelle; FSM4WSR; Web service protocol; XServices SODLRuntime; finite-state machine; formal model; infrastructure middleware; message exchange; message processing logics; runtime architecture; service-based applications; service-oriented description language; verifiable Web service runtime system; Protocols; Quality of service; Runtime; Semantics; Simple object access protocol; XML; Estelle; SOC; Verification; formal model; protocol implementation; web service runtime;
Conference_Titel :
Services Computing Conference (APSCC), 2011 IEEE Asia-Pacific
Conference_Location :
Jeju Island
Print_ISBN :
978-1-4673-0206-7
DOI :
10.1109/APSCC.2011.16
