Formalisation of SysML design models and an analysis strategy using refinement

Abstract

The increasing complexity of systems has led to increasing difficulty in design. Thestandard approach to development, based on trial and error, with testing used at later stages toidentify errors, is costly and leads to unpredictable delivery times. In addition, for critical systems,for which safety is a major concern, early verification and validation (V&V) is recognised asa valuable approach to promote dependability. In this context, we identify three important anddesirable features of a V&V technique: (i) a graphical modelling language; (ii) formal andrigorous reasoning, and (iii) automated support for modelling and reasoning. We address these points with a refinement technique for SysML supported by tools. SysML is a UML-based language for systems design; it has itself become a de facto standard in the area. There is wide availability of tool support from vendors like IBM, Atego, and Sparx Systems. Our work is distinctive in two ways: a semantics for refinement and for a representative collection of elements from the UML4SysML profile (blocks, state machines, activities, and interactions) used in combination. We provide a means to analyse design models specified using SysML. This facilitates the discovery of problems earlier in the system development lifecycle, reducing time and costs of production. In this work we describe our semantics, which is defined using a state-rich process algebra called CML and implemented in a tool for automatic generation of formal models. We also show how the semantics can be used for refinement-based analysis and development. Our case studies are a leadership-election protocol, a critical component of an industrial application, and a dwarf signal, a device used to control rail traffic. Our contributions are: a set of guidelines that provide meaning to the different modelling elements of SysML used during the design of systems; the individual formal semantics for SysML activities, blocks and interactions; an integrated semantics that combines these semantics with another defined for state machines; and a framework for reasoning using refinement about systems specified by collections of SysML diagrams.