Формальные методы анализа программ и систем

Формальные методы — это комплекс тесно взаимосвязанных друг с другом разделов математики и информатики, нацеленных на разработку математических методов описания, анализа и преобразования программ и систем в целом, которые ориентированы на повышение их надежности и ресурсных характеристик. Важнейшим отличием исследований по формальным методам от чисто теоретических изысканий является их нацеленность на практическое применение: результатом математических исследований является программная реализация и внедрение в практику ИТ-индустрии.

Целью данного профиля является устойчивое воспроизводство специалистов в области формальных методов, способных вести такого рода исследования, а также уверенно применять их и способствовать их широкому внедрению на практике. Основными направлениями формальных методов, рассматриваемых в данном профиле, являются:

• Спецификация, формализация требований, онтологическое моделирование программного обеспечения и систем, что ускоряет этап их проектирования и снижает риски неопределенности и недопонимания между заказчиками и исполнителями, а также приоткрывает путь к автоматическому и/или автоматизированному доказуемо корректному синтезу программ и систем.
• Формальная семантика программ, а также методы ее аппроксимации, которые являются базой статического семантического анализа программ, результаты которого используются для их оптимизации, поиска ошибок, верификации свойств и т.д. В частности, наблюдается разрыв между прогрессом в архитектурах вычислительных систем и способностью трансляторов производить код (например, для параллельных вычислений), в полной мере использующий все возможности для высокопроизводительных вычислений. Причина этого – сложные семантические проблемы, которые приходится решать при программировании такого рода систем.
• Верификация программ и систем, т.е. доказательное подтверждение соответствия полученной реализации исходной спецификации. Это свойство ожидаемо для любого программного обеспечения, однако оно оказывается критически важным для управляющих систем реального времени, высоконадежных и устойчивых к отказам систем, разнообразных систем, связанных с обеспечением безопасности. Для решения этих задач используются сложные логические и комбинаторные методы, ведущие при реализации к нетривиальной алгоритмике.

Следует отметить, что вопросы эффективности и надежности программ и систем актуальны в целом в современном обществе: учебные заведения, академические институты, государственные агентства из сферы высоких технологий, исследовательские подразделения лидеров ИТ-индустрии демонстрируют неуклонный рост интереса к формальным методам в программной и системной инженерии. Методы компьютерного доказательства начинают внедряться в различных областях математики.

Формальные методы уже внедряются в технологические цепочки производства программного обеспечения. Так, например, современные версии Microsoft Visual Studio предлагают средства семантического анализа программ, которые позволяют статически отыскивать некоторые виды ошибок и непрагматичные конструкции. В распространенной среде разработки Eclipse для дедуктивной верификации Java-программ применяется плагин KeYClipse, предоставляющий в данной среде разработки возможность использовать технологии формальной верификации из проекта KeY. В другой известной среде разработки IntelliJ IDEA применяется плагин OpenJML/ESC, который позволяет дедуктивно верифицировать Java-программы в этой среде с помощью возможностей системы OpenJML. Также следует отметить программные средства CertiKOS для разработки формально верифицированных операционных систем. На основе CertiKOS создано надежное программное обеспечение для беспилотных авиационных систем. Имеется набор утилит Verified Software Toolchain для дедуктивной верификации (с помощью утилиты VST-Floyd) и корректной компиляции программ на языке C. Для корректной компиляции в проектах CertiKOS и Verified Software Toolchain используется верифицированный компилятор CompCert для языка C. Компилятор CompCert все чаще применяется для разработки надежного программного обеспечения на языке C. Во многом именно применение компилятора CompCert обеспечило успех проектов CertiKOS и Verified Software Toolchain. Кроме того, в качестве примера верифицированного компилятора можно привести комплекс программных средств CakeML для языка Standard ML. Проект CakeML предоставляет не только верифицированный компилятор, но и утилиту CFML для формальной верификации компилируемых программ.

Такие компании как Intel, IBM, Nvidia, Qualcomm, Broadcomm, NXP, Siemens, Bosch и многие другие регулярно имеют открытые вакансии инженеров по формальным методам верификации.

Более того, из разряда рекомендаций применение формальных методов постепенно переходит в разряд обязательных требований при сертификации систем повышенной надежности. Для прохождения некоторых видов сертификации программного обеспечения использование формальных моделей уже стало обязательным (например, для проверки соответствия ПО встроенных систем управления ГОСТам РФ по надежности). Таким образом, потребность в специалистах, способных осознанно применять формальные методы при разработке программ, будет только расти со временем.

На протяжении последних 20 лет каждый год в бакалавриате и магистратуре ММФ и ФИТ НГУ регулярно защищаются бакалаврские и магистерские ВКР, которые посвящены различным аспектам формальных методов. Выпускники становились сотрудниками компаний Excelsior, Intel, JetBrains, Huawei, Microsoft, Meta и др.

Помимо ознакомления с фундаментальными аспектами анализа программ, студенты в рамках курсов этого профиля получают практические навыки обращения с программными инструментами, используемыми в этой области. На практических занятиях будут использоваться следующие инструменты: верификатор моделей SPIN, символьный верификатор моделей nuSMV, вероятностный верификатор моделей PRISM, SAT-решатель Glucose, SMT-решатели Z3 и CVC5, система интерактивного доказательства Isabelle/HOL, генератор парсеров ANTLR, а также авторский инструмент для разработки генераторов условий корректности программ.