From the beginning our design was a bit more complicated, but after some feedback we have simplified our design to three classes, Token, IDStation and EnrollmentStation.
The token is more or less just a data container containing fingerprint data of its owner and a clearance level that is in the range \([0, 3]\). The clearance level \(0\) represents an invalidated token.
ID station is where you have to authenticate yourself in order to unlock a door. The important method here is Authenticate that takes a token and an int representing a users fingerprint and sets two boolean flags that represents the door and the alarm dependning on if the authentication “succeeds” or not.
The enrollment station is where a person can be registered as a user. The enrollment station keeps track of all existing users by keeping their fingerprint data in a set, in this way no person can register twice and recieve two tokens. Our model is here somewhat simplified and does not support some things that would be convenient, such as for a user to be re-registered if his/her token has become invalidated for some reason.
Most of our specifications are pretty straight-forward. The ones that are a little bit more advanced are Authenticate in IDStation and Enroll in EnrollmentStation.
Authenticate is, just as it seems, the method that authenticates users, it has three quite large implications in the post conditions that specify when the door should be unlocked and when the alarm should be activated. The post conditions for Authenticate:
\[\begin{aligned} old(t.fingerprint) \neq fp \implies\\ doorIsLocked \land alarmIsOn \land \neg t.IsValid() \land t.ValidClearanceValue()\\ old(t.fingerprint) = fp \land old(t.clearance) < reqClearance \implies\\ doorIsLocked \land \neg alarmIsOn \land t.clearance = old(t.clearance)\\ old(t.fingerprint) = fp \land old(t.clearance) \geq reqClearance \implies\\ \neg doorIsLocked \land \neg alarmIsOn \land t.clearance = old(t.clearance)\end{aligned}\]
Authenticate requires that the door is locked and that the alarm is not active. These preconditions could be different, but we chose to have it this way because it simplified other aspects of the model.
Enroll ensures by its pre and post conditions that a person cannot enroll twice and therefore not recieve more than one token.