Security System
Extending the single door to a whole collection
Steve Reeves
This document gives the requirements and a corresponding model in Z for a
security system for a door in a building.
It is probably somewhat simpler than your model since I’ve ignored one or
two features.
1 Requirements
The door has its security controlled by a swipe-card system. The system consists
of a database that records for each user of the system what their personal
identification number (PIN) is.
The door has two mechanisms, one on the outside (for entering the building)
and one on the inside (for leaving the building).
To use the door as an exit, a person simply needs to push the big red button
marked “Push To Exit”. The system unlocks the door, allowing the person to
leave. The door remains unlocked for a certain amount of time, as given by a
system constant. After this time the door is locked.
To enter through the door, the person swipes their card and presses keys
that correspond to their four-digit PIN. The system checks that the person has
given the correct PIN and that they are allowed through the door. If these two
conditions are met, the system unlocks the door. The door remains unlocked
for a certain amount of time, as given by a system constant. After this time
the door is locked. The system also records the fact that the person concerned
used the entry mechanism.
The door’s status can be determined at any time by the system, and its
status will be exactly one of closed and locked, closed and unlocked or open.
The security system is actually part of a larger building management system
(controlling lighting, heating, safety as well as security), so if the fire alarm is
activated within the building, the door’s status must be closed and unlocked or
open.
1.1 A model
We must make available operations that initialise the system, allow entry, allow
exit, unlock a door in an emergency, allow adding a user, deleting a user,
amending a user and logging a user’s entry.
The state schema Status that describes the state of the door at any moment.
We first need to represent the three possible states of the door:
1
DoorStatus ::= closed and locked | closed and unlocked | open
(We will find that open is not needed—from the system’s point-of-view a
door is either unlocked or not. A more fancy system might record the open or
closed state of a door, but for entry and exit purposes it does not need this.)
Then we have the state of a door. This records its current status. It also records
the last times at which the door unlocked and locked. We also need to record
who can have access to this door, for which we use a database (modelled as a
partial function) from people (in the type Person) to PINs. We use log to make
a note of the fact that a person used the door at a certain time. We assume
there is a clock whose time we can read using the observation currentTime.
You’ll note that I have defined a type Time and given it a very small range.
This is to make the searching for solutions bearable—I have been running this
model with timeout for enabling operations set to 30000ms. This isn’t too long
to wait and within the six units of time that we can tick through a realistic set
of operations can be done. Note that the thing which causes a problem here is
the updating of the log. Once you have seen how the system works as it is here,
change the log update in AllowedIn so that the log in fact does not change. (In
the LATEX version of this file I have commented out the fact that log does not
change, so you can comment out the change to log and uncomment the equation
that says log does not change. Once you have done that you can change the
upper bound to Time to be a realistically large number.)
Person ::= p1 | p2
PIN ::= pin1 | pin2
Time == 0 . . 6
Status
status : DoorStatus
locked, unlocked : Time
register : Person 7→ PIN
log : Time 7→ Person
currentTime : Time
The status of the door is initialised by assuming it is closed and locked and
setting the time observations to the current time. The register is also empty at
first, as is the log.
Init
Status
status = closed and locked
locked = unlocked = currentTime = 0
register = ∅
log = ∅
We need to be able to add people to and delete them from the register.
2
AddPerson
∆Status
p? : Person
pin? : PIN
p? ∈/ dom register
register 0 = register ∪ {p? 7→ pin?}
log0 = log
currentTime0 = currentTime
status0 = status
locked0 = locked
unlocked0 = unlocked
DeletePerson
∆Status
p? : Person
p? ∈ dom register
register 0 = {p?} −C register
log0 = log
currentTime0 = currentTime
status0 = status
locked0 = locked
unlocked0 = unlocked
Amending a person’s record is also needed but we omit it here since it is a
straightforward operation to add.
We have two operations which test the person’s PIN to see if it is valid, with
reports.
Report ::= Enter | Invalid PIN | Not Registered
AllowedIn
∆Status
p? : Person
pin? : PIN
pass! : Report
p? ∈ dom register
register p? = pin?
log0 = log ∪ {currentTime 7→ p?}
pass! = Enter
locked = locked0
register = register 0
currentTime = currentTime0
3
NotAllowedIn
ΞStatus
p? : Person
pin? : PIN
pass! : Report
p? ∈ dom register
register p? 6= pin?
pass! = Invalid PIN
We also need to handle the case (and not let them in) when the person is
simply not in the register:
NotRegistered
ΞStatus
p? : Person
pass! : Report
p? ∈/ dom register
pass! = Not Registered
There are then operations representing the use of a door’s controllers (one
on the inside and one on the outside). If the inside button is pressed the door’s
status must become closed and unlocked. The door should also have a lock
operation. These operations change the times recorded appropriately too. To
model the fact that the door remains unlocked for only a certain amount of time
we represent this chosen time interval by
opening time : Time
opening time = 1
Unlock
∆Status
status = closed and locked
status0 = closed and unlocked
unlocked0 = currentTime
locked = locked0
register = register 0
currentTime0 = currentTime
According to this definition, a person can only swipe and enter once the door
has (re-)locked. That is, if the door is already unlocked, it cannot be unlocked
(again). This seems realistic. It also models the real world in that several people
might enter the building (without swiping their cards) once just one person has
swiped their card (before the door locks), and a person might swipe and unlock
the door, but then not actually go into the building. (This is why we have
human security officers, and do not rely on a database to tell us who is in a
building—it cannot be relied on!)
4
Lock
∆Status
status = closed and unlocked
unlocked < currentTime − opening time
status0 = closed and locked
locked0 = currentTime
unlocked0 = unlocked
register = register 0
log = log0
currentTime0 = currentTime
Exiting the building is then achieved by using the Unlock operation. We assume
that the Lock operation is invoked by the system itself, say every second.
(It will fail every time the system tries to use it until the door has been unlocked
for the required amount of time, after which it will succeed and the door
will lock.) Time progresses for the system, and we model this (for animation
purposes) by the operation Tick.
Tick
∆Status
currentTime0 = currentTime + 1
status0 = status
locked0 = locked
unlocked0 = unlocked
register 0 = register
log0 = log
Exit = [ b Unlock | log0 = log]
The operation for entering the building is now one of testing the person’s
PIN and unlocking the door, or not, as appropriate:
Entry = ( b AllowedIn ∧ Unlock) ∨ NotAllowedIn ∨ NotRegistered
Again we assume that the system keeps trying Lock until it succeeds.
If the fire alarm goes off, the Exit operation is invoked, and the repeated use
of Lock by the system does not happen.
2 Your task...
...is to take my solution as above and by using promotion, turn it into a system
for several doors. For the purposes of animation using ProB, the set DIN (see
the first handout for this coursework) should have just two members.
You need to develop an indexed set (e.g. a function, perhaps) of instances
of Status to represent a door database. You then need framing or promotion
schemas with which you can define (as “one-liners”) the system-level counterparts
to the single-door operations given above.
So, we need SysExit, SysEntry, SysLock, SysAddPerson and SysDeletePerson.
We will also need operation to add and delete doors from the collection which
forms the system.
The final thing to do is to specify ticking at the system level. This needs to
be done using Tick exactly as given. So, we need a single operation SysTick
which when invoked makes the time on every door tick forward by one tick.
This is quite tricky.
You might break the problem into two parts: first define an operation
SysTickAux by simple promotion, and this operation should make the given
door’s time tick; the second should define an operation SysTick that uses
SysTickAux for each possible door and makes its time tick forward, so it is
an operation composed from several uses of SysTickAux each specialised to one
of the doors. Or you might, still using Tick, define SysTick more directly.
In order that the search space in not too large, use the version that has log
updates commented out, as explained where I mention the set Time near the
beginning of the previous section.