27 апреля: Тестирование отказоустойчивости распределенной торговой системы методом эмуляции отказов

Жердер Вадим Меерович

Жердер Вадим Меерович

Костанбаев Сергей Витальевич — кандидат технических наук, главный специалист отдела разработки и сопровождения торгово-клиринговых систем Московской Биржи. Жердер Вадим Меерович — начальник отдела автоматизации тестирования, ПАО Московская биржа.

Костанбаев Сергей Витальевич

Костанбаев Сергей Витальевич

Биржевые торговые системы — высоконагруженные системы, работающие в реальном времени, которые должны удовлетворять высоким требованиям по скорости обработки сообщений и надежности. В докладе описывается архитектура распределенной торговой системы на примере одной из систем Московской биржи и протокол синхронизации состояний узлов (distributed consensus protocol), обеспечивающий ее работу. Специфика требований к торговой системе привела к необходимости разработать новый оригинальный протокол; широко известные протоколы, такие как Raft, оказались неприменимыми. Также будет представлена автоматизированная система тестирования распределенной торговой системы методом эмуляции отказов.

Доклад состоится 27 апреля 2017 года в 17:00 в Институте системного программирования РАН. Институт располагается в здании по адресу: улица Александра Солженицына, дом 25. Аудитория 110.

Leave a comment

16 марта: Доказательство свойств функциональных программ методом насыщения равенствами

Сергей Гречаник

Сергей Гречаник

Гречаник Сергей Александрович — сотрудник Института прикладной математики РАН имени М.В. Келдыша. В 2011 году окончил факультет вычислительной математики и кибернетики МГУ имени М.В. Ломоносова.

В докладе рассматривается метод преобразования программ на нестрогом функциональном языке первого порядка, основанный на комбинации методов насыщения равенствами и суперкомпиляции. Общая идея метода совпадает с идеей насыщения равенствами (предложенного в работе «Equality Saturation: A New Approach to Optimization» Тейта и др. для преобразования императивных программ) и заключается в преобразовании структуры данных, описывающей целое множество программ, а не одну программу. Используемые преобразования, однако, в основном взяты из суперкомпиляции. В рамках метода также предложено преобразование, названное слиянием по бисимуляции, соответствующее доказательству эквивалентности функций по индукции или коиндукции. Показано, что метод применим для индуктивного доказательства эквивалентности программ. Изложение основных идей метода можно найти в препринте «Полипрограммы как представление множеств функциональных программ и преобразования над ними».

Доклад состоится 16 марта 2017 года в 17:00 в Институте системного программирования РАН. Институт располагается в здании по адресу: улица Александра Солженицына, дом 25. Аудитория 110.

Leave a comment

16 февраля: Методы и средства верификации протоколов когерентности памяти

Буренков Владимир Сергеевич

Буренков Владимир Сергеевич

Буренков Владимир Сергеевич — научный сотрудник АО «МЦСТ». В 2012 году окончил факультет «Информатика и системы управления» МГТУ имени Н.Э. Баумана (магистр техники и технологий по направлению «Информатика и вычислительная техника»).

В докладе будет рассмотрена проблема верификации протоколов когерентности памяти масштабируемых промышленно разрабатываемых микропроцессорных систем. Представлен новый метод параметризованной верификации протоколов когерентности памяти, основанный на преобразованиях моделей протоколов когерентности памяти, написанных на языке Promela. Предложена методика верификации протоколов когерентности памяти, представляющая весь процесс верификации, который начинается написанием исходных формальных моделей протоколов когерентности и заканчивается проведением параметризованной верификации протоколов когерентности. Описана разработанная система верификации протоколов когерентности памяти и рассказано об опыте ее использования для верификации протокола когерентности памяти 16-ядерной системы из микропроцессоров «Эльбрус-4С».

Доклад состоится 16 февраля 2017 года в 17:00 в Институте системного программирования РАН. Институт располагается в здании по адресу: улица Александра Солженицына, дом 25. Аудитория 110.

Leave a comment

19 января: Кибербезопасность и бортовые операционные системы

Абрамов Александр Владимирович

Абрамов Александр Владимирович

Абрамов Александр Владимирович — генеральный директор ООО «НТЦ «АМДЭФ». Закончил факультет микроприборов и технической кибернетики МГИЭТ (ТУ). Работал над проектами ГУП НПЦ «Спурт» и НТЦ «АМДЭФ» по созданию аппаратуры помехоустойчивого кодирования сигналов спутниковой связи. Разработчик операционных систем реального времени «Пилот» и «Куб» для встраиваемых систем подвижной радиосвязи.

Фисун Илья Юрьевич

Фисун Илья Юрьевич

Фисун Илья Юрьевич — разработчик в МГТУ имени Н.Э. Баумана. Закончил Московскую финансово-промышленную Академию.

В ходе доклада будет рассмотрен вопрос влияния стандартов и специфики авиационной отрасли на архитектуру операционной системы комплекса бортового оборудования летательного аппарата. Кроме того, будут представлены текущие результаты работы НТЦ «АМДЭФ» над проектом по созданию подсистемы безопасности операционной системы реального времени для гражданской авиации.

