To obtain access to full text of journal and articles you must register!
- Article name
- Application of TLA+ notation for describing the model of isolated program environment of subjects and its further verification
- Authors
- Kanner A. M., , kanner@okbsapr.ru, JSC "OKB SAPR", Moscow, Russia
- Keywords
- IPES model / IPES model specification / IPES model verification / Lamport's temporal logic of actions / TLA+ / Model Checking method
- Year
- 2021 Issue 3 Pages 8 - 11
- Code EDN
- Code DOI
- 10.52190/2073-2600_2021_3_8
- Abstract
- The article considers the disadvantages of verification of mathematical notations of the security models. It is proposed to use the Lamport's temporal logic of actions to represent the security models in a formal language suitable for verification which will be held using specialized tools. The model of isolated program environment of subjects is considered, it's specification is given in TLA+ notation, and the advantages of verifying this specification using specialized tools are described.
- Text
- BUY for read the full text of article
- Buy
- 500.00 rub
