MEIDYA

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.

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]

Download

• 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 (AspectsGeneration.zip) is a Java eclipse project. The main class is CompileZ.Interface

  Download the Z-To-Aspect

Contributors

• Dr. Mohamed Hadj Kacem [Email]

• MSc. Slim Kallel [Email]

• Prof. Mohamed Jmaïel [Email]

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.

Acknowledgement