Бочкарев06окт26

Докладчик: Арсений Бочкарёв (ИТМО, аспирант) Тема: Разработка среды для моделирования и верификации коммуникационных протоколов Аннотация: Одним из способов получения строгих математических гарантий корректности коммуникационных протоколов являются инструменты проверки моделей. Однако использование существующих верификаторов зачастую может требовать ручного описания низкоуровневых деталей асинхронного взаимодействия, что усложняет процесс моделирования и повышает порог входа для экспертов предметной области. Доклад содержит краткий обзор существующих формализмов и языков представления протоколов. Далее будет представлена собственная среда моделирования, центральным элементом которой является небольшой предметно-ориентированный язык "TVL" на базе семантики взаимодействующих автоматов с ограниченными каналами. Данный язык позволяет высокоуровнево описывать логику обмена сообщениями, абстрагируясь от вычислительных конструкций. Созданный инструментарий обеспечивает трансляцию моделей и спецификаций во входные языки инструментов SPIN и TLA+ (TLC), а также возможности по автоматической генерации этих спецификаций и унифицированное представление результатов верификации. Кроме того, будут освещены текущие результаты по развитию проекта: разработка собственного инструмента проверки моделей, ускорение верификации при помощи CEGAR и расширение возможностей языка TVL.