A formal framework for software development using publish/Subscribe architecture

High flexibility of publish/Subscribe architecture that is a common architectural style for component based systems make it to be capable of developing and supporting large software systems. But difficult aspect of Publish/Subscribe systems is their validation. Existing efforts for developing formal foundation for specifying and reasoning about these systems are hard to use by practitioners who are not familiar with formal methods. To face this challenge this paper proposes a formal framework for software development using Publish/Subscribe architecture. Modeling components by Abstract State Machines (ASMs), presentation new characteristics for parametric dispatcher and the use of model-based testing for validation are the key features of this framework.