ConStaBL -- A Fresh Look at Software Engineering with State Machines

TL;DR

This paper introduces an extended operational semantics for statecharts with concurrency and local variables, enabling precise modeling, simulation, and automated fuzz testing of complex systems.

Contribution

It presents a stricter, conflict-free semantics for statecharts with concurrency and local variables, along with a simulation algorithm and a novel fuzz testing approach.

Findings

Semantics prevents transition conflicts during simulation.

The approach allows detailed modeling of concurrent systems.

Fuzz testing identified hard-to-find issues in complex statechart models.

Abstract

Statechart is a visual modelling language for systems. In this paper, we extend our earlier work on modular statecharts with local variables and present an updated operational semantics for statecharts with concurrency. Our variant of the statechart has local variables, which interact significantly with the remainder of the language semantics. Our semantics does not allow transition conflicts in simulations and is stricter than most other available semantics of statecharts in that sense. It allows arbitrary interleaving of concurrently executing action code, which allows more precise modelling of systems and upstream analysis of the same. We present the operational semantics in the form of the simulation algorithm. We also establish the criteria based on our semantics for defining conflicting transitions and valid simulations. Our semantics is executable and can be used to simulate statechart models and verify their correctness. We present a preliminary setup to carry out fuzz testing of Statechart models, an idea that does not seem to have a precedent in literature. We have used our simulator in conjunction with a well-known fuzzer to do fuzz testing of statechart models of non-trivial sizes and have found issues in them that would have been hard to find through inspection.