Static verification of operating system monolithic kernels
| Autor: | Evgeny Novikov |
|---|---|
| Rok vydání: | 2017 |
| Předmět: |
business.industry
Computer science операционная система монолитное ядро формальная спецификация качество программной системы lcsh:QA75.5-76.95 статическая верификация Embedded system декомпозиция программной системы General Earth and Planetary Sciences lcsh:Electronic computers. Computer science business микроядро General Environmental Science |
| Zdroj: | Труды Института системного программирования РАН, Vol 29, Iss 2, Pp 97-116 (2018) |
| ISSN: | 2220-6426 2079-8156 |
| DOI: | 10.15514/ispras-2017-29(2)-4 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|