From an ERAE requirements specification to a PLUSS algebraic specification: A case study
- 100 Downloads
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.
KeywordsTemporal Logic Requirement Engineering Control Message Data Message Algebraic Specification
Unable to display preview. Download preview PDF.
- [Bid 89]Bidoit M., "PLUSS a Language for the Development of Modular Algebraic Specifications", Thèse d'Etat, LRI, May 1989.Google Scholar
- [BGM 87]Bidoit M., Gaudel M.-C. and Mauboussin A., "How to Make Algebraic Specifications more Understandable ? An Experiment with the PLUSS Specification Language", Proceedings of the METEOR Workshop on Algebraic Specifications, Passau, June 1987.Google Scholar
- [Dij 88]Dijkstra E.W, "Position Paper on "Fairness"", Software Engineering Notes, Vol 13, no2, April 1988, pp.18–20.Google Scholar
- [DHR 88]E. Dubois, J. Hagelstein and A. Rifaut, "Formal Requirements Engineering with ERAE", Philips Journal of Research, vol. 43, 3/4,1988, pp.393–414. (A revised version is available from the authors.)Google Scholar
- [Gau 85]Gaudel M.-C. "Towards Structured Algebraic Specifications", Esprit Technical Week, Bruxelles, September 1985, Proceedings of Esprit'85 Status Report, North-Holland, pp.493–510.Google Scholar
- [Hag 89]Hagelstein J., "The ERAE Language Definition", Philips Research Laboratory Brussels,June 1989.Google Scholar
- [KP 88]Kaplan S. and Pnueli A., "Specification and Implementation of Concurrently Accessed Data Structures: An Abstract Data Type Approach", Proceedings of the STACS 87 Conference, LNCS 247, Springer Verlag.Google Scholar
- [Kap 89]Kaplan S., "The Transit Node via Process Specifications", Draft, July 1989.Google Scholar
- [RU 71]N.Rescher and A.Urquhart, "Temporal logic", Springer Verlag,1971.Google Scholar
- [SL 88]Schneider F.B. and Lamport L., "Another Position Paper on "Fairness"", Software Engineering Notes, Vol 13, no3, July 1988, pp. 18–19.Google Scholar
- [TW 86]Tarlecki A. and Wirsing M., "Continuous Abstract Daa Types", Fundamenta Informaticae 9, 1986, pp.95–125.Google Scholar