Incremental development of environment model and requirement specifications for subsystems of operating system monolithic kernels
Methods and tools for automated static verification aim at detecting all violations of checked requirements in target programs under certain assumptions even without complete models and formal specifications. The given feature form a basis of the suggested method for incremental development of envir...
| Main Authors: | , |
|---|---|
| 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/417 |
| _version_ | 1831613938327879680 |
|---|---|
| author | I. S. Zakharov E. M. Novikov |
| author_facet | I. S. Zakharov E. M. Novikov |
| author_sort | I. S. Zakharov |
| collection | DOAJ |
| description | Methods and tools for automated static verification aim at detecting all violations of checked requirements in target programs under certain assumptions even without complete models and formal specifications. The given feature form a basis of the suggested method for incremental development of environment model and requirement specifications for subsystems of operating system monolithic kernels. This method was implemented on top of static verification framework Klever. It was evaluated by checking the Linux kernel TTY subsystem. During this study some Klever components were improved. Besides, we fixed some existing and developed new environment model and requirement specifications. Almost all made changes also helps at static verification of loadable modules of the Linux kernel. Developers of automated static verification tool CPAchecker fixed several issues that we revealed and reported during the research. Overall developed specifications allowed to increase function coverage of the TTY subsystem from 5% to 83%. Moreover, we revealed 7 bugs in loadable modules verified together with the TTY subsystem. |
| first_indexed | 2024-12-18T19:18:10Z |
| format | Article |
| id | doaj.art-8ca3c360c1714259bf799ed4b16b7f40 |
| institution | Directory Open Access Journal |
| issn | 2079-8156 2220-6426 |
| language | English |
| last_indexed | 2024-12-18T19:18:10Z |
| publishDate | 2018-10-01 |
| publisher | Ivannikov Institute for System Programming of the Russian Academy of Sciences |
| record_format | Article |
| series | Труды Института системного программирования РАН |
| spelling | doaj.art-8ca3c360c1714259bf799ed4b16b7f402022-12-21T20:56:05ZengIvannikov Institute for System Programming of the Russian Academy of SciencesТруды Института системного программирования РАН2079-81562220-64262018-10-01296254810.15514/ISPRAS-2017-29(6)-2417Incremental development of environment model and requirement specifications for subsystems of operating system monolithic kernelsI. S. Zakharov0E. M. Novikov1Институт системного программирования им. В.П. Иванникова РАНИнститут системного программирования им. В.П. Иванникова РАНMethods and tools for automated static verification aim at detecting all violations of checked requirements in target programs under certain assumptions even without complete models and formal specifications. The given feature form a basis of the suggested method for incremental development of environment model and requirement specifications for subsystems of operating system monolithic kernels. This method was implemented on top of static verification framework Klever. It was evaluated by checking the Linux kernel TTY subsystem. During this study some Klever components were improved. Besides, we fixed some existing and developed new environment model and requirement specifications. Almost all made changes also helps at static verification of loadable modules of the Linux kernel. Developers of automated static verification tool CPAchecker fixed several issues that we revealed and reported during the research. Overall developed specifications allowed to increase function coverage of the TTY subsystem from 5% to 83%. Moreover, we revealed 7 bugs in loadable modules verified together with the TTY subsystem.https://ispranproceedings.elpub.ru/jour/article/view/417операционная системамонолитное ядрокачество программной системыстатическая верификацияформальная спецификациядекомпозиция программной системымодель окружения |
| spellingShingle | I. S. Zakharov E. M. Novikov Incremental development of environment model and requirement specifications for subsystems of operating system monolithic kernels Труды Института системного программирования РАН операционная система монолитное ядро качество программной системы статическая верификация формальная спецификация декомпозиция программной системы модель окружения |
| title | Incremental development of environment model and requirement specifications for subsystems of operating system monolithic kernels |
| title_full | Incremental development of environment model and requirement specifications for subsystems of operating system monolithic kernels |
| title_fullStr | Incremental development of environment model and requirement specifications for subsystems of operating system monolithic kernels |
| title_full_unstemmed | Incremental development of environment model and requirement specifications for subsystems of operating system monolithic kernels |
| title_short | Incremental development of environment model and requirement specifications for subsystems of operating system monolithic kernels |
| title_sort | incremental development of environment model and requirement specifications for subsystems of operating system monolithic kernels |
| topic | операционная система монолитное ядро качество программной системы статическая верификация формальная спецификация декомпозиция программной системы модель окружения |
| url | https://ispranproceedings.elpub.ru/jour/article/view/417 |
| work_keys_str_mv | AT iszakharov incrementaldevelopmentofenvironmentmodelandrequirementspecificationsforsubsystemsofoperatingsystemmonolithickernels AT emnovikov incrementaldevelopmentofenvironmentmodelandrequirementspecificationsforsubsystemsofoperatingsystemmonolithickernels |