An OO and Functional Framework for Versatile Semantics of Logic-Labelled Finite State Machines
Callum McColl, Vladimir Estivill‐Castro, René Hexel · Griffith Research Online · 2017
Logic-Labeled Finite State Machines (LLFSMs) offer model-driven software development (MDSD) while enabling correctness at a high level due to their transparent semantics that enables testing as well as formal verification. This combination of the three elements (MDSD, validation, and verification) results in more reliable behaviour of software components, but semantics is constrained to specific scheduling. We offer a framework that allows to obtain significant variations that suit specific domains while maintaining the capability to generate Kripke structures for formal verification or to execute corresponding monitor or testing LLFSMs for validation in a test-driven development framework. The framework is Object-Oriented so new software patterns for scheduling can be derived to suit a particular embedded, robotic, or cyber-physical system, while at the same time enabling functional programming constructs.