Доклад состоится 19 января 2017 года в 17:00 в Институте системного программирования РАН. Институт располагается в здании по адресу: улица Александра Солженицына, дом 25. Аудитория 110.

Leave a comment

17 ноября: Проект Ангара: вычислительные эксперименты на языке программирования F#

Сергей Березин

Сергей Березин

Сергей Березин — к.ф.-м.н., доцент на ВМК МГУ, руководит лабораторией «Информационных технологий в научных исследованиях». Читает авторские курсы лекций «Компьютерная графика» и «Объектно-ориентированное программирование на платформе .NET». В область профессиональных интересов входят научная визуализация, средства хранения и анализа данных, программные средства для проведения сложных вычислительных экспериментов.

Дмитрий Войцеховский

Дмитрий Войцеховский

Дмитрий Войцеховский — закончил ВМК МГУ, прошел стажировку в группе Вычислительных наук Microsoft Research Cambridge, RSDE в лаборатории «Информационных технологий в научных исследованиях». Область профессиональных интересов — современные языки программирования, распределенные и облачные технологии, методы машинного обучения.

Доклад посвящен программному обеспечению для удобного описания и эффективного выполнения вычислительных экспериментов. В докладе будет описан набор компонентов на языке F# под кодовым названием Ангара. Проект Ангара отражает результаты долгосрочного сотрудничества с группой Computational Sciences в Microsoft Research Cambridge. Проект Ангара помогает исследователям строить воспроизводимые вычислительные эксперименты, которые могут выполняться несколько раз с нуля, с одинаковыми результатами. Полная информация о происхождении доступна для каждого результата вычислительного эксперимента, что позволяет точно отследить ход вычислений. Ангара ориентирована на эффективное инкрементальное конструирование вычислительного эксперимента. Новые этапы вычислений могут быть добавлены или изменены с повторным вычислением только результатов, затронутых изменениями. Зачастую это экономит значительное количество времени, так как многие вычислительные эксперименты могут выполняться длительное время и требовать значительных вычислительных ресурсов. Исследователь может наблюдать за промежуточными результатами эксперимента по мере их готовности, тем самым имея возможность оценить ход эксперимента на ранних итерациях, не дожидаясь окончания всего эксперимента.

Проект Ангара доступен на Github.

Доклад состоится 17 ноября в 17:00 в ИСП РАН.

Семинар проходит в Институте системного программирования РАН. Институт располагается в здании по адресу: улица Александра Солженицына, дом 25. Аудитория 110.

Leave a comment

20 октября: Инструментальная поддержка процесса верификации, определенного в документах DO-178B/C

Козырев Владимир Петрович

Козырев Владимир Петрович

Козырев Владимир Петрович — кандидат технических наук, доцент кафедры кибернетики НИЯУ МИФИ, эксперт компании «ДС БАРС».

В докладе рассматривается процесс верификации программ, разрабатываемых в соответствии с требованиями стандартов DO-178B/C, обязательные мероприятия (activities), проводимые в рамках этого процесса, и инструменты, используемые при их проведении. Представляются результаты, полученные в ходе разработки таких инструментов, проводимой в компании «ДС БАРС».

Доклад состоится 20 октября в 17:00 в ИСП РАН.

Наш семинар перемещается в уютное здание Института системного программирования РАН. Он начнется не в 18:00, а в 17:00. Институт располагается в здании по адресу: улица Александра Солженицына, дом 25. Аудитория 110.

2 Comments

15 сентября: Динамическая композиция программных компонентов

