P/S-CoM: Building correct by design Publish/Subscribe architectural styles with safe reconfiguration

We present P/S-CoM, a formal approach supporting the correct modeling of Publish/Subscribe architectural styles and safe reconfiguration of dynamic architectures for event-based communication. We elaborate a set of patterns and we define the corresponding composition rules to build correct by design Publish/Subscribe styles. The defined patterns and rules respect the principle of information dissemination guaranteeing that the produced information reaches all the subscribed consumers. The patterns are modeled as graphs and the semantics of each pattern and each rule is specified formally in Z notations. We implement these specifications under the Z-Eves theorem prover which we use to prove specification consistency. The Z specification of the designed architectural style is also built by composition by applying the composition rules coded in Z. We consider the interconnection topology between event dispatchers as well as the subscription model using elementary refinements of the style specification. Moreover, we model the reconfiguration of Publish/Subscribe architecture via guarded graph-rewriting rules whose body specifies the structural constraints and whose guards define the pre- and post-conditions ensuring in this way the preservation of stylistic constraints. Similarly, we interpret reconfiguration rules in Z notations, and we implement these rules under Z-Eves for proving that all reconfigurations are style preserving. This results in a unified formal approach which handles both the static and the dynamic aspects of Publish/Subscribe software architectures.