Safe and constructive design with UML components

Abstract

Model-based engineering emerged as an approach to tackle the complexity of current systems development. In particular, compositional strategies assume that systems can be built from reusable and loosely coupled units. However, it is still a challenge to ensure that de-sired properties hold for component integration. BRIC provides an approach for developing component-based systems which guarantee deadlock freedom. Then, we present a component based model for UML, including a metamodel, well-formedness conditions and formal seman-tics via translation into BRIC; the presentation of the semantics is given by a set of rules that cover all the metamodel elements and map them to their respective BRIC denotations. We use BRIC as an underlying (and totally hidden) component development framework so that our approach benefits from all the formal infrastructure developed for BRIC using CSP (Communi-cating Sequential Processes). Component composition, specified via UML structural diagrams, ensures adherence to classical concurrent properties: our focus is on the preservation of dead-lock freedom. Automated support is developed as a plug-in to the Astah modelling tool. The verification is carried out using FDR (a model checker for CSP), but, this is transparent to the user. A distinguishing feature of our approach is its support for traceability. For instance, when FDR uncovers a deadlock, a sequence diagram is constructed from the deadlock trace and presented to the user at the modelling level. We illustrate our overall approach with a running example and two additional case studies. We also emphasise the contributions of the proposed component model and modelling strategy via a comparison with other approaches in the literature.