Во вторник 9 декабря 2025 г. пройдет семинар "Теоретическое и экспериментальное программирование" (Руководитель: к.ф.-м.н., с.н.с. Гаранина Н.О., соруководители: к.ф.-м.н., н.с. Кондратьев Д.А., к.ф.-м.н., с.н.с. Ануреев И.С., секретарь: к.ф.-м.н. Шилов Н.В.).
Время проведения: 17.00-18.30 НСК (13.00-14.30 МСК) очно в к. 239 ИСИ СО РАН и онлайн по ссылке.
Анонсы, слайды докладов и другая информация будут доступны в группе телеграм.
Докладчик: Максим Вячеславович Нейзов (Институт Автоматики и Электрометрии СО РАН)
Тема: Loom: Использование симметрии при разработке и верификации программных реагирующих систем
Большое пространство состояний реальных программ затрудняет или делает невозможной их непосредственную верификацию методом проверки модели (model checking). Наличие симметрии в программе достаточно часто позволяет упростить модель и сократить её пространство состояний, что приводит к резкому снижению времени верификации. Классический подход состоит в обнаружении группы симметрии и построении на её основе упрощенной модели для верификации. Однако не все инструменты имеют поддержку симметрии, а инструменты с такой поддержкой не всегда справляются с поставленной задачей.
В докладе предлагается альтернативный классическому подход к разработке программ основанный на симметрии. В программе выделяется ядро – координационный центр, который работает с учётом симметрии и отвечает за выполнимость заданных темпоральных свойств.
Ядро координирует вычисления, которые вынесены за его пределы – в обвязку ядра. В связи с этим ядро имеет небольшое пространство состояний и может быть верифицировано методом проверки модели. Обвязка не может вмешиваться в работу верифицированного ядра и нарушать его свойства.
Подход продемонстрирован на примере разработки и верификации арбитра ресурсов марсохода. Арбитр координирует доступ n процессов к m ресурсам, где n и m -- натуральные числа. Используются язык программирования C/C++ и инструмент проверки модели Spin. Модель поведения ядра автоматически извлекается верификатором Spin из C-кода. Проверке подлежат темпоральные свойства, выраженные в логике LTL.