Access Control System

Chapter 8 introduced the equational specification style in an example-driven manner. The examples ofChapter 8 have been chosen to explain the basic principles of the equational style. They are therefore all tiny and a bit artificial. In this chapter, we apply the equational style to model an access control system (ACS). Thereby we demonstrate the suitability of the equational style in a more realistic context. A specification of the ACS first appeared in [BH93], from which we have adapted the following informal specification.