B Maude: A formal executable environment for Abstract Machine Notation Descriptions
Software Engineering
2021-08-19 v1 Logic in Computer Science
Abstract
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.
Cite
@article{arxiv.2108.07878,
title = {B Maude: A formal executable environment for Abstract Machine Notation Descriptions},
author = {Christiano Braga and Narciso Martí-Oliet},
journal= {arXiv preprint arXiv:2108.07878},
year = {2021}
}