Proceedings of the Institute for System Programming of the RAS
RUS  ENG    JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PACKAGE AMSBIB  
General information
Latest issue
Archive

Search papers
Search references

RSS
Latest issue
Current issues
Archive issues
What is RSS



Proceedings of ISP RAS:
Year:
Volume:
Issue:
Page:
Find






Personal entry:
Login:
Password:
Save password
Enter
Forgotten password?
Register


Proceedings of the Institute for System Programming of the RAS, 2017, Volume 29, Issue 4, Pages 217–230
DOI: https://doi.org/10.15514/ISPRAS-2017-29(4)-14
(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
References:
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.
Bibliographic databases:
Document Type: Article
Language: English
Citation: S. V. Kozin, V. S. Mutilin, “Static verification of Linux kernel configurations”, Proceedings of ISP RAS, 29:4 (2017), 217–230
Citation in format AMSBIB
\Bibitem{KozMut17}
\by S.~V.~Kozin, V.~S.~Mutilin
\paper Static verification of Linux kernel configurations
\jour Proceedings of ISP RAS
\yr 2017
\vol 29
\issue 4
\pages 217--230
\mathnet{http://mi.mathnet.ru/tisp245}
\crossref{https://doi.org/10.15514/ISPRAS-2017-29(4)-14}
\elib{https://elibrary.ru/item.asp?id=29968653}
Linking options:
  • https://www.mathnet.ru/eng/tisp245
  • https://www.mathnet.ru/eng/tisp/v29/i4/p217
  • Citing articles in Google Scholar: Russian citations, English citations
    Related articles in Google Scholar: Russian articles, English articles
    Proceedings of the Institute for System Programming of the RAS
    Statistics & downloads:
    Abstract page:120
    Full-text PDF :89
    References:33
     
      Contact us:
     Terms of Use  Registration to the website  Logotypes © Steklov Mathematical Institute RAS, 2024