Home // International Journal On Advances in Software, volume 11, numbers 3 and 4, 2018 // View article

Versatile but Precise Semantics for Logic-Labelled Finite State Machines

Authors:
Callum McColl
Vladimir Estivill-Castro
Rene Hexel

Keywords: Logic-labelled finite-state machines; Model-Driven Engineering; Real-Time Systems; Verification; Validation

Abstract:
Logic-Labeled Finite State Machines (llfsms) offer model-driven software development (MDSD) while enabling correctness at a high level due to their well-defined semantics that enables testing as well as formal verification. While this combination of the three elements (MDSD, validation, and verification) results in more reliable behaviour of software components, semantics is severely constrained in several areas. Here, we offer a framework that allows flexibility in execution semantics to suit specific domains while maintaining rigour and the capability to generate Kripke structures for formal verification or to execute corresponding monitoring or testing LLFSMs for validation in a test-driven development framework. Through the use of modern constructs that extend the object-oriented paradigm, the framework is able to define a set of semantics that enables versatile approaches to LLFSM definition and execution, as well as enabling functional programming constructs. This vastly increases the versatility and usefulness of LLFSMs, making them more adaptable to different domains, without sacrificing the benefits of executable models and the ability to perform formal verification.

Pages: 227 to 238

Copyright: Copyright (c) to authors, 2018. Used with permission.

Publication date: December 30, 2018

Published in: journal

ISSN: 1942-2628