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

TL;DR

B Maude is an executable environment for Abstract Machine Notation that leverages Maude's rewriting capabilities, enabling execution, symbolic analysis, and model checking of AMN specifications.

Contribution

It introduces a formal, executable environment for AMN based on Maude, integrating semantics through the π Framework and enabling advanced analysis techniques.

Findings

Supports execution of AMN specifications

Enables symbolic search and model checking

Provides a formal semantics foundation

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 $\pi$ 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.