Introduction to a catalogue of LOTOS correctness preserving transformations

One of the main goals of the LotoSphere Project has been the definition of a software development methodology based on the ISO standard specification language LOTOS. The methodology is meant to support system designers and implementors along the trajectory from an initial abstract specification, down to concrete design and implementation: the latter should be obtained from the former via a disciplined sequence of transformation and refinement steps. By applying a correctness preserving transformation to a given LOTOS specification S1, a designer can obtain a new LOTOS specification S2 that incorporates some design decisions, and at the same time, preserves correctness by guaranteeing that S1 and S2 are linked, at the semantic level, by some formally defined relation. The present document is a catalogue of twelve such correctness preserving transformations. Each chapter of the document is devoted to a different transformation, and follows a common presentation structure, which is explained and motivated in Section 1.1 below. In Section 1.2 we collect all the transformations in two tables, where they are classified according to various criteria, in order to provide a quick overview of the contents of the catalogue and relate the transformations to the various phases of the design methodology.