Strong Preservation by Model Deformation

Reliable and secure system design requires an increasing number of methods, algorithms, and tools for automatic program manipulation. Any program change corresponds to a transformation that affects the semantics at some given level of abstraction. We call these techniques model deformations. In this paper we propose a mathematical foundation for completeness-driven deformations of transition systems w.r.t. a given abstraction, and we introduce CEGMOD, an algorithm for the systematic deformation of Kripke structures for inducing strong preservation in abstract model checking. We prove that our model deformations are deeply related with the notions of must and may transitions in modal transition systems, providing a theoretical characterization of strong preservation in these systems.