COMPX554
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, al- low 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 → PIN log : Time → 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? ∈/ domregister
register′ = register ∪ {p? → pin?} log′ =log
currentTime′ = currentTime status′ = status
locked′ = locked
unlocked′ = unlocked
DeletePerson ∆Status
p? : Person
p? ∈ dom register
register′ = {p?} −▹ register log′ =log
currentTime′ = currentTime status′ = status
locked′ = locked
unlocked′ = 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?
log′ = log ∪ {currentTime → p?} pass! = Enter
locked = locked′
register = register′
currentTime = currentTime′
3
NotAllowedIn ΞStatus
p? : Person pin? : PIN pass! : Report
p? ∈ dom register register p? ̸= 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? ∈/ domregister
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 status′ = closed and unlocked unlocked′ = currentTime locked = locked′
register = register′ currentTime′ = 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 status′ = closed and locked
locked′ = currentTime
unlocked′ = unlocked
register = register′
log = log′
currentTime′ = currentTime
Exiting the building is then achieved by using the Unlock operation. We as- sume 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 un- locked 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
currentTime′ = currentTime + 1 status′ = status
locked′ = locked
unlocked′ = unlocked
register′ = register log′ =log
Exit = [Unlock | log′ = 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 = (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 counter- parts to the single-door operations given above.
5
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.
6