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:
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
id sg-smu-ink.sis_research-6006
record_format dspace
spelling sg-smu-ink.sis_research-60062020-03-12T09:34:53Z A formal semantics for complete UML state machines with communications LIU, Shuang LIU, Yang ANDRÉ, Étienne CHOPPY, Christine SUN, Jun WADHWA, Bimlesh DONG, Jin Song 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. 2013-06-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/5003 info:doi/10.1007/978-3-642-38613-8_23 https://ink.library.smu.edu.sg/context/sis_research/article/6006/viewcontent/a_formal.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University State Machine Model Check Formal Semantic Linear Temporal Logic Event Pool Software Engineering
institution Singapore Management University
building SMU Libraries
continent Asia
country Singapore
Singapore
content_provider SMU Libraries
collection InK@SMU
language English
topic State Machine
Model Check
Formal Semantic
Linear Temporal Logic
Event Pool
Software Engineering
spellingShingle State Machine
Model Check
Formal Semantic
Linear Temporal Logic
Event Pool
Software Engineering
LIU, Shuang
LIU, Yang
ANDRÉ, Étienne
CHOPPY, Christine
SUN, Jun
WADHWA, Bimlesh
DONG, Jin Song
A formal semantics for complete UML state machines with communications
description 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.
format text
author LIU, Shuang
LIU, Yang
ANDRÉ, Étienne
CHOPPY, Christine
SUN, Jun
WADHWA, Bimlesh
DONG, Jin Song
author_facet LIU, Shuang
LIU, Yang
ANDRÉ, Étienne
CHOPPY, Christine
SUN, Jun
WADHWA, Bimlesh
DONG, Jin Song
author_sort LIU, Shuang
title A formal semantics for complete UML state machines with communications
title_short A formal semantics for complete UML state machines with communications
title_full A formal semantics for complete UML state machines with communications
title_fullStr A formal semantics for complete UML state machines with communications
title_full_unstemmed A formal semantics for complete UML state machines with communications
title_sort formal semantics for complete uml state machines with communications
publisher Institutional Knowledge at Singapore Management University
publishDate 2013
url https://ink.library.smu.edu.sg/sis_research/5003
https://ink.library.smu.edu.sg/context/sis_research/article/6006/viewcontent/a_formal.pdf
_version_ 1770575170256240640