Abstract
The architecture description languages (ADL) have been developed to formally model software architectures. One of the challenges of ADLs is their ability to perform the validation and/or verification of software system properties very early in their life cycle and throughout their development process. The Wright formal ADL is based on CSP and, thus, inherits its equivalence and refinement relations as well as support for the verification of general properties using the FDR2 model checker. In this paper, we proposed to open UML2.0 on the Wright ADL in order to verify the behavioral consistency of UML2.0 software architectures. To achieve this, we suggested to translate this software architecture into a Wright specification. Using Wr2fdr tool, these Wright descriptions were automatically translated to a CSP specification acceptable by the FDR2 model-checker.