Static Verification of Linux Kernel Configurations
| Autor: | S. V. Kozin, V. S. Mutilin |
|---|---|
| Jazyk: | English<br />Russian |
| Rok vydání: | 2018 |
| Předmět: | |
| Zdroj: | Труды Института системного программирования РАН, Vol 29, Iss 4, Pp 217-230 (2018) |
| Druh dokumentu: | article |
| ISSN: | 2079-8156 2220-6426 |
| DOI: | 10.15514/ISPRAS-2017-29(4)-14 |
| Popis: | 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. |
| Databáze: | Directory of Open Access Journals |
| Externí odkaz: |
|