Formal Methods: Foundations and Applications

Abstract

In this work, we propose a semantics for Activity Diagrams based on the COMPASS Modelling Language (CML): a formal specification language to model systems which is based on the CSP and VDM specification languages. A distinguishing feature of our semantics is that it is defined as part of a larger effort to define the semantics of several diagrams of SysML, a UML profile for systems engineering. We have defined a fairly comprehensive semantics for Activity Diagrams, which comprises action, object and control nodes constructors, control and object flow, interruptible regions among other features. We illustrate our semantics with diagrams of an emergency response system. We also discuss an analysis strategy which involves an integrated view of diagrams like block definition and state machines. © 2013 Springer-Verlag.