Dynamic software architectures verification using DynAlloy

Graph Grammars have been often used for modeling dynamic changes in software architectures. In particular, we have previously characterized some classes of dynamicity in terms of particular aspects of graph grammars. Moreover we have identified classes of properties that can be naturally associated to any of such kinds of dynamicities. In this paper we approach the problem of verifying such properties over graph grammars specifications. In particular, we use DYNALLOY for attempting this task and we have concentrated on proving properties associated to a particular programmable dynamic software architecture.