Fragmented Retrenchment, Concurrency and Fairness

Retrenchment is presented in a simple relational framework as a more flexible development concept than refinement for capturing the early preformal stages of development, and briefly justified. Fragmented retrenchment permits the granularity of actions to decrease across a development step, many concrete steps retrenching a sinract one. This generates the usual proliferation of interleavings of events at the concrete level. Event structures, particularly flow event structures, help to control thin the retrenchments of a single abstract step, while the concurrent reading of the fragmented retrenchment proof obligation permits acceptable interleavings of retrenchments of different steps. It is observed that retrenchment allows the convenient description of unfair behaviours when fairness is not guaranteed.

• Type: Conference
• Year: 2000
• Where: ICFEM
• Authors: Richard Banach, Michael Poppleton
• Keywords: Fragmented Retrenchment, Fragmented Retrenchment Proof, ICFEM 2000, Retrenchment, Software Engineering