Security system case study

This paper is an early draft of the specification of a security system. We begin by giving a full description in English of the client company and their requirements for card issuing system and a door control system. The formal notation, Z, is then used to specify the door control system, in terms of both it's basic functionality and it's interaction with the people who use it. The specification of the card issuing system is left as an exercise for the reader. Suggestions as to how to proceed with this can be found at the end of the paper.