2.10 Location Access Controller

$\includegraphics[width=7mm]{img/tick_64.png}$
Goals: In this section, we will take a closer look at a few more complex proofs. For this we use the model of a location access controller. The goal is to develop the proofs that ensure there are no deadlocks present in the initial model and in the first refinement.

Through the model used in this section, we study a complete system and remind the proof rules of formal development. The system’s task is to control the access of certain people to different locations of a site. The system is thus based on whether a person has (or does not have) access to a particular location.

Before describing the initial model, import the archive file Doors.zip that contains the model. To do this, select File $\rangle$ Import $\rangle$ General $\rangle$ Existing Project into Workspace. Then select the according archive file and click on Finish. It will take Rodin a few seconds to extract and load all the files.

Rodin Handbook

2.10 Location Access Controller