FROM AN ERAE REQUIREMENTS SPECIFICATION TO A PLUSS ALGEBRAIC SPECIFICATION - A CASE-STUDY

Formal specification languages and methods for refining specifications into programs have, up to now, received more attention than methods for obtaining the initial formal specification. This situation is corrected in the ESPRIT project METEOR, which distinguishes the two activities of requirements engineering (RE) - obtaining the right specification - and design engineering (DE) - using that specification properly. Because of their difference of nature, these two activities gain from using different languages: RE languages should be closer to natural language constructs, whereas DE languages should easily describe computer artifacts. In particular, the RE language ERAE is based on temporal logic, whereas the DE language PLUSS uses algebraic specifications, with emphasis on modularity and structuring concepts. This paper investigates the transition between these two formalisms, which takes place when the requirements specification is found satisfactory. As an example, we use the specification of a transit node in a telephonic network.