ru-STEP по-русски

 

Российский онлайн-семинар
по фундаментальным вопросам программной инженерии,
теории и экспериментальному программированию:
ru-STEP = russian seminar on Software Engineering, Theory and Experimental Programming.

(Тестовая версия страницы семинара. При необходимости Вы можете перейти на страницу семинара на английском языке.)

Учредители семинара:

  • Игорь Сергеевич Ануреев (Институт систем информатики СО РАН - Новосибирск, anureev "на" iis.nsk.su)
  • Дмитрий Александрович Кондратьев (Институт систем информатики СО РАН - Новосибирск, apple-66 "на" mail.ru)
  • Александр Владимирович Наумчев (Университет Иннополис - Иннополис, a.naumchev "на" innopolis.ru)
  • Денис Константинович Пономарев (Институт систем информатики СО РАН и Новосибирский Государственный Университет - Новосибирск, ponom "на" iis.nsk.su)
  • Алексей Владимирович Промский (Институт систем информатики СО РАН - Новосибирск, promsky "на" iis.nsk.su)
  • Андрей Александрович Садовых (Университет Иннополис - Иннополис, a.sadovykh "на" innopolis.ru)
  • Николай Вячеславович Шилов (Университет Иннополис - Иннополис, shiloviis "на" mail.ru)

Общие сведения о семинаре:

Как зарегистрироваться для участия в семинаре, в обсуждениях и/или как подать заявку на выступление:

  • Желающие выступить на семинаре приглашаются написать по электронной почте любому/нескольким/всем из учредителей семинара (с темой письма "Заявка на ru-STEP").
  • Желающие получать напоминание (оповещение) о ближайшем заседании накануне семинара (тему, докладчика, техническую среду проведения, дату и время) могут заполнить Google-форму https://forms.gle/earZy3hFJKmHQLoZ7.
  • Для обсуждения работы семинара, состоявшихся докладов и других связанных с семинаром тем создана (Google-)группа.

Предстоящие заседания семинара:

Joseph Alexander Brown (Начальник Лаборатории искусственного интеллекта в разработке игр, Университет Иннополис): Affordance Theory in Game Design - A Guide Toward Understanding Players Монография Affordance Theory in Game Design. A Guide Toward Understanding Players подготовлена профессором Joseph Alexander Brown совместно с аспирантом Университета Иннополис Hamna Aslam и была опубликована 2020 издательством Morgan & Claypool Publishers.
Abstract: Games, whether educational or recreational, are meant to be fun. How do we ensure that the game delivers its intent?
The answer to this question is playtesting. However, a haphazard playtest process cannot discover play experience from various dimensions. Players' perceptions, affordances, age, gender, culture, and many more human factors influence play experience. A playtest requires an intensive experimental process and scientific protocols to ensure that the outcomes seen are reliable for the designer.
Playtesting and players' affordances are the focus of this book. This book is not just about the playtest procedures but also demonstrates how they lead to the conclusions obtained when considering data sets. The playtest process or playtest stories differ according to the hypothesis under investigation. We cover examples of playtesting to identify the impact of human factors, such as age and gender, to examine a player's preferences for game objects' design and colors. The book details topics to reflect on possible emotional outcomes of the player at the early stages of game design as well as the methodology for presenting questions to players in such a way as to elicit authentic feedback.
This book is intended mainly for game designers, researchers, and developers. However, it provides a general understanding of affordances and human factors that can be informative for readers working in any domain.
Познакомиться с оглавлением монографии и краткими биографиями авторов можно по указанным ссылкам.
Дата и время: пятница 25 июня, 2021 (12:00-13:40 в Москве и 16:00-17:40 в Новосибирске) Семинар пройдет на платформе Zoom (via this link).

Прошедшие заседания семинара: (в порядке Last-In - First-Out):

