Дмитрий Трайтель: Сертифицированный специалист по мониторингу во время выполнения.

Описание: Вторник, 26 мая 2026 г.
Сертифицированный мониторинг во время выполнения
(Дмитрий Трайтель, Копенгагенский университет)

Мониторинг во время выполнения занимается проверкой, событие за событием, соответствует ли работающая система формальной спецификации. Традиционно мониторы во время выполнения выдают лишь пустые вердикты, предоставляя пользователям мало объяснений и не давая возможности независимо проверить ответ. В этом докладе рассматривается направление работы, в котором вердикты заменяются объектами доказательства — древовидными свидетелями, близкими к семантике спецификации, которые одновременно служат удобочитаемыми объяснениями и машинопроверяемыми сертификатами. Нашей отправной точкой является надежная и полная локальная система доказательства для линейной темпоральной логики (LTL) на словах лассо, которая предоставляет объяснения для контрпримеров, полученных от средств проверки моделей. Затем мы адаптируем локальную систему доказательства к условиям онлайн-мониторинга и к метрической темпоральной логике (MTL) над потоками событий с временными метками, а также добавляем средство проверки доказательств, доказавшее свою корректность в Isabelle/HOL. Наконец, мы расширяем подход к метрической темпоральной логике первого порядка (MFOTL), используя аргумент активной области, который приводит к конечным объектам доказательства первого порядка. Мы вводим и используем разделенные деревья решений для представления объяснений MFOTL и интегрируем этот подход в инструмент WhyMon с графическим интерфейсом для интерактивного изучения объяснений.

Более подробную информацию о семинарах MIAO можно найти на сайте https://jakobnordstrom.se/miao-seminars/ .