Во вторник 6 октября 2026 г. состоится семинар имени В. А. Непомнящего в ИСИ СО РАН "Т...
Во вторник 6 октября 2026 г. состоится семинар имени В. А. Непомнящего в ИСИ СО РАН "Теоретическое и экспериментальное программирование" (Руководитель: к.ф.-м.н., с.н.с. Гаранина Н.О., соруководители: к.ф.-м.н., н.с. Кондратьев Д.А., к.ф.-м.н., с.н.с. Ануреев И.С., секретарь: к.ф.-м.н. Шилов Н.В.). Время проведения: 17.30-19.00 НСК (13.30-15.00 МСК) очно в к. 239 ИСИ СО РАН и онлайн по ссылке: https://telemost.yandex.ru/j/28529522210499 Докладчик: Арсений Бочкарёв (аспирант ИТМО). Тема: Разработка среды для моделирования и верификации коммуникационных протоколов. Одним из способов получения строгих математических гарантий корректности коммуникационных протоколов являются инструменты проверки моделей. Однако использование существующих верификаторов зачастую может требовать ручного описания низкоуровневых деталей асинхронного взаимодействия, что усложняет процесс моделирования и повышает порог входа для экспертов предметной области. Доклад содержит краткий обзор существующих формализмов и языков представления протоколов. Далее будет представлена собственная среда моделирования, центральным элементом которой является небольшой предметно-ориентированный язык "TVL" на базе семантики взаимодействующих автоматов с ограниченными каналами. Данный язык позволяет высокоуровнево описывать логику обмена сообщениями, абстрагируясь от вычислительных конструкций. Созданный инструментарий обеспечивает трансляцию моделей и спецификаций во входные языки инструментов SPIN и TLA+ (TLC), а также возможности по автоматической генерации этих спецификаций и унифицированное представление результатов верификации. Кроме того, будут освещены текущие результаты по развитию проекта: разработка собственного инструмента проверки моделей, ускорение верификации при помощи CEGAR и расширение возможностей языка TVL.