Deductive Model Refinement

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 M of system dynamics and a set phi of required properties, model refinement is an iterative process that eliminates behaviors of M that do not satisfy the required properties. The result of model refinement is a refined model M' that satisfies by construction the required properties F. The calculations needed to generate refinements of 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.