Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

6-2013

Abstract

UML is a widely used notation, and formalizing its semantics is an important issue. Here, we concentrate on formalizing UML state machines, used to express the dynamic behaviour of software systems. We propose a formal operational semantics covering all features of the latest version (2.4.1) of UML state machines specification. We use labelled transition systems as the semantic model, so as to use automatic verification techniques like model checking. Furthermore, our proposed semantics includes synchronous and asynchronous communications between state machines. We implement our approach in USM2C, a model checker supporting editing, simulation and automatic verification of UML state machines. Experiments show the effectiveness of our approach.

Keywords

State Machine, Model Check, Formal Semantic, Linear Temporal Logic, Event Pool

Discipline

Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 10th International Conference, IFM 2013 Turku, Finland, June 10-14

First Page

331

Last Page

346

ISBN

9783642386121

Identifier

10.1007/978-3-642-38613-8_23

Publisher

Springer Link

City or Country

Turku, Finland

Additional URL

https://doi.org/10.1007/978-3-642-38613-8_23

Share

COinS