Proceedings of ISP RAS

Integration Points of Operating System Verification Techniques

A. K. Petrenko (ISP RAS, Moscow; MSU, Moscow; MIPT, Moscow; HSE, Moscow), V. V. Kuliamin (ISP RAS, Moscow; MSU, Moscow; HSE, Moscow), A. V. Khoroshilov (ISP RAS, Moscow; MSU, Moscow; MIPT, Moscow; HSE, Moscow)


In this work the problem of high quality verification techniques applicable for operating systems is formulated. A perspective approach to solve this problem is integration of various verification methods. The solution technique can be considered successful if it allows to check the whole operating system and to verify in more accurate way the most important functions and components of the system, using more strict and formal methods for it. Based on the ISP RAS experience in operating system verification projects conducted using various verification techniques we determine development artifacts, that can be suitable integration point candidates for integration of formal specification based static and dynamic verification techniques for operating systems.
The article proposes to define common (shared) artifacts based on the consideration of typical verification tasks. Typical problems encountered in the use of different techniques of verification, provide the basis for integration techniques and verification processes. These types of problems are: the definition of a software contracts of modules (functions); the construction of the model environment; building the path, demonstrating the error; bringing levels of abstraction and assessment of the completeness of the verification. To the greatest extent on the role of artifacts representing the points of integration claim: software contract specifications, environment models and measurement of verification completeness.


Theorem proving, software model checking, model-based testing, operating system, integration of verification methods, software contracts


Proceedings of the Institute for System Programming, vol. 27, issue 5, 2015, pp. 175-190.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2015-27(5)-10

Full text of the paper in pdf (in Russian) Back to the contents of the volume