I have tried to formalise the natural language requirements into an Event-B model. It is not necessarily complete, and may not be fully in line with the natural language description. But it is a starting point for a discussion.
Formalisation of the key manager
This Event-B model is an attempt to formalise the requirements of the VerifyThis Long Term Challenge 2020. It is deliberately kept on a very high level of abstraction, but should have enough detail to clarify the behaviour of the system.
Links
- PDF documentation of the Event-B model.
- Event-B (RODIN) sources are available on request. Just send me a mail.
Author: Mattias Ulbrich, ulbrich@kit.edu