Versatile but Precise Semantics for Logic-Labelled Finite State Machines

  • Authors
  • McColl C, Estivill-Castro V, Hexel R
  • UPF authors
  • ESTIVILL CASTRO, VLADIMIR;
  • Type
  • Scholarly articles
  • Journal títle
  • International journal on advances in software
  • Publication year
  • 2018
  • Volume
  • 11
  • Number
  • 3-4
  • Pages
  • 227-238
  • ISSN
  • 1942-2628
  • Publication State
  • Published
  • 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.
  • Complete citation
  • McColl C, Estivill-Castro V, Hexel R. Versatile but Precise Semantics for Logic-Labelled Finite State Machines. International journal on advances in software 2018; 11(3-4): 227-238.