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

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

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

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