Abstract:
Here, DP-model named in the title is presented. There are many essential features which differ it from DP-models earlier developed for other computer systems. In particular, it contains nonmonotone rules of state transformations being necessary in analysis of conditions for transferring access rights and realizing information flows in OS.