Imen Loulou , Ahmed Hadj Kacem , Mohamed Jmaiel , Khalil Drira
May 2007
First International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2007) (VECOS)
Verification and Evaluation of Computer and Communication Systems
5-6 May 2007
software architecture, Publish/Subscribe architectural style, dynamic architecture, graph rewriting, formal specification
This paper addresses the dynamic aspect of Publish/Subscribe architectures. We propose an integrated formal approach for the specification and verification of reconfigurations over the topology of Publish/Subscribe architecture styles. We integrate a functional approach and a structural approach based on graph grammars. The purpose is to express dynamism while offering a simple specification which can be easy to read and to understand. We use the specification language Z to describe the constraints made on the architecture style and we describe the dynamic of architecture via guarded graph-rewriting rules whose guards mainly describe the pre- and post-conditions ensuring in this way the preservation of stylistic constraints. To ensure that the system is evolving correctly, we elaborate a verification process which validates each rule, whose semantic is described in Z notation, using the ZEVES theorem prover.
This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/