Model Refinement: Generating Refinements for Algorithm and System Design

Deductive model refinement (hereafter simply “model refinement”) is a uniform approach to generating correct-by-construction designs for algorithms and systems from formal specifications. Given an overapproximating model \(\mathcal{M}\) of system dynamics and a set \(\varPhi \) of required properties, model refinement is an iterative process that eliminates behaviors of \(\mathcal{M}\) that do not satisfy the required properties. The result of model refinement is a refined model \(\mathcal{M}'\) that satisfies by construction the required properties \(\varPhi \) . The calculations needed to generate refinements of \(\mathcal{M}\) typically involve quantifier elimination and extensive formula/term simplification modulo the underlying domain theories. This paper focuses on the enforcement of basic safety properties in the form of state, action, and path invariants. We have run a prototype implementation of model refinement based on the Z3 SMT solver over a variety of system and algorithm design problems.