” 辅导COMPX554程序、System留学生程序 写作、 写作JavaSecurity SystemExtending the single door to a whole collectionSteve ReevesThis document gives the requirements and a corresponding model in Z for asecurity system for a door in a building.It is probably somewhat simpler than your model since Ive ignored one ortwo features.1 RequirementsThe door has its Security controlled by a swipe-card system. The system consistsof a database that records for each user of the system what their personalidentification 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 buttonmarked Push To Exit. The system unlocks the door, allowing the person toleave. The door remains unlocked for a certain amount of time, as given by asystem constant. After this time the door is locked.To enter through the door, the person swipes their card and presses keysthat correspond to their four-digit PIN. The system checks that the person hasgiven the correct PIN and that they are allowed through the door. If these twoconditions are met, the system unlocks the door. The door remains unlockedfor a certain amount of time, as given by a system constant. After this timethe door is locked. The system also records the fact that the person concernedused the entry mechanism.The doors status can be determined at any time by the system, and itsstatus 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 isactivated within the building, the doors status must be closed and unlocked oropen.1.1 A model 辅导COMPX554作业、System留学生作业 写作We must make available operations that initialise the system, allow entry, allowexit, unlock a door in an emergency, allow adding a user, deleting a user,amending a user and logging a users 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:1DoorStatus ::= closed and locked | closed and unlocked | open(We will find that open is not neededfrom the systems point-of-view adoor is either unlocked or not. A more fancy system might record the open orclosed 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 recordsthe last times at which the door unlocked and locked. We also need to recordwho can have access to this door, for which we use a database (modelled as apartial function) from People (in the type Person) to PINs. We use log to makea note of the fact that a person used the door at a certain time. We assumethere is a clock whose time we can read using the observation currentTime.Youll note that I have defined a type Time and given it a very small range.This is to make the searching for solutions bearableI have been running thismodel with timeout for enabling operations set to 30000ms. This isnt too longto wait and within the six Units of time that we can tick through a realistic setof operations can be done. Note that the thing which causes a problem here isthe 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. (Inthe LATEX version of this file I have commented out the fact that log does notchange, so you can comment out the change to log and uncomment the equationthat says log does not Change. Once you have done that you can change theupper bound to Time to be a realistically large number.)Person ::= p1 | p2PIN ::= pin1 | pin2Time == 0 . . 6Statusstatus : DoorStatuslocked, unlocked : Timeregister : Person 7 PINlog : Time 7 PersoncurrentTime : TimeThe status of the door is initialised by assuming it is closed and locked andsetting the time observations to the current time. The register is also empty atfirst, as is the log.InitStatusstatus = closed and lockedlocked = unlocked = currentTime = 0register = log = We need to be able to add people to and delete them from the register.2AddPersonStatusp? : Personpin? : PINp? / dom registerregister 0 = register {p? 7 pin?}log0 = logcurrentTime0 = currentTimestatus0 = statuslocked0 = lockedunlocked0 = unlockedDeletePersonStatusp? : Personp? dom registerregister 0 = {p?} C registerlog0 = logcurrentTime0 = currentTimestatus0 = statuslocked0 = lockedunlocked0 = unlockedAmending a persons record is also needed but we omit it here since it is astraightforward operation to add.We have two operations which test the persons PIN to see if it is valid, withreports.Report ::= Enter | Invalid PIN | Not RegisteredAllowedInStatusp? : Personpin? : PINpass! : Reportp? dom registerregister p? = pin?log0 = log {currentTime 7 p?}pass! = Enterlocked = locked0register = register 0currentTime = currentTime03NotAllowedInStatusp? : Personpin? : PINpass! : Reportp? dom registerregister p? 6= pin?pass! = Invalid PINWe also need to handle the case (and not let them in) when the person issimply not in the register:NotRegisteredStatusp? : Personpass! : Reportp? / dom registerpass! = Not RegisteredThere are then operations representing the use of a doors controllers (oneon the inside and one on the outside). If the inside button is pressed the doorsstatus must become closed and unlocked. The door should also have a lockoperation. These operations change the times recorded appropriately too. Tomodel the fact that the door remains unlocked for only a certain amount of timewe represent this chosen time interval byopening time : Timeopening time = 1UnlockStatusstatus = closed and lockedstatus0 = closed and unlockedunlocked0 = currentTimelocked = locked0register = register 0currentTime0 = currentTimeAccording to this definition, a person can only swipe and enter once the doorhas (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 peoplemight enter the building (without swiping their cards) once just one person hasswiped their card (before the door locks), and a person might swipe and unlockthe door, but then not actually go into the building. (This is why we havehuman security officers, and do not rely on a database to tell us who is in abuildingit cannot be relied on!)4LockStatusstatus = closed and unlockedunlocked currentTime opening timestatus0 = closed and lockedlocked0 = currentTimeunlocked0 = unlockedregister = register 0log = log0currentTime0 = currentTimeExiting the building is then achieved by using the Unlock operation. We assumethat 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 unlockedfor the required amount of time, after which it will succeed and the doorwill lock.) Time progresses for the system, and we model this (for animationpurposes) by the operation Tick.TickStatuscurrentTime0 = currentTime + 1status0 = statuslocked0 = lockedunlocked0 = unlockedregister 0 = registerlog0 = logExit = [ b Unlock | log0 = log]The operation for entering the building is now one of testing the personsPIN and unlocking the door, or not, as appropriate:Entry = ( b AllowedIn Unlock) NotAllowedIn NotRegisteredAgain 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 useof 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 systemfor several doors. For the purposes of animation using ProB, the set DIN (seethe first handout for this coursework) should have just two members.You need to develop an indexed set (e.g. a function, perhaps) of instancesof Status to represent a door database. You then need framing or promotionschemas with which you can define (as one-liners) the system-level counterpartsto the single-door operations given above.5So, we need SysExit, SysEntry, SysLock, SysAddPerson and SysDeletePerson.We will also need operation to add and delete doors from the collection whichforms the system.The final thing to do is to specify ticking at the system level. This needs tobe done using Tick exactly as given. So, we need a single operation SysTickwhich 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 operationSysTickAux by simple promotion, and this operation should make the givendoors time tick; the second should define an operation SysTick that usesSysTickAux for each possible door and makes its time tick forward, so it isan operation composed from several uses of SysTickAux each specialised to oneof 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 logupdates commented out, as explained where I mention the set Time near thebeginning of the previous section.6如有需要，请加QQ：99515681 或邮箱：99515681@qq.com
“
添加老师微信回复‘’官网 辅导‘’获取专业老师帮助，或点击联系老师1对1在线指导。
