О семинаре

Заседания семинара посвящены современным проблемам программной инженерии, методам и инструментам разработки, анализа и тестирования программ. В список тем семинара входят:

  • Извлечение, анализ и моделирование требований
  • Парадигмы моделирования вычислительных систем
  • Методы проектирования систем
  • Архитектуры программных систем
  • Статический и динамический анализ программ
  • Динамическая верификация и мониторинг
  • Автоматизация построения тестов
  • Анализ полноты тестирования
  • Моделирование, измерение и тестирование производительности
  • Анализ защищенности и безопасности вычислительных систем
  • Интеграция различных методов верификации
  • Проблемы внедрения новых технологий в практику разработки
  • Вопросы обучения технологиям разработки и анализа программ

Семинар рассчитан на студентов, аспирантов и их руководителей, а также практиков и специалистов из индустрии. О планах активно принимать участие в семинаре заявили представители компаний Intel, Microsoft, Яндекс и др.

Заседания семинара проходят раз в месяц по четвергам в 17:00, в Институте системного программирования РАН в аудитории 110.

Если вы хотите выступить на семинаре, напишите об этом Александру Константиновичу Петренко.

Ближайшая встреча семинара состоится 21 марта 2019 года

Будем рады, если вы расскажете коллегам о семинаре и разместите наш постер у вас.

 
Leave a comment

21 марта: Управление дублированной информацией в software данных

Кознов Дмитрий Владимирович

Кознов Дмитрий Владимирович

Кознов Дмитрий Владимирович — доктор технических наук, профессор кафедры системного программирования СПбГУ.

В компаниях по разработке ПО и в отдельных программных проектах к настоящему времени накапливается большое количество данных – требования, ошибки и отчёты об ошибках, запросы на изменения, комментарии к коду и документация, исходные тексты программ и их версии, тесты и т.д. Важной характеристикой этих данных является возрастающий объем и наличие разнообразной текстовой информации. При этом остро стоит вопрос автоматического управления этими данными, в частности, управление дублированием. В докладе будет рассказано о задаче управления дублированными отчётами об ошибках (crash reports) на примере индустриального решения компании JetBrains, а также о задаче поиска и рефакторинга нечётких дубликатов в JavaDoc-документации. Будут также рассмотрены различные индустриальные постановки задачи управления нечёткими дубликатами как в программном коде, так и в других software-данных.

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

Leave a comment

21 февраля: Методы и средства реализации программно-управляемого процесса разработки программного обеспечения критически важных информационных систем

Самонов Александр Валерьянович

Самонов Александр Валерьянович

Самонов Александр Валерьянович — старший научный сотрудник Военно-космической академии имени А.Ф. Можайского, кандидат технических наук, доцент.

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

- графово-текстовая метамодель формализованного представления комплекса требований и описаний архитектуры в виде набора взаимосвязанных fUML-диаграмм;

- методика реализации программно-управляемого процесса разработки и верификации при помощи разработанных моделей и алгоритмов.

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

Leave a comment

20 сентября: Автоматное программирование: определение, модель, реализация

Вячеслав Любченко

Вячеслав Любченко

Любченко Вячеслав Селиверстович — независимый разработчик. Научные интересы: автоматное программирование.

В докладе дается оценка текущему состоянию автоматного программирования. По мнению автора доклада, это универсальная технология проектирования программ на базе теории конечных автоматов. Рассматриваются вопросы формализации и реализации автоматного программирования. В качестве формальной модели автоматных программ на структурном уровне предлагается использовать схему программы, управление описывается в виде абстрактной модели конечного автомата. Для эффективного описания, алгоритмизации, программирования и реализации программных автоматных процессов на уровне модели управления вводятся следующие законы и модели: инерционный закон функционирования автоматов, модель дизъюнктивных автоматов, модель вложенных автоматов и модель сетей на их базе. В контексте параллельной модели автоматного программирования формулируется сетевая модель управления автоматных программ. Для корректной реализации параллелизма реальных процессов модель параллельных автоматных программ дополняется концепцией теневой памяти. Рассматривается алгоритм программного ядра интерпретации автоматных программ, заданных таблицами переходов. Дается определение параллельного объектного автоматного программирования и рассматривается его возможная реализации на языке С++. В заключение обсуждается перспектива использования и развития парадигмы визуального автоматного программирования и его приложений в качестве модели и средства реализации программных процессов кибер-физических систем.

Здесь можно скачать слайды доклада в формате PDF.

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

Leave a comment

21 июня: К вопросу построения инструмента формальной верификации смарт-контрактов

Шишкин Евгений Сергеевич

Шишкин Евгений Сергеевич

Шишкин Евгений Сергеевич — ведущий исследователь, научный отдел компании ИнфоТеКС. Научные интересы: дедуктивные методы формальной верификации, методы формальной спецификации, построение специализированных доменных логик, спецификация и верификация распределенных и реагирующих систем, функциональное программирование.

Информационные системы на базе технологии блокчейн способны реализовывать принципиально новые виды бизнес-сценариев с повышенным уровнем прозрачности выполняемых операций, сохраняемых данных и возможностью проводить криптовалютные взаиморасчеты. Бизнес-сценарии оформляются в виде специальных программ, называемых смарт-контрактами. Ряд инцидентов по взлому смарт-контрактов убедительно показал, что индустрия не умеет строить надежные смарт-контракты и остро нуждается в дополнительных средствах проверки корректности программных артефактов этого класса.

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

В основном докладе планируется затронуть такие темы:

  • Научная и бизнес-актуальность решаемой задачи
  • Существующие решения поиска дефектов в программах на языке Solidity и байт-коде EVM
  • Альтернативные языки написания смарт-контрактов, устраняющие некоторые классы ошибок «по построению»
  • Свойства программ смарт-контрактов, которые желательно уметь проверять, включая темпоральные свойства
  • Об одном подходе тяжеловестной дедуктивной верификации смарт-контрактов

Помимо доклада планируется провести дискуссию со специалистами ИСП РАН и, возможно, приглашенными экспертами по программированию и аудиту смарт-контрактов для выработки общего взгляда на проблему и пути решения.

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

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

Leave a comment

1 марта: О верификации программ, манипулирующих строковыми данными

Непейвода Антонина Николаевна

Непейвода Антонина Николаевна

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

В докладе будет рассмотрена проблема преобразования и верификации программ, манипулирующих строками. Предложен новый метод описания свойств параметризованных конфигураций анализируемой программы посредством языка уравнений в словах. Уравнение в словах есть выражение вида w = u, где w, u - слова в алфавите, являющимся объединением алфавита символов и алфавита строковых переменных. За счет использования языка уравнений в словах можно выявить и кратко выразить некоторые нетривиальные свойства допустимых значений параметров.

Метод развивается в терминах суперкомпиляции - метода преобразования программ, основанного на развертке и свертке дерева параметризованных состояний оптимизируемой программы. На базе идеи описания свойств строковых параметров посредством уравнений в словах построен модельный суперкомпилятор MSCP-A - оптимизатор программ на языке программирования Рефал.

Расширенный вариант аннотации доклада можно прочитать по этой ссылке.

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

Leave a comment

16 ноября: Операционные методы в приложении к слабым моделям памяти

Антон Подкопаев

Антон Подкопаев

Подкопаев Антон Викторович — аспирант кафедры системного программирования математико-механического факультета СПбГУ, сотрудник JetBrains Research (Language Processing Lab).

Антон Подкопаев работает над моделями памяти для языков С/С++ с учетом многопоточности. Модель памяти должна предоставлять гарантии программисту и тем ограничивать пространство возможных поведений программы. С другой стороны, модель памяти обязана учитывать оптимизирующее поведение компиляторов и процессоров, т.к. они влияют на семантику многопоточной программы. Антон Подкопаев предложил операционный вариант модели памяти для языков C/С++ и доказал корректность компиляции для «обещающей’» модели памяти в две модели процессорной архитектуры ARM — ARMv8 POP и ARMv8.3.

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

Leave a comment

21 сентября: ИНТЕРКОМП-технология создания сложных систем управления

Грудцин Сергей Николаевич

Грудцин Сергей Николаевич

Грудцин Сергей Николаевич — кандидат физико-математических наук, ведущий специалист НПО «Алмаз».

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

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

Leave a comment

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