P/S-CoM+: A Formal Approach to Design Correct Publish/Subscribe Architectural Styles

In this paper we propose P/S-CoM+, a formal approach that helps architects to model correct publish/subscribe architectural styles (PSAS). We extend P/S-CoM formal approach, that focuses on the correct by design of PSAS structure, by behavioral aspect. We specify communication schemas including the state of component types and ensuring no loss of events. We formally model behavioral properties namely delivery semantics, ordering and persistence of notifications. We set up a formal method for composing communication schemas and building correct PSAS. We develop an ECLIPSE plugin P/S-CoM´SD that assists architects in graphically conceiving the desired PSAS. We describe the dynamic behavior of component types by specifying interaction rules. All the specifications are coded in Z notation and proved under Z-Eves theorem prover.