Proceedings of ISP RAS

Verification and analysis of variable operating systems

V.V. Kuliamin (ISP RAS, Moscow, Russia, MSU, Moscow, Russia, HSE, Moscow, Russia)
E.M. Lavrischeva (ISP RAS, Moscow, Russia, MIPT, Moscow, Russia)
V.S. Mutilin (ISP RAS, Moscow, Russia)
A.K. Petrenko (ISP RAS, Moscow, Russia, MSU, Moscow, Russia, HSE, Moscow, Russia)


This paper regards problems of analysis and verification of complex modern operating systems, which should take into account variability and configurability of those systems. The main problems of current interest are related with conditional compilation as variability mechanism widely used in system software domain. It makes impossible fruitful analysis of separate pieces of code combined into system variants, because most of these pieces of code has no interface and behavior. From the other side, analysis of all separate variants is also impossible due to their enormous number. The paper provides an overview of analysis methods that are able to cope with the stated problems, distinguishing two classes of such approaches: analysis of variants sampling based on some variants coverage criteria and variation-aware analysis processing many variants simultaneously and using similarities between them to minimize resources required. For future development we choose the most scalable technics, sampling analysis based on code coverage and on coverage of feature combinations and variation-aware analysis using counterexample guided abstraction refinement approach.


operating system, software product family, variability model, software verification, static analysis, model checking, type safety checking, source code coverage, covering array, counterexample-guided abstraction refinement


Proceedings of the Institute for System Programming, vol. 28, issue 3, 2016, pp. 189-208.

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

DOI: 10.15514/ISPRAS-2016-28(3)-12

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