Formal modeling of the Simple Text Oriented Messaging Protocol using Event-B method

This paper presents an incremental formal modeling of the Simple Text Oriented Messaging Protocol (STOMP) using Event-B method. STOMP is a simple text-oriented protocol, similar to HTTP. It provides an interoperable wire format so that STOMP clients can communicate with any STOMP message broker to provide easy and widespread messaging interoperability among many languages and platforms. In this paper we model the protocol step by step by using refinement, a technique of Event-B. The first step will be the modeling of the most abstract specification of the protocol. Then by refinement more details of the protocol specification will be added to the model. By this approach, the model will be a more explicit representation of the target protocol by each refinement. In the developed Event-B models of the STOMP protocol described in this paper, all proofs are generated and discharged by the Rodin tool.