20 марта: Построение расписаний для строго-периодических систем реального времени

Сергей Зеленов

Зеленов Сергей Вадимович

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

В докладе будут представлены результаты исследований в области построения расписаний для строго-периодических систем реального времени. Соответствующий программный компонент включен в разрабатываемую в ИСП РАН совместно с ГосНИИАС открытую систему поддержки проектирования и верификации комплексов бортового авиационного оборудования MASIW (Modular Avionics System Integrator Workplace).

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

Leave a comment

20 февраля: Интерактивный алгоритм составления тестовых случаев

Федор Строк

Федор Строк

Строк Федор Владимирович — выпускник совместной магистерской программы Высшей Школы Экономики и Яндекса «Анализ Интернет Данных». В данный момент аспирант отделения прикладной математики и информатики НИУ-ВШЭ. Работает старшим инженером по автоматизации тестирования в группе тестирования баннерной системы Яндекса.

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

Сейчас существует два основных подхода к построению тестовых случаев: ручной и автоматический перебор (pairwise, n-wise). Во втором случае сложно восстановить, как именно были получены тестовые случаи. Предлагается интерактивный алгоритм, который позволяет использовать преимущества обоих подходов. Алгоритм основан на математическом аппарате анализа формальных понятий. В докладе будут рассмотрены несколько примеров использования предлагаемого подхода.

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

4 Comments

19 декабря: Верификация параллельных программ в случае слабой консистентности памяти (по-английски)

Roland Meyer

Roland Meyer

Roland Meyer - профессор-ассистент теоретической информатики, руководитель группы теории параллельного программирования (Технический университет Кайзерслаутерн). Он окончил Университет Ольденбурга (Германия) и там же получил степень кандидата наук. Проходил стажировку в LIAFA (Laboratoire d’Informatique Algorithmique: Fondements et Applications), Париж.

Научные интересы: автоматизация верификации программ, формальные языки, моделирование параллельных систем (в основном, это модели с бесконечным числом состояний для реконфигурируемых сетей в случае слабой модели памяти).

Последовательная консистентность (sequential consistency) - одна из наиболее очевидных и простых моделей разделяемой памяти. В этой модели операции атомарны и выполняются в порядке их вызова. Программисты зачастую предполагают, что их программы выполняются именно с последовательной консистентностью, однако для современных вычислительных систем это не так. Аппаратура на основе слабой консистентности (relaxed memory models) зачастую работает более эффективно, т.к. она может применять такие оптимизации как внеочередное выполнение (out-of-program-order) и non-store atomic executions. Однако программы, корректные в случае последовательной консистентности, могут вести себя неправильно в случае слабой консистентности. Последнее время всё больше и больше используется такая аппаратура (например, многоядерные процессоры), что делает проблему написания корректной программы в случае слабой консистентности всё более актуальной.

В этом докладе будет представлен обзор достижений в области верификации параллельных программ в случае слабой консистентности. Главный акцент будет сделан на модель Total Store Ordering, которая была реализована в процессорах семейства x86. Будет рассмотрена проблема достижимости, т.е. проверки того, что во время выполнения заданная программа может прийти в некоторое состояние (памяти). Кроме того, будет рассмотрена проблема определения того, соответствует ли выполнение программы в случае слабой консистентности выполнению в случае последовательной консистентности. Будет показано, что обе проблемы разрешимы, но сложность решения может сильно отличаться для разных классов параллельных программ.

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

2 Comments

21 ноября: Программно-конфигурируемые сети: практические проблемы и задачи.

Александр Шалимов

Александр Шалимов

Шалимов Александр Владиславович — старший программист-разработчик Центра Прикладных Исследований Компьютерных Сетей (ЦПИКС) и младший научный сотрудник МГУ имени М.В. Ломоносова. Окончил факультет ВМК МГУ, кандидат физико-математических наук. В 2010 году прошел стажировку в Microsoft Research (США), где занимался разработкой компилятора для многоядерного процессора нового поколения. С 2011 по 2012 год в качестве приглашенного научного сотрудника работал в Microsoft Research (США), где занимался разработкой системы выполнения программ для процессора нового поколения. В данный момент ведет научные исследования и разработку в области программно-конфигурируемых систем: распределенная сетевая операционная система, высокопроизводительный виртуальный программный коммутатор, виртуализация сетей и сетевых функций.

Область научных интересов — это компьютерные сети, архитектуры вычислительных систем и компиляторы: программно-конфигурируемые сети, многоядерная обработка пакетов, распределенные системы, системы поддержки исполнения программ, компактное представление программ, энергоэффективное выполнение программ.

Программно-конфигурируемые сети (software defined network) — новая концепция управления компьютерными сетями. ПКС — это разделение процессов передачи и управления данными, централизация управления сетью при помощи унифицированных программных средств, виртуализация физических сетевых ресурсов. Технология сравнительно недавно вышла из лабораторных исследований в индустрию, но при этом уже сейчас прогнозируют, что рынок ПКС-решений будет показывать темпы роста не менее 60 % в год и к 2018 г. достигнет объема $35 млрд (с текущих $252 млн). При этом на рынке пока отсутствуют единые стандарты и слишком много информации, которая мешает реально оценить состояние дел. В рамках данного семинара будет рассказано о технологии ПКС и проведена демонстрация работы ПКС-решений для модельной сети.

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

Leave a comment

17 октября: Исследовательские микроядерные операционные системы. Достижения последнего десятилетия, особенности архитектур, вызовы будущего.

Семинар «Технологии разработки и анализа программ» продолжает свою работу в 2013 году.

Василий Сартаков

Василий Сартаков

Сартаков Василий Андреевич - аспирант МИФИ (факультет кибернетики и информационной безопасности), более пяти лет разработок в области встраиваемых и высокопроизводительных систем. Специалист по операционным системам, контрибьютор в нескольких Open Source проектах, с 2011 - развивает RnD подразделение в ksys labs.

Идея микроядерных систем, то есть систем, где большая часть функциональности ядра исключена из привилегированного режима, зародилась в начале 70-х годов. С тех пор было произведено множество попыток реализовать высокопроизводительное микроядро. Известным микроядерным проектом был проект Mach, впоследствии GNU/Mach, разрабатываемый в начале 90-х. Это ядро демонстрировало существенную деградацию производительности в сравнении с монолитно-модульными системами типа Linux. В конце 90ых появилась концепция микроядра L4, представленная в соответствующей спецификации. В соответствии с этой спецификацией, в течение последнего десятилетия разрабатывалось множество проектов таких как L4Ka::Pistachio, L4/Fiasco, SeL4, L4.Verified, L4Re/Fiasco.OC и другие.
Параллельно с развитием проектов архитектуры L4 были реализованы другие микроядерные операционные системы, например Barellfish и Microsoft Singularity. Эти операционные системы не получили такое распространение как L4 (например, компания Qualcomm активно использует L4 в своих платформах), но обладают специфическими особенностями архитектур и реализаций.
Доклад посвящен обзору некоторых исследовательских микроядерных проектов последнего десятилетия, их архитектурам и особенностям применения.

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

Leave a comment

18 апреля: Исследования Microsoft Research в области верификации программных систем

Елена Павлова

Елена Павлова

Елена Анатольевна Павлова - к.т.н., координатор программ, Microsoft

Leave a comment

21 марта: Process mining: извлечение, анализ и совершенствование процессов на основе логов событий.

Ломазова Ирина Александровна

Ломазова Ирина Александровна

В докладе будет рассказано о process mining - направлении исследований, которое находится на стыке между компьютерной обработкой и извлечением данных (data mining), с одной стороны, и моделированием и анализом процессов с другой. Основная идея этого направления состоит в обнаружении, мониторинге и улучшении реальных процессов путем извлечения знания из логов событий, доступных в современных информационных системах.

Докладчик: Ломазова Ирина Александровна - д.ф.-м.н., профессор, НИУ Высшая школа экономики.

Область научных интересов: формальные модели параллельных и распределенных систем, анализ поведенческих свойств, сети Петри, моделирование и анализ бизнес-процессов.

Leave a comment

21 февраля: SEMAT - к теории программной инженерии. Состояние и направления развития.

Позин Борис Аронович

Позин Борис Аронович

Докладчик: Позин Борис Аронович - доктор технических наук, профессор, Председатель SEMAT Russian Chapter, технический директор (CTO) компании ЕС-Лизинг, член правления фонда ФОСТАС.

Leave a comment

17 января: Моделирование и формальная верификация микроархитектуры

Александр Готманов

Александр Готманов

Александр Готманов – научный сотрудник Московского отделения лаборатории САПР (Strategic CAD Labs, Intel Corporation (Москва). В 2005 году закончил факультет ВМК МГУ имени М.В. Ломоносова. Область деятельности - моделирование, анализ и оптимизация микроархитектуры СБИС (в частности, формальная верификация транспортной логики, т.н. коммуникационных фабрик, сетей и систем на кристалле).

В докладе речь пойдет о задаче моделирования микроархитектуры коммуникационных фабрик (транспортной логики, уровня передачи пакетов) в современных системах на кристалле (СнК). Будет рассмотрена среда моделирования и верификации xMAS, разработанная в лаборатории SCL. Используя язык xMAS, можно быстро создавать компактные, графические модели (диаграммы) микроархитектурных блоков и проводить формальную проверку их правильности. Методы верификации моделей xMAS ориентированы на конкретные типы свойств (разные виды свойств safety, свойство отсутствия зависаний). Процесс верификации автоматизирован и, как правило, не требует вмешательства со стороны пользователя. Среда xMAS применялась для анализа микроархитектуры промышленных СнК на ранних этапах проектирования (до появления первой версии спецификации).

Leave a comment

20 декабря: Динамическая проверка HDL-описаний на основе эталонных моделей

Александр Камкин

Александр Камкин

Александр Камкин – к.ф.-м.н., старший научный сотрудник Института системного программирования РАН. Область научных интересов: спецификация и верификация цифровой аппаратуры, статический и динамический анализ HDL-описаний, генерация тестов для микропроцессоров.

Leave a comment