Modeling and Enforcing Invariants of Dynamic Software Architectures


Meidya is based on three principal steps allowing the control of the software architecture evolution of component-based applications. This approach supports the modeling of the dynamic architecture, formal verification and enforcement of the architectural invariants.

In the first step, the designer specifies the dynamic software architecture using a UML profil that we propsoe. First, he/she defines the architectural style (i.e. describes the set of component types, the connection types between them, and architectural invariants) as well as the reconfiguration operations associated with their pre- and post-conditions. Second, the designer maps automatically UML models towards XML language. This function ensures that each generated XML description is well-formed and valid according to the appropriate XML schema defining the proposed meta-model. If the XML description does not satisfy the XML schema, the designer should correct his model.

In the second step, the designer automatically translate the graphic UML models (i.e. defined in the first step) to Z specifications. In addition, the designer should intervene in the theorem prover Z/EVES to verify the consistency of the architectural style on the one hand, the preservation of the architectural invariants during the architectural evolution on the other hand. In the two previous steps, the designer uses our open source FUJABA plug-in to model and validate the dynamic software architecture and to translate the UML models into Z specifications.

In the third step, the programmer automatically translates the formal Z specification of a dynamic software architecture into code. Using our aspect generator tool, the developer produces AspectJ aspects from the Z specification (i.e. defined in the second step). The generated aspects will be integrated in a modular way in the functional application code in order to enforce the architectural invariants at run-time. We stress that the functional application code should be implemented without any software invariant related code. In addition, the names of the classes, their methods, and attributes in the business code should be the same as those used in the graphical model performed at the first step.

Tool Support

The proposed approach for modeling, validating and translating into Z specifications was realized as three FUJABA plug-ins.

Fujaba Tools
The ArchitecturalProfil plug-in ensures the integration of our proposed profile by providing two interfaces. Each interface is equipped with a toolkit to model the architectural style and the reconfiguration operations. This figure presents a screenshot of the FUJABA Tool Suite displaying the emergency operations architectural style.
The plug-in automatically maps the drawn models towards XML language. After that we validate the generated models (XML description) according to the associated meta-model (XML schema): ArchitecturalStyle XML Schema Download the ArchitecturalStyle.XSD and OperationReconfiguration XML Schema Download the OperationReconfiguration.XSD. The XML schema are saved in the FUJABA directory.
The UMLToZ plug-in transforms the generated XML descriptions into Z specifications (as LATEX files). This transformation is carried out in an automatic manner.

Case Studies


    We applied Meidya on three case studies.  As an example, we present: 
    - Modelling phase: The Screenshot of the models 
    - Validation phase: The generated XML file 
    - Verification phase: The generated Z file 
    - Enforcement phase: The generated AspectJ code

  • Emergency Operation System (EOS) [link]

  • Patient monitoring System (PMS) [link]

  • Collaborative Authoring System (CAS) [link]


  • ArchitecturalProfil

    • Description : A plug-in based on a UML profile. It offers two interfaces that, using a toolkit, to model the architectural style and the reconfiguration operations.
    • Setup : The ArchitecturalProfil plug-in should be added under the plugins directory of the FUJABA tool.

      Download the ArchitecturalProfil plug-in

  • UMLToZ

    • Description : A plug-in providing tools for the automatic transformation of a modeling-based UML profile to the Z notation.
    • Setup : The UMLToZ plug-in should be added under the plugins directory of the FUJABA tool.

      Download the UMLToZ plug-in

  • Aspect Generator

    • Description : The aspect generator allows to translate the Z specifications (generated by our Fujaba Plug-in) into aspects in AspectJ language. There are two generation options: automatic and semi-automatic.
    • Setup : The zip file ( is a Java eclipse project. The main class is CompileZ.Interface

      Download the Z-To-Aspect


Research Groups

  • ReDCAD Research Unit (Tunisia)

    • National School of Engineers of Sfax
      Route de la Soukra km 3.5 B.P., 1173, 3038 Sfax - Tunisia

  • LAAS - CNRS (France)

    • UniversitÚ Paul Sabatier, Toulouse
      7 avenue du Colonel Roche, 31077 Toulouse Cedex 4 - France

  • Software Technology Group (Germany)

    • University of Technology Darmstadt
      Hochschulstr. 10, 64289 Darmstadt - Germany

Related papers

A paper describing the whole approach has been accepted

for publication in the Springer SoSyM journal

  • Mohamed Nadhmi Miladi, Mohamed Hadj Kacem, Achraf Bouchriss, Mohamed Jmaiel, and khalil Drira. A UML rule-based approach for describing and checking dynamic software architectures. In AICCSA'08: Proceedings of the 6th ACS/IEEE International Conference on Computer Systems and Applications, Doha, Qatar, 2008. IEEE Computer Society
  • Mohamed Nadhmi Miladi, Mohamed Jmaiel, and Mohamed Hadj Kacem. A UML profile and a fujaba plugin for modelling dynamic software architectures. In MoDSE'07: Proceedings of the Workshop on Model-Driven Software Evolution, pages 20-23, Amsterdam, Netherlands, 2007. IEEE Computer Society
  • Mohamed Hadj Kacem, Mohamed Jmaiel, Ahmed Hadj Kacem, and khalil Drira. An UML-based approach for validation of software architecture descriptions. In TEAA'06: Proceedings of the 2nd International Conference on Trends in Enterprise Application Architecture, volume 4473 of Lecture Notes in Computer Science, pages 158-171, Berlin, Germany, 2007. Springer
  • Slim Kallel, Anis Charfi, Mira Mezini, and Mohamed Jmaiel. Combining Formal Methods and Aspects for Specifying and Enforcing Architectural Invariants, Proceedings of the International Conference on Coordination Models and Languages, Lecture Notes in Computer Science 4467, Springer, pages 211–230, Paphos, Cyprus, June 2007.
  • Slim Kallel, Anis Charfi and Mohamed Jmaiel. Using Aspects for Enforcing Formal Architectural Invariants, In Proceedings. of the 4th International Workshop on Formal Aspect of Component Software, Electronic Notes in Theoretical Computer Science, volume 215, Elsevier, pages 1–15, Sophia-Antipolis, France, September 2007.


We would like to thank Mohamed Nadhmi Miladi and Achraf Boukhriss for several helpful in order to implement the ArchitecturalProfile and the UMLToZ plug-ins.