A contractual approach for the verification of UML2.0 software architectures

The functional and qualitative properties are conventionally considered after software is completed. Currently, researchers consider treating those properties as soon as the architectural design phase. In this paper, the modelling and verification of the syntactic, behavioural and qualitative properties in UML2.0 software architectures are studied. To achieve this, a UML profile extending the UML2.0 component model by a set of qualitative concepts is proposed. The new profile, called CUMLQoS, is able to model the UML2.0 software architectures equipped with qualitative properties. Our verification approach suggests using the Acme/Armani ADL as a checking machine of syntactic and qualitative properties of UML2.0 software architectures deriving from our CUMLQoS profile. The choice of this ADL is justified by its ability of formal verification of different types of properties related to software architectures. As a second step of our verification approach, UML2.0, Port State Machine (PoSM), Wright and CSP are combined to check the behavioural consistency of UML2.0 software architecture. To achieve this, a set of systematic rules is proposed allowing the translation of UML2.0 source model to the Wright target model. Using Wr2fdr tool, the Wright specification can automatically be translated to a CSP specification acceptable by the FDR2 model-checker.