Arrangements of Finite-state Machines - Semantics, Simulation, and Model Checking

Vladimir Estivill-Castro, Rene Hexel

2013

Abstract

We propose a contrasting approach to the main stream direction that UML and {\tt STATEMATE} have recently taken when using finite-state machines (FSMs) to model behaviour. That is, rather than the event-driven model that is currently dominant, we suggest to adopt a model of time, a synchronous model. We do support concurrency in our arrangements of FSMs but eliminate the sources of unpredictable threads of execution. Currently, such capacity of the dominant semantics actually results in the need to create many language constructs to regulate threads that, in many cases, even result in imprecise semantics, hampering their use for model-driven development (MDD). By allowing transitions to only be labeled by statements of logic and by executing the machines with an offline schedule, we obtain a simpler language, with less burden for the developer. This creates far reaching potential for accompanying tools, such as integrated development environments, simulators, and even formal verification through model-checking. Model-checking is of particular importance as MDD becomes ubiquitous. Model-checking is possible for our FSMs as we do not need to consider all possible combinations of progress of each of the many threads that the event-driven alternative requires.

Paper Citation

in Harvard Style

Estivill-Castro V. and Hexel R. (2013). Arrangements of Finite-state Machines - Semantics, Simulation, and Model Checking . In Proceedings of the 1st International Conference on Model-Driven Engineering and Software Development - Volume 1: MODELSWARD, ISBN 978-989-8565-42-6, pages 182-189. DOI: 10.5220/0004317101820189

in Bibtex Style

@conference{modelsward13,
author={Vladimir Estivill-Castro and Rene Hexel},
title={Arrangements of Finite-state Machines - Semantics, Simulation, and Model Checking},
booktitle={Proceedings of the 1st International Conference on Model-Driven Engineering and Software Development - Volume 1: MODELSWARD,},
year={2013},
pages={182-189},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0004317101820189},
isbn={978-989-8565-42-6},
}

in EndNote Style

TY - CONF
JO - Proceedings of the 1st International Conference on Model-Driven Engineering and Software Development - Volume 1: MODELSWARD,
TI - Arrangements of Finite-state Machines - Semantics, Simulation, and Model Checking
SN - 978-989-8565-42-6
AU - Estivill-Castro V.
AU - Hexel R.
PY - 2013
SP - 182
EP - 189
DO - 10.5220/0004317101820189