Using ASMs and Spec# to Formal Modeling and Analysis Publish/Subscribe Architectures

The Publish/Subscribe architecture has been proposed as a suitable architecture to develop highly dynamic systems. Although the structure of this architecture is easy to understand, unfortunately modeling and validating the whole system is complicated. In this paper, we present a formal approach based on Abstract State Machines (ASM) to model systems using this architecture. Then, to validate the designed models we use model-based testing. To do so, we propose a transformation from ASMs to Spec# language. The key feature of the proposed approach are new parametric dispatcher and the use of model-based testing for validation.