Correctness preserving transformations for the late phases of development

A LOTOS based stepwise refinement methodology has been defined in the Lotosphere project (ref to T1.1). Starting from an initial set of user requirements, the methodology describes a stepwise, disciplined and formal process for deriving implementations. At the core of the methodology are the notions of design, design step, and design trajectory. A design is a LOTOS specification of the system at a certain level of abstraction, complemented with some informal text representing the aspects of the system that are not (yet) formalised. A design can be refined in many ways into another design. A design step implies the selection of one the possible refinements which incorporates some design decision and takes into account a relevant subset of the user requirements. A design trajectory is a sequence of valid design steps that starts from the user requirements and leads to a design or to a realisation where these requirements have been completely satisfied.