A specification of the cat and mouse problem
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.
KeywordsReal-time specification system engineering analysis formal specification
Unable to display preview. Download preview PDF.
- Hayes, Ian, editor. Specification Case Studies. Pentice-Hall, Englewood Cliffs, NJ, 1987.Google Scholar
- 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
- 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
- Sannella, Donald. A survey of formal software development methods. Technical Report ECS-LFCS-88-56, Edinburgh University, 1988.Google Scholar
- Spivey, J.M. Understanding Z, volume 3 of Cambridge Tracts in Theoretical Computer Science. Cambridge Univerity Press, 1988.Google Scholar
- Spivey, J.M. The Z Notation: A Reference Manual. Prentice-Hall, New York, NY, 1989.Google Scholar