A formal component model for UML based on CSP aiming at compositional verification

Model-based engineering emerged as an approach to tackle the complexity of current system 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 desired properties hold for component integration. We present a component-based model for UML, including a metamodel, well-formedness conditions and formal semantics 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 our previous work on 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. Component composition, specified via UML structural diagrams, ensures adherence to classical concurrent properties: our focus is on the preservation of deadlock freedom. Automated support is developed as a plug-in to the Astah modelling tool. Verification is carried out using FDR (a model checker for CSP); we address scalability using compositional reasoning (inherent to the approach) and behavioural patterns. The formal reasoning 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. The overall approach is illustrated with a running example and two additional case studies.