McFSM: Near Turing-Complete Finite-State Based Programming
- Finite state machines (FSMs) are an appealing mechanism for simple practical computations: They lend themselves to very effcient and deterministic implementation, are easy to understand, and allow for formally proving many properties of interest. Unfortunately, their computational power is deemed insuffcient for many tasks, and their usefulness has been further hampered by the state space explosion problem and other issues when naïvely trying to scale them to sizes large enough for many real–life applications. This paper expounds on theory and implementation of multiple coupled fnite state machines (McFSMs), a novel mechanism that combines benefits of FSMs with near Turing-complete, practical computing power, and that was designed from the ground up to support static analysis and reasoning. We develop an elaborate category–theoretical foundation based on non–deterministic Mealy machines, which gives a suitable algebraic description for novel ways of blending di#erent computing models. Our experience is based on a domain specific language and an integrated development environment that can compile McFSM models to multiple target languages, applying it to use-cases based on industrial scenarios. We discuss properties and advantages of McFSMs, explain how the mechanism can interact with real–world systems and existing code without sacrificing provability, determinism or performance. We discuss how McFSMs can be used to replace and improve on commonly employed programming patterns, and show how their effcient handling of large state spaces enables them to be used as core building blocks for distributed, safety critical, and real–time systems of industrial complexity, which contributes to the longdesired goal of providing executable specifications.
Author: | Florian Murr, Wolfgang MauererORCiDGND |
---|---|
URL / DOI: | https://www.lfdr.de/Publications/2021/MuMa21.pdf |
Document Type: | Preprint |
Language: | English |
Year of first Publication: | 2021 |
Release Date: | 2023/02/07 |
Tag: | automata; coupled machines Finite state machines; Mealy machines; category theory; executable specifcation; formal models; generative approaches; static analysis |
Pagenumber: | 11 |
Institutes: | Fakultät Informatik und Mathematik |
Fakultät Informatik und Mathematik / Labor für Digitalisierung (LFD) | |
research focus: | Digitalisierung |
Licence (German): | Keine Lizenz - Es gilt das deutsche Urheberrecht: § 53 UrhG |