Model Based Engineering of Specifications by Retrenching Partial Requirements
Richard Banach, Michael R. Poppleton · ePrints Soton (University of Southampton) · 2001
In conventional model oriented formal refinement, the abstract model is supposed to capture all the properties of interest in the system, in an as clutter-free as possible a manner. Subsequently, the refinement process guides development inexorably towards a faithful implementation. However refinement says nothing about how to obtain the abstract model in the first place. In reality developers experiment with prototype models and their refinements until a workable arrangement is discovered. Retrenchment is a formal technique intended to capture some of the informal approach to a refinable abstract model in a formal manner that will integrate with refinement. This is in order that the benefits of a formal approach can migrate further up the development hierarchy. After a presentation of the basic ideas of retrenchment, a simple telephone system feature interaction case study is given to illustrate how retrenchment can relate incompatible partial models to a more definitive consolidated model during the development of the contracted specification.