FSM4WSR: A Formal Model for Verifiable Web Service Runtime

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.