Static verification of operating system monolithic kernels
The most of modern widely used operating systems have monolithic kernels since this architecture aims at reaching maximum performance. Usually monolithic kernels without various extensions like device drivers consist of several million lines of code in the programming language C/C++ and in the assem...
Main Author: | |
---|---|
Format: | Article |
Language: | English |
Published: |
Ivannikov Institute for System Programming of the Russian Academy of Sciences
2018-10-01
|
Series: | Труды Института системного программирования РАН |
Subjects: | |
Online Access: | https://ispranproceedings.elpub.ru/jour/article/view/254 |
id |
doaj-9f4093ac999b497aab2a10e6b612d24a |
---|---|
record_format |
Article |
spelling |
doaj-9f4093ac999b497aab2a10e6b612d24a2020-11-25T02:17:53Zeng Ivannikov Institute for System Programming of the Russian Academy of SciencesТруды Института системного программирования РАН2079-81562220-64262018-10-012929711610.15514/ISPRAS-2017-29(2)-4254Static verification of operating system monolithic kernelsE. M. Novikov0Институт системного программирования РАНThe most of modern widely used operating systems have monolithic kernels since this architecture aims at reaching maximum performance. Usually monolithic kernels without various extensions like device drivers consist of several million lines of code in the programming language C/C++ and in the assembly language. With time, their source code evolves quite intensively: a new functionality is supported, various operations are optimized, bugs are fixed. The high practical value of operating system monolithic kernels defines strict requirements for their functionality, security, reliability and performance. Approaches for software quality assurance which are currently used in practice help to identify and to fix quite a number of bugs, but none of them allows to detect all possible bugs of kinds sought for. This article shows that different approaches to static verification, which are aimed at solving this task, have significant restrictions if applied to monolithic kernels as a whole, primarily due to a large size and complexity of source code that is constantly evolving. As a first step towards static verification of operating system monolithic kernels a method is proposed for decomposition of kernels into subsystems.https://ispranproceedings.elpub.ru/jour/article/view/254операционная системамонолитное ядромикроядрокачество программной системыстатическая верификацияформальная спецификациядекомпозиция программной системы |
collection |
DOAJ |
language |
English |
format |
Article |
sources |
DOAJ |
author |
E. M. Novikov |
spellingShingle |
E. M. Novikov Static verification of operating system monolithic kernels Труды Института системного программирования РАН операционная система монолитное ядро микроядро качество программной системы статическая верификация формальная спецификация декомпозиция программной системы |
author_facet |
E. M. Novikov |
author_sort |
E. M. Novikov |
title |
Static verification of operating system monolithic kernels |
title_short |
Static verification of operating system monolithic kernels |
title_full |
Static verification of operating system monolithic kernels |
title_fullStr |
Static verification of operating system monolithic kernels |
title_full_unstemmed |
Static verification of operating system monolithic kernels |
title_sort |
static verification of operating system monolithic kernels |
publisher |
Ivannikov Institute for System Programming of the Russian Academy of Sciences |
series |
Труды Института системного программирования РАН |
issn |
2079-8156 2220-6426 |
publishDate |
2018-10-01 |
description |
The most of modern widely used operating systems have monolithic kernels since this architecture aims at reaching maximum performance. Usually monolithic kernels without various extensions like device drivers consist of several million lines of code in the programming language C/C++ and in the assembly language. With time, their source code evolves quite intensively: a new functionality is supported, various operations are optimized, bugs are fixed. The high practical value of operating system monolithic kernels defines strict requirements for their functionality, security, reliability and performance. Approaches for software quality assurance which are currently used in practice help to identify and to fix quite a number of bugs, but none of them allows to detect all possible bugs of kinds sought for. This article shows that different approaches to static verification, which are aimed at solving this task, have significant restrictions if applied to monolithic kernels as a whole, primarily due to a large size and complexity of source code that is constantly evolving. As a first step towards static verification of operating system monolithic kernels a method is proposed for decomposition of kernels into subsystems. |
topic |
операционная система монолитное ядро микроядро качество программной системы статическая верификация формальная спецификация декомпозиция программной системы |
url |
https://ispranproceedings.elpub.ru/jour/article/view/254 |
work_keys_str_mv |
AT emnovikov staticverificationofoperatingsystemmonolithickernels |
_version_ |
1724884522681499648 |