代写COMPX554、System留学生代做、代做Java，c/c++，Python程序语言

日期：2020-10-10 11:09

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.

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