Graphical simulation of the dynamic evolution of the software architectures specified in Z

This paper provides a graphical simulator that enables to apprehend the dynamic of components-based software architectures based on their formal specification. The simulator initially accepts (as an input) an already validated Z specification using the Z/EVES tool. Then, it generates graphical entities, according to the UML notation, representing software´s components and their connectors. Thereafter, the user may generate architecture instances by adding components and connections between them. Architecture instances can be updated by destroying components/connections or by modifying their interconnections. The user actions are checked through the formal specification of the architectural style.