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

Authors: Taoufik Sakka Rouis; Mohamed Tahar Bhiri; Mourad Kmimech; Faouzi Moussa

Addresses: Cristal Laboratory, ENSI, University of Manouba, Manouba, Tunisia ' MIRACL Laboratory, ISIMS, University of Sfax, Sfax, Tunisia ' UR-OASIS Laboratory, ENIT, University of Tunis El Manar, Tunis, Tunisia ' Cristal Laboratory, ENSI, University of Manouba, Manouba, Tunisia

Abstract: 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.

Keywords: software architecture; verification; contract; UML2.0; PoSM; model-checker; FDR2.

DOI: 10.1504/IJCAT.2018.090030

International Journal of Computer Applications in Technology, 2018 Vol.57 No.1, pp.45 - 58

Received: 03 Oct 2016
Accepted: 19 Jan 2017
Published online: 27 Feb 2018 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article