Vérification formelle d'architectures logicielles à base d'UML
Malgré son pouvoir expressif, UML ne transporte pas en lui-même une sémantique très précise pour décrire les architectures logicielles. Nous préconisons une ouverture d'UML sur l'ADL formel Wright via notre profil W-UML. En outre, afin d'analyser davantage les descriptions architecturales en Wright, nous proposons une approche de traduction systématique de Wright vers Ada. Ceci permet l'utilisation des outils de vérification formelle des programmes concurrents associés à Ada tels que FLAVERS afin d'analyser et raisonner formellement sur des architectures décrites initialement en W-UML.
In spite of its expressive capacity, UML does not transport in itself a very precise semantics to describe software architectures. We recommend an opening of UML on the formal ADL Wright via our W-UML profile. Moreover, in order to more analyze architectural descriptions as Wright, we propose a systematic approach of translation of Wright towards Ada. This allows the use of the tools for formal verification of the concurrent programs associated Ada such as FLAVERS in order to analyze and reason formally on the architectures described initially in W-UML.
M.TAHAR BHIRI, M.GRAIET, J.GIRAUDIN, A.BEN HAMADOU
langage de description d'architectures, architecture logicielle, UML, vérification formelle, Wright.
architecture description language, software architecture, UML, formal verification, Wright.
Français
|
