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