Семинар теоретического и экспериментального программирования имени В.А. Непомнящего
Семинар возобновляет серию одноименных научных семинаров Института систем информатики СО РАН и носит имя своего основателя Валерия Александровича Непомнящего.
Семинар посвящен исследованиям и использованию формальных методов при разработке программных систем. Он может служить площадкой для обмена идеями и опытом между энтузиастами-исследователями и практиками, а также для расширения кругозора студентов и аспирантов.
В рамках семинара предполагаются доклады о собственных исследованиях, обзор конференций и/или интересных работ отечественных и зарубежных ученых, а также просмотр и обсуждение докладов ведущих ученых и представителей индустрии.
Семинар проводится еженедельно по вторникам 17.00-18.30 НСК (13.00-14.30 МСК) очно в к. 239 ИСИ СО РАН и онлайн по ссылке.
Анонсы, слайды докладов и другая информация будут доступны в группе телеграм.
Руководитель: к.ф.-м.н., с.н.с. Гаранина Наталья Олеговна
Соруководители: к.ф.-м.н., н.с. Кондратьев Дмитрий Александрович, к.ф.-м.н., с.н.с. Ануреев Игорь Сергеевич
Секретарь: к.ф.-м.н. Шилов Николай Вячеславович
Первый семинар состоится 23 сентября в 17:00 в каб. 239 ИСИ СО РАН.
Докладчик: к.ф.-м.н., с.н.с. Гаранина Наталья Олеговна
Тема: Безопасные мутации взаимодействующих автоматов: на пути к либеральному программированию
В нашей работе мы исследуем изменения взаимодействующих через каналы FIFO-машин, формализующих поведение акторов коммуникационных протоколов. Мотивацией нашей работы служит тот факт, что описание поведения акторов на специализированных языках программирования протоколов, может изменяться в силу различных причин, таких как изменение содержания сообщений, изменение условий или последовательности получения и отправки сообщений, изменение адресатов и т.п. Во всех этих случаях необходимо убедиться, что коммуникационный протокол, участником которого является изменившийся актор, по-прежнему остаётся корректным. Формальная верификация коммуникационных протоколов является ресурсоёмкой процедурой, поэтому целесообразно определить безопасные изменения поведения акторов, сохраняющие корректность протокола. В этой работе мы рассматриваем класс мутаций акторов, который предполагает включение поведений акторов, т.е. мутировавший актор выполняет только часть работы оригинального актора.