Geodesic
The techniques of formalization of OS Astra Linux Special Edition access control model using Event-B formal method for verification using Rodin and ProB
Prikladnaâ diskretnaâ matematika, no. 2 (2021), pp. 83-96

Voir la notice de l'article provenant de la source Math-Net.Ru

The paper presents techniques to specification access control model of OS Astra Linux Special Edition (the MROSL DP-model) in the formalized notation (formalized using the Event-B formal method), that are based on the use of several global types, separation of general total functions into specific total functions, reduction in the number of invariants and guard of events, which iterate over subsets of a certain set. The result of using these techniques was the simplification of automated deductive verification of formalized notation using the Rodin tool and adaptation of the model to verification by model checking formalized notation using the ProB tool. These techniques can be useful in development of the MROSL DP-model, and also in development of other access control models and verification using appropriate tools.
Keywords: access control model, deductive verification, Event-B, Rodin, model checking, ProB. 
@article{PDM_2021_2_a4,
     author = {P. N. Devyanin and M. A. Leonova},
     title = {The techniques of formalization of {OS} {Astra} {Linux} {Special} {Edition} access control model using {Event-B} formal method for verification using {Rodin} and {ProB}},
     journal = {Prikladna\^a diskretna\^a matematika},
     pages = {83--96},
     publisher = {mathdoc},
     number = {2},
     year = {2021},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/PDM_2021_2_a4/}
}
TY  - JOUR
AU  - P. N. Devyanin
AU  - M. A. Leonova
TI  - The techniques of formalization of OS Astra Linux Special Edition access control model using Event-B formal method for verification using Rodin and ProB
JO  - Prikladnaâ diskretnaâ matematika
PY  - 2021
SP  - 83
EP  - 96
IS  - 2
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/PDM_2021_2_a4/
LA  - ru
ID  - PDM_2021_2_a4
ER  - 
%0 Journal Article
%A P. N. Devyanin
%A M. A. Leonova
%T The techniques of formalization of OS Astra Linux Special Edition access control model using Event-B formal method for verification using Rodin and ProB
%J Prikladnaâ diskretnaâ matematika
%D 2021
%P 83-96
%N 2
%I mathdoc
%U http://geodesic.mathdoc.fr/item/PDM_2021_2_a4/
%G ru
%F PDM_2021_2_a4
P. N. Devyanin; M. A. Leonova. The techniques of formalization of OS Astra Linux Special Edition access control model using Event-B formal method for verification using Rodin and ProB. Prikladnaâ diskretnaâ matematika, no. 2 (2021), pp. 83-96. http://geodesic.mathdoc.fr/item/PDM_2021_2_a4/