Проектирование сертифицированного компилятора предикатных программ
Аннотация
Компилятор со средствами дедуктивной верификации подлежит тщательной сертификации для подтверждения высокого уровня доверия к результатам дедуктивной верификации. Разработка компилятора предикатных программ на базе его модели в соответствии с модельно-ориентированной технологией повышает уровень доверия к компилятору. Главной частью модели компилятора является модель внутреннего представления программы, реализуемая в рамках третьего релиза компилятора предикатных программ. В настоящей работе описывается архитектура модели внутреннего представления программы. Важнейшим аспектом модели является анализ типов. В описании модели используется специально разработанный язык спецификации структур данных компилятора. Верификация модели и разработка программы компилятора на базе модели обеспечат высокую надежность компилятора.
Об авторе
В. И. Шелехов
Институт систем информатики имени А. П. Ершова СО РАН; НГУ
Россия
Россия
Шелехов Владимир Иванович, к.т.н., зав. лаб. системного программирования, Институт систем информатики имени А. П. Ершова СО РАН; доцент кафедры программирования НГУ
630090, Новосибирск, просп. Ак. Лаврентьева, 6, тел. (383) 330-27-21
Список литературы
1. Шелехов В. И., Чушкин М. С. Верификация программы быстрой сортировки с двумя опорными элементами // Научный сервис в сети Интернет. М.: ИПМ им. М. В. Келдыша, 2018. 26 с. URL: http://persons.iis.nsk.su/files/persons/pages/dqsort.pdf (дата обращения: 12.03.2019).
2. ГОСТ Р ИСО/МЭК 15408-3-2013. Информационная технология. Методы и средства обеспечения безопасности. Критерии оценки безопасности информационных технологий. Часть 3. Компоненты доверия к безопасности. М.: Стандартинформ, 2014. 150 с.
3. Kästner D., Wünsche U., Barrho J., Schlickling M., Schommer B., Schmidt M., Ferdinand C., Leroy X., Blazy S. CompCert: Practical experience on integrating and qualifying a formally verified optimizing compiler // ERTS 2018: Embedded Real Time Software and Systems. SEE, January 2018. P. 1–9.
4. Coq Proof Assistant [Электронный ресурс]. URL: https://coq.inria.fr/ (дата обращения: 12.03.2019).
5. Карнаухов Н. С., Першин Д. Ю., Шелехов В. И. Язык предикатного программирования Новосибирск, 2018. 42 с. URL: http://persons.iis.nsk.su/files/persons/pages/plang14.pdf (дата обращения: 12.03.2019).
6. Девянин П. Н., Ефремов Д. В., Кулямин В. В., Петренко А. К., Хорошилов А. В., Щепетков И. В. Моделирование и верификация политик безопасности управления доступом в операционных системах // М.: Горячая линия – Телеком, 2019. 261 с. URL: http://www.ispras.ru/publications/security_policy_modeling_and_verific ation.pdf (дата обращения: 21.03.2019).
7. Операционные системы Astra Linux [Электронный ресурс]. URL: http://www.astralinux.ru (дата обращения: 12.03.2019).
8. Шелехов В. И. Проект системы предикатного программирования. Новосибирск: ИСИ СО РАН, 2018. 24 с. URL: http://persons.iis.nsk.su/files/persons/pages/project1.pdf (дата обращения: 12.03.2019).
9. Шелехов В. И. Семантика языка предикатного программирования // ЗОНТ-15. Новосибирск, 2015. 13 с. URL: http://persons.iis.nsk.su/files/persons/pages/semZont1.pdf (дата обращения: 12.03.2019).
10. Каблуков И. В., Шелехов В. И. Реализация оптимизирующих трансформаций в системе предикатного программирования // Системная информатика. 2017. № 11. С. 21–48. Электрон. журн. 2018. URL: http://persons.iis.nsk.su/files/persons/pages/opttransform4.pdf (дата обращения: 12.03.2019).
Рецензия
Для цитирования:
Шелехов В.И. Проектирование сертифицированного компилятора предикатных программ. Вестник СибГУТИ. 2019;(3):89-95.
For citation:
Shelekhov V. Certified compiler design of predicate programs. The Herald of the Siberian State University of Telecommunications and Information Science. 2019;(3):89-95. (In Russ.)
Просмотров:
381
Послать статью по эл. почте 