2.10 Proving Deadlock Freeness

Goals: In this section, we will take a closer look at a few more complex proofs. Here 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.

This example has been taken from the Event-B book (1.2.1) and is quite sophisticated. In this section, we are dealing with a subset of the complete model. We encourage readers to consult the example in the book.

Through the model used in this section, we study a complete system and mention the proof rules of formal development. This system’s job 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 Import General 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.