A specification of the cat and mouse problem

  • William G. Wood
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 600)


The cat and mouse problem described herein was proposed as a sample real-time pedagogical problem at the REX workshop. It is very simple, and includes some real-time aspects. I decided to specify this particular problem to demonstrate one way of dealing with time in the specification language Z. This paper contains a description of the problem, the Z specification, and a justification for choosing Z as the specification language.


Real-time specification system engineering analysis formal specification 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Hayes, Ian, editor. Specification Case Studies. Pentice-Hall, Englewood Cliffs, NJ, 1987.Google Scholar
  2. [2]
    Place, Patrick, Wood, William, Luckham, David C., Mann, Walter, and Sankar, Sriram. Formal development of ada programs using z and anna: A case study. SEI Technical Report CMU/SEI-91-TR-1, Software Engineering Institute, Carnegie Mellon University, Pittsburgh, PA, 1991. ESD-91-TR-1.Google Scholar
  3. [3]
    Place, Patrick, Wood, William, and Tudball, Mike. Survey of formal specification techniques for reactive systems. SEI Technical Report CMU/SEI-90-TR-5, Software Engineering Institute, Carnegie Mellon University, Pittsburgh, PA, 1990. ESD-TR-90-206.Google Scholar
  4. [4]
    Sannella, Donald. A survey of formal software development methods. Technical Report ECS-LFCS-88-56, Edinburgh University, 1988.Google Scholar
  5. [5]
    Spivey, J.M. Understanding Z, volume 3 of Cambridge Tracts in Theoretical Computer Science. Cambridge Univerity Press, 1988.Google Scholar
  6. [6]
    Spivey, J.M. The Z Notation: A Reference Manual. Prentice-Hall, New York, NY, 1989.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • William G. Wood
    • 1
  1. 1.Software Engineering Institute (Sponsored by the U.S. Department of Defense)Carnegie Mellon UniversityPittsburgh

Personalised recommendations