RUS  ENG
Full version
JOURNALS // Proceedings of the Institute for System Programming of the RAS // Archive

Proceedings of ISP RAS, 2017 Volume 29, Issue 4, Pages 217–230 (Mi tisp245)

Static verification of Linux kernel configurations

S. V. Kozina, V. S. Mutilinb

a National Research University Higher School of Economics
b Institute for System Programming of the Russian Academy of Sciences

Abstract: The Linux kernel is often used as a real world case study to demonstrate novel software product line engineering research methods. It is one of the most sophisticated programs nowadays. To provide the most safe experience of building of Linux product line variants it is necessary to analyse Kconfig file as well as source code. Ten of thousands of variable statements and options even by the standards of modern software development. Verification researchers offered lots of solutions for this problem. Standard procedures of code verification are not acceptable here due to time of execution and coverage of all configurations. We offer to check the operating system with special wrapper for tools analyzing built code and configuration file connected with coverage metric. Such a bundle is able to provide efficient tool for calculating all valid configurations for predetermined set of code and Kconfig. Metric can be used for improving existing analysis tools as well as decision of choice the right configuration. Our main goal is to contribute to a better understanding of possible defects and offer fast and safe solution to improve the validity of evaluations based on Linux. This solution will be described as a program with instruction for inner architecture implementation.

Keywords: Software Product Lines, Linux, Kconfig, Preprocessor.

Language: English

DOI: 10.15514/ISPRAS-2017-29(4)-14



Bibliographic databases:


© Steklov Math. Inst. of RAS, 2024