About methods of developing consistent description of the MROSL DP-model for OS and DBMS for its verification with Rodin and ProB tools

Access control mechanism performs one of the main functions to ensure the security of information security tools, such as OS or DBMS. Formal models of access control are developed to achieve confidence in correctness of this mechanism, to create conditions for the scientific justification of its compliance with the security requirements. The paper presents methods of consistent description of the MROSL DP-model in the language used in mathematics (mathematical notation) and in Event-B formal method (formalized notation). The first result of using these methods in refining the formalized notation was provision the possibility of its joint verification by deductive method and method of model checking using the Rodin and ProB tools. The second result was modeling using Event-B formal method of interacting systems with their own developed access control mechanisms, such as OS and DBMS, which is necessary to match the description of the model in mathematical notation. These methods are formed on expression of the properties of the original hierarchical description of the model in mathematical notation in a sequential refinement of the model levels based on the refinement technique of Rodin and on application of total functions instead of directly using axiom of mathematical induction.