Проблематика семинара
Разработка ПО на сегодняшний день — это очень трудоемкий процесс, в котором легко допустить ошибку. Ошибки разработчиков ведут к плачевным последствиям, таким как утечки личной информации пользователей, кражи кибер-валюты, даже к потере человеческих жизней. Поэтому цель моей работы в области синтеза программ — автоматизировать низкоуровневые аспекты разработки ПО, чтобы одновременно повысить продуктивность разработчиков и избавиться от целых классов ошибок.
Более конкретно: мы хотим предоставить разработчику возможность описать глобальные свойства программной системы (например, что она никогда не перешлет данные моей кредитной карты другому пользователю), а потом автоматически сгенерировать код, который позаботится о том, чтобы заданная разработчиком спецификация всегда выполнялась.
Это очень сложная задача, которая подразумевает поиск нужного нам кода среди всех возможных программ на данном языке, то есть в огромном пространстве поиска. Разные группы ученых по всему миру предлагают различные подходы к тому, как выполнять такой поиск эффективно. Моя группа разрабатывает один из таких подходов, основанный на системе типов языка программирования. Об этом и был мой доклад.
О текущей научной работе
Моя группа сейчас работает по нескольким направлениям в области синтеза программ. Одна из проблем, которую мы исследуем: как добиться того, чтобы автоматически генерируемый код не только выполнял нужные функции, но еще и делал это эффективно, с минимальными затратами времени, памяти и энергии. Оказывается, эту задачу тоже можно решить с помощью системы типов (только специальной, такой, которая может описывать потребление ресурсов).
Совсем новое, очень интересное направление: мы сотрудничаем с факультетом лингвистики UCSD, в надежде использовать синтез программ как инструмент, который сможет помочь ученым-фонологам лучше понимать правила произношения слов в разных языках мира, а также определить, как и почему дети способны осваивать эти правила.
Актуальные проблемы научных групп в Университете ИТМО по смежным темам
На моем докладе в альма-матер присутствовали студенты, аспиранты, преподаватели. Некоторые из них занимаются очень близким направлением — синтезом автоматных моделей, поэтому они задавали очень интересные вопросы. Например, один из самых острых вопросов в нашей области на данный момент: если заданную разработчиком спецификацию невозможно реализовать в виде программы, как это быстро определить и как помочь разработчику исправить спецификацию. Этот вопрос прозвучал во время семинара, но на него, к сожалению, никто пока не знает удовлетворительного ответа.
Как изменилась работа Университета ИТМО за 10 лет
Я была в Петербурге в отпуске, и, конечно, не могла упустить возможности посетить альма-матер. По сравнению с 2008-м годом очень приятным сюрпризом для меня стало, что теперь на базе кафедры есть четыре полноценные научные лаборатории под руководством молодых доцентов, в них работают аспиранты на постоянной основе, а не в свободное от работы время, как было в основном 10 лет назад, они публикуются в международных журналах и участвуют в конференциях — прогресс в плане научной работы очевиден.
Перспективы будущего сотрудничества
Меня особенно интересует работа группы Владимира Ульянцева в области синтеза автоматных моделей. Я думаю, эти исследования нам могут очень пригодиться в нашем совместном проекте с лингвистами, так что надеюсь начать сотрудничество с этой группой!
ITMO.NEWS также расспросил Владимира Ульянцева, руководителя международной лаборатории «Компьютерные технологии» об исследованиях в подразделении.
Какие задачи при разработке ПО решает синтез автоматных моделей, для чего он нужен?
Автоматная модель — это просто набор состояний (вершины графа) и переходов между ними по определенным условиям (помеченные ребра графа). Такая модель довольно проста и наглядна, поэтому ее используют при визуализации и построении различных процессов, программных и аппаратных систем. Например, детерминированные конечные автоматы используются при построении компиляторов и в системах распознавания речи. Автомат с лентой памяти называется машиной Тьюринга, и всякий интуитивный алгоритм можно реализовать в виде такой машины. В Университете ИТМО у нас на лекциях об этом прекрасно рассказывает Андрей Сергеевич Станкевич.
Более сложные, управляющие автоматы используются для создания софта контроллеров: можно "нарисовать" логику управления системы и автоматизировано преобразовать в код. Такой подход называется автоматным программированием, предложенным Анатолием Абрамовичем Шалыто, профессором Университета ИТМО.
Синтез (или построение, вывод) автоматных моделей — это процесс их автоматизированного создания по некоторой известной, заданной пользователем, информации. То есть, вместо того, чтобы "рисовать" автомат вручную, силами инженера, алгоритм создает его из спецификации. К примеру, задача синтеза конечного автомата формулируется так: пусть у нас есть примеры правильного и неправильного поведения автомата; необходимо найти минимальный автомат, который соответствует правильным примерам и не соответствует неправильным. Задачами в области синтеза исследователи занимаются уже больше 50 лет. С 2010 года занимается ими в том числе наша группа.
Каких результатов вы хотите достичь?
Одна из наших постоянных задач — усовершенствование существующих и разработка новых подходов к синтезу конечных автоматов. Так, в работе Finding all minimum-size DFA consistent with given examples: SAT-based approach (Zakirzyanov I., Shalyto A., Ulyantsev V.) был усовершенствован лучший на сегодняшний день алгоритм точного построения конечных автоматов. Аспирант Илья Закирзянов сейчас занимается вопросами применения алгоритмов для построения моделей существующих программ, а недавно выиграл под этот проект грант РФФИ "Мой первый грант" (18-37-00425).
Синтез автоматных моделей как контроллеров, так и самих систем, актуален при создании надежного и проверенного программного обеспечения. В тесной коллаборации с Университетом Аалто, где работает соруководитель нашей лаборатории Валерий Вяткин, мы разрабатываем методы тестирования, верификации и синтеза киберфизических систем. Такие методы используются при создании и проверке контроллеров, работающих, к примеру, на ядерных станциях и гражданских судоходных системах. Проще говоря, мы ищем ответ на вопрос "что еще в наших силах сделать, чтобы не нести потери от ошибок контроллеров?" Наше международное взаимодействие нашло поддержку Министерства образования и науки в рамках федеральной целевой программы (проект RFMEFI58716X0032).
Прочитать большое интервью с Надеждой Поликарповой о ее академической карьере и научных интересах можно тут.
