Correctness by Construction with Logic-Labeled Finite-State Machines -- Comparison with Event-B

Formal methods have seen emergent success recently with the deployment of Event-B. However, Event-B explicitly postulates that models there are not executable. This seems to contradict the parallel emergence of model-driven development (MDD). We show here that logic-labeled finite-state machines (LLFSMs) are effective in carrying out the "correct from construction" agenda of formal methods such as Event-B and simultaneously achieve the aims of MDD. As a result, we obtain models that are directly interpretable, compliable, and executable enabling traceability, transparency and rapid maintainability, while at the same time enabling simulation, validation and formal verification with model checking. Moreover, the Event-B capacity to develop closed models is also very natural with arrangements of LLFSMs, and therefore further safety analysis such as failure-mode effects analysis (FMEA) can be performed. We demonstrate this with two well-known examples in the literature.