Abstract
Model refinement is a technique indispensable for modeling large and complex systems. Many formal specification methods share
this concept which usually comes together with the definition of refinement correctness, i.e., the mathematical proof of a
logical relation between an abstract model and its refined models. Model refinement is one of the main concepts which the
Abstract State Machine (ASM) formal method is built on. Proofs of correct model refinement are usually performed manually,
which reduces the usability of the ASM model refinement approach. An automatic support to assist the developer in proving
refinement correctness along the chain of refinement steps could be of extreme importance to improve, in practice, the adoption
of ASMs. In this paper, we present how the integration between the ASMs and Satisfiability Modulo Theories (SMT) can be used
to automatically prove correctness of model refinement for the ASM method.
[download the pdf file] [DOI]