B Maude: A formal executable environment for Abstract Machine Notation Descriptions
This work provides a formal executable environment for the B method, addressing a specific need in formal methods and software engineering, but it is incremental as it builds on existing frameworks like Component-based Semantics and Interpreting Automata.
The authors tackled the lack of an executable environment for Abstract Machine Notation (AMN) descriptions by developing B Maude, a prototype implemented in Maude that enables execution via rewriting, symbolic search with narrowing, and Linear Temporal Logic model checking.
We propose B Maude, a prototype executable environment for the Abstract Machine Notation implemented in the Maude language. B Maude is formally defined and results from the implementation of the semantics of AMN as denotations in the $π$ Framework, a realization of Mosses' Component-based Semantics and Plotkin's Interpreting Automata. B Maude endows the B method with execution by rewriting, symbolic search with narrowing and Linear Temporal Logic model checking of AMN descriptions.