Event-B

Last updated Mar 28, 2023 Edit Source

A formal specification framework based on Set Theory.

A system for controlling access to a university building

• An university has some fixed number of students.
• Students can be inside or outside the university building.
• The system should allow a new student to be registered in order to get the access to the university building.
• To deny the access to the building for a student the system should support deregistration.
• The system should allow only registered students to enter the university building.

• A system should support adding a permission for a student in order to get an access to a particular printer and removing a permission.
• A system should support removing a student’s access to all printers at once.
• A system should support giving the combined permissions of any two students to both of them.

• To keep track of changing permissions, it will make use of a variable access whose type is a relation between STUDENTS and PRINTERS.