Consider the specification of the document management system described below:
A document management system consists of three components: 1) a document terminal which is a user interface whereby the user may enter information about himself/herself to access the system, 2) a Guard Service which verifies that the user has access to the document server and provides this access, and 3) a document server which may be used to insert documents, delete documents, or transfer documents from one repository to another.
The document terminal will request from the user a login id and a password and will convey this information to the Guard Service. If the user is authenticated, an indicator will be given to a Location Service. This Location Service locates the documents accessible by the user depending on the user's security level, which is implied by the indicator. One such id is an administrative id which allows user information to be added or updated. The type of information collected about each user is login name, actual name, agency (CIA, DoD, FBI, NSA, USA, USAF, USN), and security level.
The authentication server allows a login with correct password to either add users as indicated above or to access the document server. The authentication server will block further access by a login id after 5 unsuccessful attempts without a successful one. All login attempts are logged, whether successful or unsuccessful.
The document server associates repositories for documents at different security levels. The repository will only be exposed to the users with the corresponding security level. The security level will indicate which repositories the user has access to and whether this access is read only or read/write. Even if the user has read/write access to a certain repository, he/she may not remove a document belonging to a service he/she does not belong to (e.g. a CIA agent may not remove FBI owned documents). If a user attempts five invalid operations, his/her login id will be disabled. All transactions are logged, whether successful or unsuccessful.
Both the authentication and document servers will operate concurrently in order to service many different client requests from various terminals.
Your final report should include: 1) a discussion of the requirements as stated, especially indicating what domain or other implicit knowledge you assumed to complete the specification and rationale for preconditions, postconditions, permission predicates, or their absense, 2) the VDM++ specification, 3) a UML model corresponding to that specification (i.e. you may generate it from the VDM++ rather than enter it directly), and 4) a sample run of your executable system, showing a sequence of operations and the resulting repositories.