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

Место: Факультет компьютерных наук, Кочновский проезд, д. 3, ауд. 205
Время: 1 июня, 18:30 – 20:00 

Доклады состоятся в рамках научно-исследовательского семинара аспирантской школы по компьютерным наукам.

Первый доклад

Тема: Энергоэффективный метод распознавания деятельности человека в реальном времени с помощью инерциальных датчиков и динамических байесовских сетей
Докладчик:  Роман Черешнев, аспирант второго года обучения, департамент анализа данных и искусственного интеллекта факультета компьютерных наук

Современные методы распознавания человеческой деятельности, основанные на инерциальных датчиках показывают отличные результаты. Но это достигается за счет длительных вычислений процессора и большого потребления энергии. Поэтому эти сложные модели не могут использоваться для прогнозирования в реальном времени или в мобильных системах, например, в мониторинге пожилых людей или в системах долгосрочного мониторинга состояния здоровья. В докладе представляется новый метод, основанный на моделировании плотности распределения данных с использованием динамических байесовских сетей. Наш метод не использует алгоритмы на основе динамического программирования, которые, как известно, медленны.

В наших сравнительных тестах показано, что наш метод работает в два раза быстрее, чем методы искусственных нейронных сетей, и в восемь раз быстрее, чем рекуррентные нейронные сетей и скрытые марковские модели. Точность нашего метода также превосходит точность других методов. 

Второй доклад

Тема: Задача назначения задержек вылетов воздушных судов при регулировании потоков воздушного движения с учетом неопределённости прогноза
Докладчик:  Рамис Габейдулин, аспирант второго года обучения, департамент программной инженерии факультета компьютерных наук

Третий доклад

Тема: Динамическая верификация ядра операционной системы для анализа выполнения высокоуровневых требований защиты информации
Докладчик:  Денис Ефремов, аспирант второго года обучения, базовая кафедра «Системное программирование» Института системного программирования РАН факультета компьютерных наук

Современные операционные системы — это большие и сложные системы. Обоснование корректности поведения данных систем является одной из наиболее важных задач программной инженерии. Актуальность данной темы определяется многообразием компонентов, используемых в операционной системе Linux и реализованных в виде модулей ядра, корректность которых является важнейшей составляющей надежности всей системы, так как модули работают с тем же уровнем привилегий, что и остальное ядро операционной системы Linux.

Тема верификации ядер операционных систем активно развивается последние 20 лет. Существуют успешные попытки верификации отдельных составляющих операционных систем, однако существующие методы в нынешнем виде не всегда подходят для верификации готовых компонентов операционных систем, в том числе модулей ядра операционной системы Linux.

В докладе будет представлен метод, позволяющий производить оценку больших объёмов кода на соответствие формальным моделям, применение которого давало бы возможность повысить общий уровень безопасности, надёжности и устойчивости к ошибкам исследуемых систем; дана картина текущего статуса реализации предложенного метода в ходе работ по верификации модуля безопасности операционной системы GNU/Linux.