Preview

Труды Института системного программирования РАН

Расширенный поиск

Инкрементальное построение спецификаций моделей окружения и требований для подсистем монолитного ядра операционных систем

https://doi.org/10.15514/ISPRAS-2017-29(6)-2

Полный текст:

Аннотация

Методы и инструменты автоматической статической верификации позволяют выявить все ошибки искомых видов в целевых программах при выполнении определенных предположений даже в условиях отсутствия полных моделей и формальных спецификаций. Эта возможность является основой предлагаемого в работе метода инкрементального построения спецификаций моделей окружения и требований для подсистем монолитного ядра операционных систем. Данный метод был реализован в системе статической верификации Klever и применен для проверки подсистемы поддержки терминальных устройств ядра ОС Linux.

Об авторах

И. С. Захаров
Институт системного программирования им. В.П. Иванникова РАН
Россия


Е. М. Новиков
Институт системного программирования им. В.П. Иванникова РАН
Россия


Список литературы

1. Е.М. Новиков. Возможности статической верификации монолитного ядра операционных систем. Труды ИСП РАН, том 29, вып. 2, 2017 г., стр. 97-116. DOI: 10.15514/ISPRAS-2017-29(2)-4

2. Е.М. Новиков. Развитие ядра операционной системы Linux. Труды ИСП РАН, том 29, вып. 2, 2017 г., стр. 77-96. DOI: 10.15514/ISPRAS-2017-29(2)-3

3. D. Engler, M. Musuvathi. Static analysis versus model checking for bug finding. In Proceedings of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'04), LNCS, volume 2937, pp. 191-210, 2004.

4. T. Ball, S.K. Rajamani. SLIC: A specification language for interface checking of C. Technical Report MSR-TR-2001-21, Microsoft Research, 2001.

5. Е.М. Новиков. Развитие метода контрактных спецификаций для верификации модулей ядра операционной системы Linux. Диссертация на соискание ученой степени кандидата физико-математических наук, Институт системного программирования РАН, 2013.

6. A. Khoroshilov, V. Mutilin, E. Novikov, I. Zakharov. Modeling Environment for Static Verification of Linux Kernel Modules. In Proceedings of the 9th International Ershov Informatics Conference (PSI'14), LNCS, vol. 8974, pp. 400-414, 2014.

7. K.R.M. Leino. Developing verified programs with Dafny. In Proceedings of the 2013 International Conference on Software Engineering (ICSE '13), pp. 1488-1490, 2013.

8. П.Н. Девянин, В.В. Кулямин, А.К. Петренко, А.В. Хорошилов, И.В. Щепетков. Сравнение способов декомпозиции спецификаций на Event-B. Программирование, т. 42, № 4, стр. 17-26, 2016.

9. М.У. Мандрыкин, В.С. Мутилин. Обзор подходов к моделированию памяти в инструментах статической верификации. Труды ИСП РАН, том 29, вып. 1, 2017 г., стр. 195-230. DOI: 10.15514/ISPRAS-2017-29(1)-12

10. М.У. Мандрыкин, А.В. Хорошилов. О дедуктивной верификации Си программ, работающих с разделяемыми данными. Труды ИСП РАН, том 27, выпуск 4, стр, 49-68, 2015. DOI: 10.15514/ISPRAS-2015-27(4)-4

11. G. Klein, J. Andronick, K. Elphinstone, T. Murray, T. Sewell, R. Kolanski, G. Heiser. Comprehensive formal verification of an OS microkernel. ACM Transactions on Computer Systems (TOCS), vol. 32, issue 1, 70 p., 2014.

12. Д. Бейер, А.К. Петренко. Верификация драйверов операционной системы Linux. Труды ИСП РАН, том 23, стр. 405-412, 2012. DOI: 10.15514/ISPRAS-2012-23-23

13. И.С. Захаров, М.У. Мандрыкин, В.С. Мутилин, Е.М. Новиков, А.К. Петренко, А.В. Хорошилов. Конфигурируемая система статической верификации модулей ядра операционных систем. Программирование, том 41, № 1, стр. 44-67, 2015.

14. E. Novikov, I. Zakharov. Towards Automated Static Verification of GNU C Programs. In Proceedings of the 11th International Ershov Informatics Conference (PSI'17), LNCS, volume 10742, 2018 (в печати).

15. D. Beyer, M.E. Keremoglu. CPAchecker: A tool for configurable software verification. In: Proceedings of the 23rd International Conference on Computer Aided Verification, Berlin, Heidelberg, Springer, pp. 184 190, 2011.


Для цитирования:


Захаров И.С., Новиков Е.М. Инкрементальное построение спецификаций моделей окружения и требований для подсистем монолитного ядра операционных систем. Труды Института системного программирования РАН. 2017;29(6):25-48. https://doi.org/10.15514/ISPRAS-2017-29(6)-2

For citation:


Zakharov I.S., Novikov E.M. Incremental development of environment model and requirement specifications for subsystems of operating system monolithic kernels. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2017;29(6):25-48. (In Russ.) https://doi.org/10.15514/ISPRAS-2017-29(6)-2

Просмотров: 62


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)