A formal semantics for complete UML state machines with communications

A formal semantics for complete UML state machines with communications

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...

Full description

Saved in:
Bibliographic Details
Main Authors: LIU, Shuang, LIU, Yang, ANDRÉ, Étienne, CHOPPY, Christine, SUN, Jun, WADHWA, Bimlesh, DONG, Jin Song
Format: text
Language:English
Published: Institutional Knowledge at Singapore Management University 2013
Subjects:
State Machine
Model Check
Formal Semantic
Linear Temporal Logic
Event Pool
Software Engineering
Online Access:https://ink.library.smu.edu.sg/sis_research/5003
https://ink.library.smu.edu.sg/context/sis_research/article/6006/viewcontent/a_formal.pdf
Tags: Add Tag
No Tags, Be the first to tag this record!
Institution: Singapore Management University
Language: English
Description
Summary: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.

Similar Items