Retrenchment: Extending Refinement for Continuous and Control Systems
Michael R. Poppleton, Richard Banach · Electronic workshops in computing · 2000
Discussion of a radiation dose calculation example demonstrates various expressive limitations of the refinement calculus, particularly for systems with continuous variables. A liberalization of refinement, called retrenchment , is proposed, which will support an analogous formal development calculus. Useful concrete system behaviour can be specified outside the domain of pure refinement, in particular behaviour under controlled precision decay. A syntax and a formal definition are presented for retrenchment in the B notation of J.-R. Abrial. Necessary transitivity and monotonicity properties for a formal development calculus are stated. A generalisation, evolving retrenchment , is proposed, and a simple example demonstrates its utility, by analogy, in control systems applications. Evolution in retrenchment is demonstrated to offer the expressive power to describe useful simulation-like behaviour, with evolving precision, in software for control systems. Finally, the dosimetry problem demonstrates the architectural value of retrenchment for the formal construction of continuous systems.