Model Based Refinement and the Design of Retrenchments

Abstract. The ingredients of typical methodologies for model based development via refinement are re-examined, and some well-known frameworks are reviewed, drawing out commonalities and differences. It is observed that the ingredients of these formalisms can frequently be ‘mixed and matched ’ much more freely than is often imagined, resulting in semantic variations on the original formulations. It is also noted that similar alterations in the semantics of specific formalisms have taken place de facto due to applications pressures and for other reasons. This analysis suggests prioritising some criteria and proof obligations over others within this family of methods. These insights are used to construct a foundation for the design of notions of retrenchment appropriate for, and complementary to, given notions of refinement. The notions of retrenchment thus derived for the specific refinement formalisms examined earlier, namely Z, B, Event-B, ASM, VDM, RAISE, IO-automata and TLA+, are presented, and within the criteria given, all turn out to be very similar