Formal Engineering Methods, International Conference on (2000)
Sept. 4, 2000 to Sept. 7, 2000
R. Banach , Manchester University
M. Poppleton , Manchester University and Open University
Retrenchment is presented in a simple relational framework as a more flexible development concept than refinement for capturing the early pre-formal stages of development, and briefly justified. Fragmented retrenchment permits the granularity of actions to decrease across a development step, many concrete steps retrenching a single abstract one. This generates the usual proliferation of inter-leavings of events at the concrete level. Event structures, particularly flow event structures, help to control these within the retrenchments of a single abstract step, while the concurrent reading of the fragmented retrenchment proof obligation permits acceptable inter-leavings of retrenchments of different steps. It is observed that retrenchment allows the convenient description of unfair behaviours when fairness is not guaranteed.
R. Banach and M. Poppleton, "Fragmented Retrenchment, Concurrency and Fairness," Formal Engineering Methods, International Conference on(ICFEM), York, England, 2000, pp. 143.