Automated Conversion of Axiomatic to Operational Models: Theory and Practice

A system may be modelled as an operational model (which has explicit notions of state and transitions between states) or an axiomatic model (which is specified entirely as a set of invariants). Most formal methods (e.g., IC3, invariant synthesis, etc) are designed for operational models and are largely inaccessible to axiomatic models. Furthermore, no prior method exists to automatically convert axiomatic models to operational ones, so operational equivalents to axiomatic models had to be manually created and proven equivalent. In this paper, we advance the state-of-the-art in axiomatic to operational model conversion. We show that general axioms in the $\mu \text{spec}$ axiomatic modelling framework cannot be translated to equivalent finite-state operational models. We also derive restrictions on the space of $\mu \text{spec}$ axioms that enable the feasible generation of equivalent finite-state operational models for them. As for practical results, we develop a methodology for automatically translating $\mu \text{spec}$ axioms to equivalent finite-state automata-based operational models. We demonstrate the efficacy of our method by using the models generated by our procedure to prove the correctness of ordering properties on three register-transfer-level (RTL) designs.