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 (LL...

Full description

Saved in:
Bibliographic Details
Main Authors: Estivill-Castro, Vladimir, Hexel, Rene
Format: Conference Proceeding
Language:English
Subjects:
Bridges
Compounds
Formal methods
Green products
model-checking
model-driven development
Object oriented modeling
Sensors
Software
state-charts
Unified modeling language
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:1530-0803
2377-5408
DOI:10.1109/ASWEC.2014.20