Универсальный подход к проверке отношений симуляции для моделей программ.
Универсальный подход к проверке отношений симуляции для моделей программ.
Авторы
Аннотация
Проверка правильности поведения систем взаимодействующих процессов (сетевых протоколов, встроенных систем, распределенных программ) – это одна из наиболее трудных задач программирования. Одним из наиболее распространенных способов ее решения является метод верификации моделей программ (model checking). В тех случаях, когда размеры модели не позволяют провести ее автоматический анализ за разумное время, модели приходится упрощать. Упрощение модели при этом должно быть корректным: если упрощенная модель удовлетворяет спецификации, то это должно служить гарантией того, что исходная модель также удовлетворяет этой спецификации. Для того чтобы убедиться в том, что одна модель является корректным упрощением другой, достаточно проверить, что между этими моделями имеется отношение подобия (симуляции). Существует и единообразный теоретико-игровой подход к вычислению широкого класса отношений симуляции. В этом подходе задача проверки симуляции сводится к задаче нахождения выигрышной стратегии в игре двух игроков. Мы обнаружили, что варианты такой игры для многих отношений имеют много общего. Это наблюдение было использовано для создания теоретико-игрового языка описания отношений симуляций на множестве моделей программ. Отношение симуляции на этом языке определяется списком формальных правил антагонистической игры. В терминах этого языка мы описали ряд отношений симуляции. Мы также разработали алгоритм, который позволяет для любой пары конечных моделей программ и по любому отношению симуляции, описанному на указанном теоретико-игровом языке, проверить, выполняется ли заданное отношение симуляции между этими моделями. На основе данного алгоритма было создано программно-инструментальное средство для проверки разных отношений симуляции между конечными моделями программ. Поиск выигрышных стратегий проводится с использованием аппарат двоичных разрешающих диаграмм. Разработанное универсальное средство проверки симуляций может использоваться при решении различных задач верификации моделей программ, включая построение абстракций моделей, вычисление инвариантов параметризованных распределенных систем.
Ключевые слова
Издание
Труды Третьей Всероссийской конференции «Методы и средства обработки информации», Москва, 2009, Москва, с. 104-110.
Научная группа
Все публикации за 2009 год
Все публикации