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.
The proposed approach for modeling, validating and translating into Z specifications was realized as three FUJABA plug-ins.
|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
and OperationReconfiguration XML Schema Download
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.
We applied Meidya on three case
studies. As an example, we present:
A paper describing the whole approach has been accepted
for publication in the Springer SoSyM journal
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.