Просмотр статьи


Номер журнала: 2019.3

Заголовок статьи: Проектирование сертифицированного компилятора предикатных программ

Резюме

Компилятор со средствами дедуктивной верификации подлежит тщательной сертификации для подтверждения высокого уровня доверия к результатам дедуктивной верификации. Разработка компилятора предикатных программ на базе его модели в соответствии с модельно-ориентированной технологией повышает уровень доверия к компилятору. Главной частью модели компилятора является модель внутреннего представления программы, реализуемая в рамках третьего релиза компилятора предикатных программ. В настоящей работе описывается архитектура модели внутреннего представления программы. Важнейшим аспектом модели является анализ типов. В описании модели используется специально разработанный язык спецификации структур данных компилятора. Верификация модели и разработка программы компилятора на базе модели обеспечат высокую надежность компилятора.

Авторы

В. И. Шелехов

Библиография

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_verification.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).

Ключевые слова

дедуктивная верификация, сертификация программ, модельно-ориентированная технология

Скачать полный текст