An Operational Semantics for Activity Diagrams using SMV

TL;DR

This paper presents an operational semantics for activity diagrams by translating them into SMV models, enabling formal analysis of their behavior, including concurrency and data support, with practical implementation and examples.

Contribution

It introduces a translation method from activity diagrams to SMV that incorporates data and supports concurrent execution, extending prior work.

Findings

The translation accurately models activity diagrams in SMV.

Implementation demonstrates practical applicability.

Examples illustrate the translation process and semantics.

Abstract

This document defines an operational semantics for activity diagrams (ADs) using a translation to SMV. The translation is inspired by the work of Eshuis [Esh06] and extends it with support for data. Each execution step of the SMV module obtained from an AD represents an executed action of this AD with interleaved execution of concurrent branches. An implementation of the given translation was used in the context of semantic differencing for ADs [MRR11]. We define the translation and give two examples, showing ADs and their complete representation in SMV.