Александр Владимирович Коновалов (Московский государственный технический университет): Введение в язык Рефал Аннотация: В докладе рассказано о языке программирования Рефал — история, синтаксис, семантика и основы метавычислений над ним. Показаны основные отличия Рефала (самого языка и метавычислений над ним) от других функциональных языков (в докладе Рефал сравнивался с Хаскелем и Эрлангом). Цель — предварить (предполагаемые в июле-августе) доклады про особенности суперкомпиляции Рефала (а участники семинара с предметной областью не знакомы). Дата: пятница 11 июня 2021. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.)
Заметки к докладу, подготовленные Андреем Валентиновичем Климовым. - Продолжить обсуждение можно присоединившись к дискуссионной (Google-) группе нашего семинара.
Пленарные доклады XI SYRCoSE: SYRCoSE (Spring/Summer Young Researchers' Colloquium on Software Engineering) организуется ежегодно начиная с 2007 широко известными специалистами в программной инженерии и программировании Александром Константиновичем Петренко (Институт системного программирования РАН, Москва) и Андреем Николаевичем Тереховым (Санкт-Петербургский Государственный Университет).
В 2021 г. местом проведения коллоквиума стал Национальный исследовательский университет Высшая школа экономики. Коллоквиум состоялся 27-28 мая и прошел в смешанном формате в комплексе ВШЭ на Покровском бульваре и дистанционно в Zoom.
С аннотациями пленарных докладов можно познакомиться по данной ссылке.
Даты выступлений пленарных докладчиков:
  • Д.А. Мордвинов - четверг 27 мая,
  • А.В. Подкопаев - пятница 28 мая,
  • Holger Schlingloff - пятница 28 мая.
Записи всех выступлений на SYRCoSE-2021 предоставлены Институтом системного программирования им. В.П. Иванникова РАН и доступны в следующих репозиториях:
Артем Сергеевич Бурмяков (Университет Иннополис): Введение в проблему консенсуса и ее применение для разработки неблокирующих параллельных алгоритмов Аннотация: Проблема консенсуса - это фундаментальная теоретическая проблема для распределенного и параллельного программирования. Проблема имеет огромное влияние на различные области приложений, такие как разработка неблокирующих параллельных алгоритмов, систем блокчейнов, алгоритмов синхронизации времени в распределенных системах и параллельных систем с отказами. В докладе формализована проблема консенсуса и рассмотрены доступные решения. В частности, мы продемонстрировано применение проблемы консенсуса для сравнения мощности синхронизации различных параллельных структур данных (например, очереди FIFO) и примитивов синхронизации ЦП для разработки параллельных неблокирующих алгоритмов с помощью "consensus numbers". Дата: пятница 14 мая 2021. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.)
Дмитрий Владимирович Кознов (Санкт-Петербургский Государственный Университет и JetBrains): Визуальное моделирование при разработке семейства телекоммуникационных систем Аннотация: Визуальное моделирование (модельно-ориентированный подход) долгие годы был предметом активных исследований и интереса со стороны индустрии. Вершиной популярности подхода стало создание и продвижение языка UML. Однако к настоящему времени энтузиазм исследователей и практиков к этой теме остыл в связи с отсутствием ощутимых, значимых практических результатов.
В докладе выдвигается тезис о том, что визуальное моделирование может быть успешным, во-первых, в рамках предметно-ориентированного подхода, во-вторых, при бесшовной интеграции со средствами разработки (IDEs), в-третьих, при использовании в рамках разработки семейств систем.
В подтверждение этих тезисов в докладе описывается пилотное предметно-ориентированное решение для программно-аппаратного семейства телекоммуникационных систем, нацеленного на автоматизацию разработки драйверов к аппаратуре и созданного на основе model-based стека технологий Eclipse.
Дата: пятница 30 апреля 2021 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН.
Андрей Михайлович Райгородский (Московский физико-технический институтб Яндекс): Теория графов и ее приложения Выступление Андрея Михайловича Райгородского было вторым из двух лекций 2021 г. из серии Ершовских лекций по информатике. Серия была основана в 2007 г. Андрем Александровичем Берсом в память о выдающемся ученом в области информатики академике Андрее Петровиче Ершове. (Подробнее - см. XVI Ершовская лекция по информатике.) Дата: пятница 23 апреля 2021. Запись лекции доступна в плейлисте Ершовских лекций.
Виктор Николаевич Касьянов (ИСИ СО РАН, Новосибирск): Академик Андрей Петрович Ершов и графы в программировании Выступление В.Н. Касьянова было первым из двух лекций 2021 г. из серии Ершовских лекций по информатике. Серия была основана в 2007 г. Андрем Александровичем Берсом в память о выдающемся ученом в области информатики академике Андрее Петровиче Ершове. (Подробнее - см. XV Ершовская лекция по информатике.) Дата: пятница 16 апреля 2021. Запись лекции доступна в плейлисте Ершовских лекций.
Первое рабочее совещание (workshop) ''Проект VeriDevOps - концепция, текущая работа'' На совещании бала представлена базовая концепция проекта VeriDevOps, цель которого автоматизация защиты и верификации для предотвращения различных угроз кибер-безопасности. Основа проекта формализация требований к кибер-безопасности, верификация и защита.
Проект находится на начальной стадии, поэтому в докладах были представлены базовые идеи и текущие направления разработки:
  1. Концепция проекта VeriDevOps.
  2. Обзор литературы по следующим направлениям:
    • извлечение требований безопасности из документов на естественном языке,
    • шаблоны формализации требований,
    • защита и верификация защиты от уязвимостей.
