B Maude: A formal executable environment for Abstract Machine Notation Descriptions

08/17/2021
by   Christiano Braga, et al.
0

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.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset