• A
  • A
  • A
  • ABC
  • ABC
  • ABC
  • А
  • А
  • А
  • А
  • А
Regular version of the site
For visually-impairedUser profile (HSE staff only)Search

Program for Static Verification of Configurations of Linux Operating System Kernel

Student: Svyatoslav Kozin

Supervisor: Alexander K. Petrenko

Faculty: Faculty of Computer Science

Educational Programme: Software Engineering (Bachelor)

Year of Graduation: 2017

Current work is dedicated to process of variability-aware Linux kernel verification. The Linux kernel is often used as a real world case study to demonstrate novel software product line engineering research methods. 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. Tens of thousands of variable, statements and options is a huge number 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, so it was offered to check the operating system with special wrapper for tools analyzing built code and configuration file. Such a bundle is able to provide efficient tool for calculating all valid configurations for predetermined set of code and Kconfig. These analyses 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. The built solution uses such tools as Undertaker, z3, CPAchecker and has console interface. The paper contains 39 pages, 3 chapters, 10 illustrations, 31 bibliography items, 4 appendices. Keywords: Software Product Lines, Linux, Kconfig, Preprocessor.

Student Theses at HSE must be completed in accordance with the University Rules and regulations specified by each educational programme.

Summaries of all theses must be published and made freely available on the HSE website.

The full text of a thesis can be published in open access on the HSE website only if the authoring student (copyright holder) agrees, or, if the thesis was written by a team of students, if all the co-authors (copyright holders) agree. After a thesis is published on the HSE website, it obtains the status of an online publication.

Student theses are objects of copyright and their use is subject to limitations in accordance with the Russian Federation’s law on intellectual property.

In the event that a thesis is quoted or otherwise used, reference to the author’s name and the source of quotation is required.

Search all student theses