По итогам, приглашаем принять участие к публикации сборника статей - Верификация безопасности - от требований до защиты от уязвимостей.
Дата: пятница 16 апреля 2021 г. Запись совещания на YouTube канале Андрея Александровича Садовых.
Андрей Александрович Садовых (Университет Иннополис): Хакатоны в программах обучения разработке ПО. Опыт применения. Аннотация: При обучении разработке ПО мы сталкиваемся с несколькими проблемами: (1) у многих студентов не хватает опыта чтобы понять важность теоритического материала в практическом применении, что ведет к отстуствию мотивации и низкой вовлеченности; (2) программам обучения и исследователям нужен постоянный контакт с индустрией, что трудно реализовать в рамках классических курсов; (3) у компаний затруднен доступ к результатам исследований в области разработки ПО, а так же затруднена возможность донести до преподавателей и студентов насущные проблемы разработки. Мы предлагаем обучающие хакатоны, как способ улучшить образовательный и иследовательский процесс с помощью кратковременных но интенсивных встреч где компании, исследователи и студенты вместе решают небольшие задачи из индустрии. В докладе обсуждаем один из рецептов проведения хакатона, обобщаем отзовы участников и обсуждаем развитие этой идеи. Дата: пятница 2 апреля 2021 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.)
Александр Анатольевич Семенов (Институт динамики систем и теории управления, Иркутск): Применение алгоритмов решения SAT к обращению дискретных функций с приложениями в криптоанализе Аннотация: Доклад предполагает краткий обзор последних достижений в разделе алгебраического криптоанализа, в котором к системам уравнений криптоанализа применяются современные SAT решатели (SAT-based cryptanalysis). Было рассказано об общих техниках трансляции алгоритмов, задающих дискретные функции, в SAT. Будет дано точное понятие SAT иммунности дискретной функции. С использованием этого понятия было показано, как свести к задаче псевдобулевой оптимизации проблему построения атаки из класса «угадывай и определяй» на рассматриваемую функцию. Также были представлены результаты ряда вычислительных экспериментов. Дата: пятница 19 марта 2021 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.)
Лидия Васильевна Городняя (ИСИ СО РАН, Новосибирск): Не обижайте девушек и женщин! Доклад Л.В. Городней - основное выступление на "обобщенном 8 марта" - заседании семинара, организованного совместно с Математическим Клубом Университета Иннополис.
Аннотация: Доклад базируется преимущественно на фактографии вокруг термина "архитектура фон Неймана", конфликта вокруг патента на конструкцию ENIAC-а, особенностях юбилейных мероприятий и истории ЭВМ в нашей стране. Кроме собственно документов отдельные штрихи являются реконструкцией автора, основанной на понимании механизмов поведения.
После выступления Л.В. Городней состоялась открытая дискуссия. Участники заранее посмотрели несколько фильмов об женщинах-математиках (например, "Одаренная" и "Скрытые фигуры").
Дата: понедельник 8 марта 2021 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.)
Александр Михайлович Дехтярь (Калифорнийский Государственный Политехнический Университет, Сан Луис Обиспо): Координированное преподавания курса "Программная Инженерия для Всех Аннотация: В наши дни, преподавание основ программной инженерии в высших учебных заведениях фактически эксклюзивно ведется только для студентов "вычислительных" специальностей (информатика, компьютерные науки, программная инженерия, компьютерная инженерия, информационные системы). В то же время, барьер для успешного участия в процессе создания программного обеспечения для профессионалов с "невычеслительным" образованием, в ролях владельца ПО, специалиста в предметной области, конечного пользователя, тестера, менеджера по продукту, и других, неукоснительно снижается. Разработчики ПО сталкиваются с не-разработчиками в процессе создания ПО все чаще и чаще. Получается странная ситуация, когда среди участников проекта разработки ПО, одна группа (программисты-разработчики) обучается программной инженерии и процессу создания ПО во время своего обучения в вузах, а другая группа (все остальные участники процесса) не получают такого образования. В этом докладе мы расскажем о начальной стадии нашей попытки исправить эту ситуацию путем разработки и преподавания курса под названием "Программная инженерия без программирования" для студентов, обучающихся "невычеслительным" специальностям. Для того чтобы преподавание этого курса соответствовало девизу нашего университета "Обучайся созидая!" мы использовали технику координированного преподавания для совместного прочтения этого курса и курса "Введение в программную инженерию" для студентов специальности "программная инженерия". "Координированное преподавание" это разработанный нами в начале 2010х подход к преподаванию двух курсов с одной темой направленных на разные студенческие аудитории, при котором, каждый курс содержит свой собственный набор лекционного материала, но оба класса объединены работой над совместными лабораторными заданиями и проектами. Для студентов курса "Программная инженерия без программирования" возможность прямого общения с разработчиками, и совместной работы над программным обеспечением оказалась весьма полезной. В докладе, мы расскажем о том как построено координированное обучение, как оно было применено к курсу "Программная инженерия без программирования", и об извлеченных из нашего опыта уроках.
Соавторы: Бруно да Сильва (кафедра Информатики и Программной Инженерии, Калифорнийский Государственный Политехнический Университет, Сан Луис Обиспо), Аня Гудман (кафедра Химии, Калифорнийский Государственный Политехнический Университет, Сан Луис Обиспо).
Дата: пятница 5 марта 2021 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН.
Сергей Михайлович Старолетов (Алтайский государственный технический университет): Model checking games and a genome sequence search Аннотация: В презентации рассмотрена концепция Model Checking Games для решения алгоритмических задач. Описаны текущие подходы в этой области и осуществлен переход к игре между пользователем и верификатором с целью предоставить решение проблемы, закодированное в системе переходов и формуле LTL с требованием. Показано, как программировать и решать некоторые известные головоломки, используя этот подход. Была рассмотрена проблеме поиска паттерна в последовательности генома и рассказано о реализации метода использования Z-функции поиска подстрок на Promela, построении модели, использования реальных вирусных данных, а затем игра проверки модели с верификатором SPIN. Основываясь на экспериментах, можно сказать, что проблема поиска паттерна с некоторыми отклонениями решается с помощью Swarm Model Checking и метода Hash Compact. Дата: пятница 19 февраля 2021 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.)
Николай Вячеславович Шилов (Университет Иннополис): Устранение рекурсии в задачах на динамическое программирование Аннотация: Трансформационный подход к верификации программ был очень популярной темой исследований в первые десятилетия теории программирования. Многие выдающиеся пионеры теории программирования внесли свой вклад в разработку данного направления исследований: Джон Маккарти, Амир Пнуэли, Дональд Кнут... Много интересных примеров трансформационного подхода было тщательно изучено, что привело к методам устранения рекурсии, известным как хвостовая рекурсия и как ко-рекурсия. В данной работе мы подробно исследуем (мы надеемся) новые примеры паттернов устранимой рекурсии, причем, устранение рекурсии основано на трансформациях программ и анализе задач, решаемых этими программами. Дата: пятница 5 февраля 2021 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.)
Заседание, приуроченное к World Logic Day (https://en.wikipedia.org/wiki/World_Logic_Day) Выступления: (1) Захар Ягудин (студент 2го курса Университета Иннополис) - "О 0-1 законах для графов и логик", (2) Дмитрий Александрович Кондратьев (ИСИ СО РАН) - "Доказательство в системе ACL2 того, что sqrt(2)не является (рациональным) числом", (3) Борис Леонидович Файфель (Саратовский государственный технический университет) - "Решаем логические задачи на императивном языке программирования", (4) Андрей Валентинович Климов (Институт прикладной математики РАН) - "Использование суперкомпиляции для получения эффективных императивных программ для задачи о расстановке ферзей". Дата: пятница 15 января 2021 г. Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН.
День проблем Выступили: (1) Дмитрий А. Кондратьев (ИСИ СО РАН, Новосибирск), (2) Андрей В. Климов (ИПМ РАН, Москва), (3) Аркадий В. Климов (ИППМ РАН, Москва), (4) Н.В. Шилов (Университет Иннополис), (5) Л.В. Городняя (ИСИ СО РАН, Новосибирск). Дата: среда 30 декабря 2020 г. Рабочая (необработанная) запись на Google Drive.
Bertrand Meyer (Politecnico di Milano, Innopolis University, and Eiffel Software): The four PEGS of requirements engineering Abstarct: Bad software requirements can jeopardize projects., but requirements as commonly practiced remain a weak link in software engineering. What passes for requirements in industry usually consists of a few use cases or user stories, which fail to capture many essential aspects of systems. There is a considerable literature on requirements, including some excellent textbooks, but their lessons are rarely heeded; many projects, in particular, fail to take into account the Jackson-Zave distinction between system and environment. The standard IEEE plan for requirements dates back to 1998 and does not meet the demands of today’s ambitious developments. I will present ongoing work intended to help industry produce more useful requirements. It includes precise definitions of requirements concepts and a standard plan for requirements specifications. The plan contains four books covering the four “PEGS” of requirements engineering: Project, Environment, Goals and System. The talk does not attempt to introduce radical new concepts but rather builds on existing knowledge to define a solid basis for requirements engineering and provide projects with precise and helpful guidelines. Дата: среда 16 декабря 2020 г. Рабочая (необработанная) запись на Google Drive.
Станислав Павлович Кикоть (London Metropolitan University): Магистерские программы по информатике в Великобритании. Дата: среда 2 декабря 2020 г. Рабочая (необработанная) запись на Google Drive.
Дмитрий Александрович Кондратьев (ИСИ СО РАН): Методы и средства для формальной верификации Cloud Sisal программ. Аннотация: В ИСИ СО РАН разрабатывается облачная система параллельного программирования (CPPS). Входным языком CPPS является Cloud Sisal. Это функциональный язык программирования, основанный на циклических выражениях. Главной особенностью CPPS является неявный параллелизм, который достигается с помощью векторизации циклических выражений. В состав CPPS входят подсистемы CSV1 и CSV2 для дедуктивной верификации Cloud Sisal программ. Рассмотрим сходства обеих подсистем. Во-первых, входным аргументом обеих подсистем является Cloud Sisal программа, аннотированная на языке системы ACL2. Во-вторых, для избежания задания инвариантов циклов в обеих подсистемах используется символический метод верификации финитных итераций. Этот метод основан на замене действия цикла на применение рекурсивной функции. В-третьих, в обеих подсистемах для доказательства условий корректности применяется система ACL2. Рассмотрим основное отличие обеих подсистем. Подсистема CSV1 основана на трансляции Cloud Sisal программ в C-программы. К результату трансляции применяется система дедуктивной верификации C-lightVer, разработанная в ИСИ СО РАН ранее. Поэтому, символический метод верификации финитных итераций применяется к циклам языка C, полученным в результате трансляции Cloud Sisal циклов. Система ACL2 применяется для доказательства условий корректности полученных C-программ. В отличие от подсистемы CSV1, подсистема CSV2 основана на дедуктивной верификации исходных Cloud Sisal программ. Поэтому, символический метод верификации финитных итераций применяется к Cloud Sisal циклам. Система ACL2 применяется для доказательства условий корректности исходных Cloud Sisal программ. Даты: первая часть - среда 18 ноября 2020 г., вторая часть - среда 25 ноября 2020 г. Рабочие (необработанные) записи первой части и второй части на Google Drive.
Александр Владимирович Наумчев (Университет Иннополис): Seamless Requirements and specifications. Дата: среда 28 октября 2020 г. Рабочая (необработанная) запись на Google Drive.
Наталья Олеговна Гаранина (ИСИ СО РАН): An Ontology-based Approach to Support Formal Verification of Concurrent Systems. Abstract: Formal verification ensures the absence of design errors in a system with respect to system's requirements. This is especially important for the control software of critical systems, ranging from automatic components of avionics and spacecrafts to modules of distributed banking transactions. We present a verification support framework that enables automatic extraction of a concurrent system's requirements from the technical documentation and formal verification of the system design using an external or built-in verification tool that checks whether the system meets the extracted requirements. Our support approach also provides visualization and editing options for both the system model and requirements. The key data components of our framework are ontological descriptions of the verified system and its requirements. We describe the methods used in our support framework and we illustrate their work for the use case of an automatic control system. Дата: среда 21 октября 2020 г. Рабочая (необработанная) запись на Google Drive.