Первое всероссийское соревнование по формальной верификации программ VeHa-2023 прошло в рамках конференции PSSV-2023 с 3 и 4 ноября. Команда Механико-математического факультета Новосибирского Государственного университета завоевала третье место. В ее состав вошли магистранты первого года обучения по профилю «Формальные методы анализа программ и систем» Наталья Панченко, Роман Брек и Максим Шарапов. Первое место и второе места заняли команды студентов из Санкт-Петербургского политехнического университета Петра Великого.
В числе организаторов и судей соревнования VeHa-2023 были преподаватели профиля «Формальные методы анализа программ и систем» ММФ НГУ Наталья Гаранина и Дмитрий Кондратьев.
Задачи соревнования в основном были связаны с решением проблем миссии «Луна-25» с помощью формальных методов анализа программного обеспечения. Участники соревнования использовали такие методы как дедуктивная верификация программ и верификация моделей.
«Луна-25» — проект по запуску посадочной автоматической межпланетной станции для исследования верхнего слоя поверхности у южного полюса Луны и лунной экзосферы, а также отработки технологий посадки и анализа лунного грунта. Входил в Федеральную космическую программу России на 2016–2025 годы. 11 августа этого года космический аппарат «Луна-25» был успешно выведен на траекторию перелета к Луне, 19 августа в ходе выполнения операции при переходе на предпосадочную орбиту произошла нештатная ситуация, которая не позволила выполнить маневр с заданными параметрами. По результатам предварительного анализа, вследствие отклонения фактических параметров импульса от расчетных автоматическая станция перешла на нерасчетную орбиту и прекратила свое существование из-за столкновения с поверхностью Луны.
— Перед нами была поставлена задача — представить себя на месте специалистов, которые верифицируют программное обеспечение, загруженное на космическую станцию «Луна-25». Мы должны были промоделировать все системы, которые были описаны как установленные на станции, и с помощью инструментов верификации — программного языка для так называемого model checking — смоделировать ситуацию с предположительной ошибкой в программном обеспечении. Сделать это следовало таким образом, чтобы верификация показала наличие риска падения станции, а потом исправить эту ошибку — показать, как избежать крушения. Мы добились частичного результата — промоделировали систему, но ошибку не исправили. Но уже этого было достаточно, чтобы нам присудили третье место, поскольку задача была очень сложная, но справились мы с ней неплохо, — рассказал Роман Брек.
Мероприятие проходило в смешанном формате: онлайн и офлайн в Иннополисе, по месту проведения конференции PSSV. В нем приняли участие студенты и аспиранты из университетов Санкт-Петербурга, Иннополиса, Новосибирска и Москвы, а также команда сотрудников компании Astra Linux. Команда ММФ НГУ боролась за победу в режиме онлайн.
Программа соревнований включала тьюториалы по методам и средствам формальной верификации. Победители получили денежные призы и дипломы, а участники — сертификаты участия.
Организаторы считают, что первое соревнование прошло успешно и планируют сделать это мероприятие ежегодным.
— Наша команда, носившая незамысловатое название «NSU», участвовала в соревновании дистанционно. Теоретические лекции, проводимые организаторами, были крайне полезны: лекция по model checking позволила мне освежить в памяти полученные в бакалавриате знания, а вот дедуктивную верификацию мне раньше не приходилось применять на практике, поэтому лекция о ней была вдвойне интересна. Требовалось решить по одной задаче на каждую тему, и мы разделили обязанности: Наталья решала задачу на дедуктивную верификацию, а мы с Романом взялись за model checking.
Спортивный интерес и грамотное разделение обязанностей позволили нашей команде занять третье место на соревновании, я очень рад полученному результату.
Было здорово поучаствовать в соревновании на тему верификации программ. Такие соревнования пока не очень распространены, но я надеюсь, что эта сфера получит развитие, и организаторы VeHa-2023 порадуют нас еще многими подобными соревнованиями! — поделился своими впечатлениями о соревновании Максим Шарапов.
