ОТЗЫВ НАУЧНОГО РУКОВОДИТЕЛЯ
на диссертационную работу Кривчикова Максима Александровича «Формальные модели и верификация свойств программ с использованием промежуточного представления», представленную к защите на соискание учёной степени кандидата физико-математических наук по специальности 05.13.17 — теоретические основы информатики
Диссертационная работа посвящена исследованию процессов разработки формальных моделей программ и языков программирования, которые используются при написании исходных текстов программ. Актуальность работы определяется сложностью реализации процессов формальной верификации крупных, наукоемких программных комплексов, которая востребована на всех этапах их жизненного цикла. Особую значимость верификация представляет для программных средств, использующихся при сопровождении объектов критически важных инфраструктур. Ошибки в таких комплексах могут стать причиной значительного материального ущерба, способны приводить к последствиям катастрофического характера, сопряжённым с угрозой здоровью и жизни людей. Методы формальной верификации позволяют получать строгое математическое доказательство выполнения программой предъявляемых к ней требований. Для эффективного проведения формальной верификации, как правило, необходимо иметь модель программы, адекватно описывающую её семантику. Получение такой модели осложняется еще и тем фактом, что при написании программ, как правило, используется несколько языков программирования. Разработка математических моделей и основанных на них программных средств для преодоления отмеченных сложностей является целью диссертационного исследования. Тема диссертации соответствует положениям пп. 2, 5, 14 областей исследования согласно Паспорту специальности 05.13.17 «Теоретические основы информатики».
В первой главе диссертации автор рассматривает предысторию и современное состояние исследований в области методов описания формальных моделей программ. Критический анализ перечисленных в первом и втором разделах главы многочисленных литературных источников позволил обосновать выбор лямбда-исчисления с зависимыми типами в качестве базовой формальной модели. Анализ показал, что использование такой формальной модели для промежуточного представления семантики программ, написанных с использованием нескольких языков программирования, с целью их формальной верификации, ранее не рассматривалось.
По итогам представленного обзора, в третьем разделе автор формулирует основные задачи исследования. В их число входят как задачи теоретического характера, а именно — выбор используемой разновидности исчисления, так и практического, такие как реализация промежуточного исполнения и описание семантики существующих языков программирования в терминах промежуточного исполнения.
Вторая глава содержит описание лямбда-исчисления с зависимыми типами, в том числе — новую его разновидность, предложенную автором. Первый раздел главы посвящён описанию лямбда-исчисления с зависимыми типами в разновидности Расширенного Исчисления Конструкций. Этот раздел может рассматриваться как вводный. Во втором разделе автор вводит понятия типов идентичности, которые достаточно часто рассматриваются в рамках лямбда-исчисления с зависимыми типами и его логических интерпретаций как аналоги утверждений о равенстве (идентичности) объектов. Современная расширенная интерпретация таких типов в рамках гомотопической теории типов позволяет использовать типы идентичности для более широкого класса спецификаций и утверждений. Однако на настоящее время не было получено вычислительной интепретации гомотопической теории типов, что затрудняет её практическое применение. Автор предлагает подход к решению такой задачи с помощью введения в исчисление дополнительных правил редукции. Для вновь вводимых правил доказываются свойства, обеспечивающие сохранение типов термов при применении правил. Кроме того, доказано, что для известных типов термы удаления типов идентичности являются редексами, т. е. к таким термам могут применяться правила редукции.
Третья глава посвящена реализации макета языка программирования и формальной спецификации, а также программного средства, которое предназначено для проверки типов выражений такого языка. Язык основан на предложенной автором разновидности лямбда-исчисления с зависимыми типами. Для практического использования автор расширяет разновидность исчисления известными типами, используемыми для описания данных. Такие типы включают конечные типы (аналоги конечных множеств), тип натуральных чисел, индуктивные и коиндуктивные типы. Набор основных термов языка составляет промежуточное представление для описания семантики языков программирования, разработка которого является одной из основных задач диссертационного исследования.
Четвёртая и пятая главы представляют результаты применения разработанного автором макета языка программирования и программного средства к задачам описания формальных моделей программ. В четвёртой главе приводится построенная автором с использованием макета языка и программного средства модель статической формальной семантики языка промежуточного представления стандарта ECMA-335. Для демонстрации практической применимости такой модели предлагается динамическая семантика подмножества языка, для разработки которой автор адаптирует подход на основе монад к макету базового языка. Предложенная формальная семантика используется для исследования минимального фрагмента кода, входящего в состав используемого на практике программного комплекса моделирования теплогидравлических процессов в энергетических реакторах атомных электростанций. Пятая глава содержит модель динамического параллельного исполнения программ, для описания которой также используется макет базового языка. Для модели доказываются свойства, позволяющие утверждать, что процесс параллельного исполнения корректен при выполнении ряда свойств. Такие свойства могут быть получены статически, что демонстрируется с использование фрагмента кода, который использовался в четвёртой главе.
В Заключении сформулированы основные результаты и выводы по итогам исследования, а также отмечены перспективные направления дальнейших исследований.
Новизна исследований и результатов диссертации заключается: в новой разновидности лямбда-исчисления с зависимыми типами, поддерживающей нетривиальные типы идентичности с помощью предложенных автором правил редукции; в реализации макетов языка и программного средства для проверки типов выражений такого языка на основе такой разновидности исчисления; в описании новых формальных моделей существующих языков программирования, методов параллельного исполнения программ и семантики программ.
Содержание диссертации свидетельствует о том, что представленные в ней результаты являются новыми и вносят весомый вклад в решение задачи описания формальных моделей программ и используемых при их разработке языков программирования с целью их дальнейшей формальной верификации.
Достоверность и обоснованность полученных результатов подтверждается:
— чёткостью формулировок цели диссертации и постановок общей и частных задач исследования;
— наличием математических моделей и математической строгостью доказательств заявленных автором свойств;
— результатами обсуждения основных положений диссертации на научных и научно-практических конференциях и семинарах, а также публикациями в рецензируемых научных изданиях, в том числе — в изданиях, индексируемых Web of Science и Scopus.
С 2009 года по настоящее время является сотрудником НИИ механики МГУ (по совместительству). С 2014 года он занимает должность научного сотрудника лаборатории автоматизации экспериментальных исследований на полную ставку. В 2013-14 учебном году, будучи аспирантом, он получал стипендию Президента Российской Федерации для аспирантов по приоритетным направлениям модернизации и технологического развития российской экономики. принимал участие в выполнении научно-исследовательских работ НИИ механики МГУ, заказчиками которых являлись ОАО «ВНИИАЭС» (разработка полномасштабной вычислительной модели «Виртуальная АЭС»), а также ФАУ «ГНИИ ПТЗИ ФСТЭК России» (исследование технических средств защиты информации в распределенных критически важных системах информационной инфраструктуры). Кроме того, он участвует в научно-исследовательской работе по развитию и сопровождению системы подготовки принятия решений на основе анализа информации о результатах научной, педагогической, инновационной деятельности ИАС «Наука МГУ» («ИСТИНА»).
С позиций педагогической деятельности, активно участвует в работе научного семинара «Проблемы современных информационно-вычислительных систем», ведёт занятия практикума на ЭВМ у студентов третьего курса механико-математического факультета МГУ. принимал участие в руководстве курсовыми и дипломными работами студентов механико-математического факультета. В целом, Кривчикова Максима Александровича можно охарактеризовать как квалифицированного научного работника, способного самостоятельно ставить и решать сложные исследовательские задачи.
С учётом изложенного выше, считаю, что работа соответствует всем требованиям, предъявляемым к диссертациям на соискание учёной степени кандидата физико-математических наук по специальности 05.13.17 «Теоретические основы информатики», а её автор заслуживает присуждения ему учёной степени кандидата физико-математических наук по этой специальности.
Научный руководитель
доктор физико-математических наук, профессор
