Certified compiler design of predicate programs
Abstract
A compiler with deductive verification facilities should be thoroughly certified to obtain high level of assurance. The development of the compiler for a predicate program using a compiler model in accordance with a model-based design method makes the compiler to be of a higher level of assurance. The main part of a compiler model is the model of inner program representation for a predicate program. The model is designed in the framework of third release of the compiler. The model architecture for inner representation of predicate program is described. Type checking is specially analyzed as an important aspect in the compiler development. The verification of the model and compiler development on the base of the model should guarantee a high level of compiler reliability.
About the Author
V. Shelekhov
Институт систем информатики имени А. П. Ершова СО РАН; НГУ
Russian Federation
Russian Federation
References
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).
Review
For citations:
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.)
Views:
406
Email this article 