Гринкруг Ефим Михайлович — кандидат технических наук, профессор департамента программной инженерии факультета компьютерных наук НИУ ВШЭ. В прошлом — разрабочик ОС М-10 (НИИ Вычислительных комплексов имени М.А. Карцева, эксперт компании Параграф (www.parallelgraphics.com), начальник отдела LuxoftLabs и CТО компании Meshnetics.

Гринкруг Ефим Михайлович

Гринкруг Ефим Михайлович

Обсуждается компонентная модель, позволяющая в динамике (без компиляции) создавать и использовать новые составные компоненты. Базовыми компонентами служат специальные компоненты JavaBeans, предназначенные для использование в предлагаемой компонентной модели. Определяются базовые и составные типы компонентов, их реализации, представления и функциональность их инстансов. Обсуждается программная архитектура и компонентная реализация среды для поддержки динамической композиции компонентов и их функционирования. Приводятся примеры и направления практического использования в различных приложениях.

Доклад состоится 15 сентября в 17:00 в ИСП РАН.

Наш семинар перемещается в уютное здание Института системного программирования РАН. В этот раз он начнется не в 18:00, а в 17:00. Институт располагается в здании по адресу: улица Александра Солженицына, дом 25. Аудитория 110. В этот раз прямой трансляции и записи семинара не будет — ждем всех вас лично на семинаре!

Leave a comment

21 апреля: Методы деанонимизации пользователей сети Tor

Сергей Авдошин

Сергей Авдошин

Авдошин Сергей Михайлович — руководитель Департамента программной инженерии НИУ Высшая школа экономики, кандидат технических наук, профессор НИУ ВШЭ.

Александр Лазаренко

Александр Лазаренко

Лазаренко Александр Вячеславович — студент 2 курса бакалавриата образовательной программы «Программная инженерия» НИУ Высшая школа экономики.

На сегодняшний день одним из инструментов для обеспечения приватности пользователей в глобальной сети является сеть Tor. Это полностью децентрализованная, оверлейная анонимная сеть, состоящая из волонтерских серверов. Все эти свойства обеспечивают высокий уровень анонимности пользователей, что позволяет успешно скрывать свои следы в интернете. Однако, среди пользователей Tor попадаются и преступники: наркоторговцы, воры и прочие нарушители порядка. Для того, чтобы предотвращать незаконную деятельность, необходимо деанонимизировать этих пользователей. О методах деанонимизации и пойдет речь в данном докладе.

Послушать доклад можно будет 21 апреля в 18:00 на факультете ВМК МГУ.

Внимание! Важная информация по поводу прохода в МГУ! В связи с усилением пропускной системы, если вы хотите приехать на доклад в МГУ, просим до 12:00 понедельника, 18 апреля, прислать нам на почту sdat@ispras.ru (даже если вы уже были у нас на семинаре до марта этого года) свои ФИО, где и кем работаете, кратко свои достижения (например, ученая степень, звание, если есть). Не забудьте взять с собой паспорт на семинар.

Вы можете присылать свои вопросы как до доклада, так и во время него, по электронной почте sdat@ispras.ru или в твиттер для @sdat_seminar.

Leave a comment

24 марта: Геоинформационное ПО: технологии и проблемы

Дмитрий Барышников

Дмитрий Барышников

Барышников Дмитрий — разработчик NextGIS, коммитер GDAL, член сообщества ГИС-Лаб.

Геоинформационное программное обеспечение (ГИС) решает задачи, связанные со сбором, обработкой и представлением геоданных - особого вида данных, обязательно имеющих пространственную компоненту (географические или иные координаты). Речь пойдет о том, что такое ГИС, как устроено ПО ГИС, какие есть форматы геоданных, протоколы, особенности и способы визуализации, алгоритмы обработки, а также современные тенденции в области ГИС.

Послушать доклад можно будет 24 марта в 18:00 на факультете ВМК МГУ. Выступит представитель «GIS-Lab — неформального сообщества специалистов в области ГИС и ДЗЗ, развивающих себя и помогающих осваивать пространственные технологии тем, кому необходима помощь». Сайт gis-lab.info.

Внимание! Важная информация по поводу прохода в МГУ! В связи с усилением пропускной системы, если вы хотите приехать на доклад в МГУ, просим до 12:00 понедельника, 21 марта, прислать нам на почту sdat@ispras.ru (даже если вы уже были у нас на семинаре) свои ФИО, где и кем работаете, кратко свои достижения (например, ученая степень, звание, если есть). Не забудьте взять с собой паспорт.

Вы можете присылать свои вопросы как до доклада, так и во время него, по электронной почте sdat@ispras.ru или в твиттер для @sdat_seminar.

Leave a comment

18 февраля: Технология разработки пакетов поддержки модулей для ОС РВ Багет

Юрий Михайлович Лазутин

Лазутин Юрий Михайлович — доктор ф.-м. наук (05.13.11), заведующий отделом базового программного обеспечения в отделении разработки вычислительных систем ФГУ ФНЦ НИИСИ РАН.

Одной из разработок НИИСИ РАН являются операционные системы реального времени, в частности, ОС РВ Багет 2.* и ОС РВ Багет 3.*. С целью упрощения ее перенесения для новой целевой архитектуры или при изменении существующей архитектуры часть операционной системы, зависящая от аппаратуры, четко выделена. Эта часть, называемая пакетом поддержки модуля (ППМ), поставляется вместе с исходными текстами операционной системы. Её адаптация к аппаратуре (например, добавление или изменение драйверов устройств) производится путем внесения изменений в исходные тексты ППМ. При этом нет необходимости вносить изменения в другие части системы. На семинаре будет рассказано о сложившейся за 20 лет технологии разработки ППМ (более 10-ти различных модулей и около 10 «систем на кристалле», в основном - MIPS1 и «MIPS64», но поддерживается и i386).

Послушать доклад можно будет 18 февраля в 18:00 на факультете ВМК МГУ.

Вы можете присылать свои вопросы как до доклада, так и во время него, по электронной почте sdat@ispras.ru или в твиттер для @sdat_seminar. Но лучше всего прийти к нам на семинар лично в МГУ. На входе в МГУ действует пропускная система, поэтому для оформления пропуска заранее пришлите, пожалуйста, свою фамилию, имя и отчество на sdat@ispras.ru (не забудьте взять с собой паспорт).

Leave a comment