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