Specification of the transit node in PSFd

  • S. Mauw
  • F. Wiedijk
Part IV Algebraic Specification
Part of the Lecture Notes in Computer Science book series (LNCS, volume 490)


The specification language PSFd is used to give a formal specification of a transit node, a common case study in ESPRIT project METEOR. The design of the specification derived from the informal text and the ERAE specification is included. A short discussion on the relation to the specification in ERAE is provided.


Atomic Action Incoming Message Informal Text Informal Reasoning Algebraic Specification 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

9. References

  1. [BHK89]
    J.A. Bergstra, J. Heering & P. Klint, Algebraic specification, ACM Press Frontier Series, Addison Wesley, 1989.Google Scholar
  2. [BK86]
    J.A. Bergstra & J.W. Klop, Process algebra: specification and verification in bisimulation semantics,, in: Math. & Comp. Sci. II, (M. Hazewinkel, J.K. Lenstra & L.G.L.T. Meertens, eds.), CWI Monograph 4, pp 61–94, North-Holland, Amsterdam, 1986.Google Scholar
  3. [DHR88]
    E. Dubois, J. Hagelstein & A. Rifaut, Formal requirements engineering with ERAE, Philips Journal of Research 43, nos. 3/4, pp. 393–414, 1988.Google Scholar
  4. [Hag88]
    J. Hagelstein, The Transit Node — ERAE specification, METEOR PRLB Report, 1988.Google Scholar
  5. [HR89]
    J. Hagelstein & A. Rifaut, The semantics of ERAE, Philips Research Laboratory Brussels Manuscript, Belgium, 1989.Google Scholar
  6. [Ide88]
    IDEAS interface user guide, Centre de Recherches de la C.G.E., Marcoussis 1988.Google Scholar
  7. [MHB89]
    A. Mauboussin, J. Hagelstein, M. Bidoit, M-C. Gaudel & H. Perdrix, From an ERAE requirement specification to a PLUSS algebraic specification: A case study, Report METEOR task 10, 1989.Google Scholar
  8. [MV88]
    S. Mauw & G.J. Veltink, A Process Specification Formalism, Report P8814, University of Amsterdam, Amsterdam, 1988. To appear in: Fundamenta Informaticae.Google Scholar
  9. [MV89]
    S. Mauw & G.J. Veltink, An introduction to PSF d, in: Proc. TAPSOFT 89 (J. Diaz & F. Orejas, eds.), LNCS 352, Volume 2, pp 272–285, Springer Verlag, 1989.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1991

Authors and Affiliations

  • S. Mauw
    • 1
  • F. Wiedijk
    • 1
  1. 1.Programming Research GroupUniversity of AmsterdamAmsterdamThe Netherlands

Personalised recommendations