ТЕСТИРОВАНИЕ, ВЕРИФИКАЦИЯ И ВАЛИДАЦИЯ ПРОГРАММ
удк 681.3.06
ТЕОРЕТИКО-ИГРОВОЕ СРЕДСТВО ПРОВЕРКИ ОТНОШЕНИЙ
СИМУЛЯЦИЙ
© 2011 г. П.Е. Булычев Вычислительный центр РАН Факультет вычислительной математики и кибернетики МГУ им.М.В. Ломоносова 119992 Москва, Воробьевы горы E-mail: peter.bulychev@gmail.com Поступила в редакцию 12.06.2011 г.
Одним из наиболее распространенных методов проверки правильности программ является верификация моделей программ. В этом методе проверяется не сама программа, а её модель, задаваемая структурой Крипке (размеченной системой переходов). Спецификация обычно задаётся формулой темпоральной логики. Во многих подзадачах верификации моделей программ используются отношения, заданные на множестве моделей и сохраняющие выполнимость формул темпоральных логик. Существует целый ряд таких отношений, и они называются отношениями симуляции. В настоящей статье предложена программная система, предназначенная для проверки широкого класса отношений симуляции между конечными моделями программ. В основу этой системы положен теоретико-игровой подход к проверке симуляции. Система состоит из двух компонентов: формального языка, позволяющего описывать различные симуляции в терминах антогонистической игры двух игроков, и программно-инструментального средства, которое по двум размеченным системам переходов и описанию симуляции проверяет, выполняется ли заданная симуляция между этими системами переходов.
1. ВВЕДЕНИЕ
Проверка правильности программ — это одна из наиболее трудных задач программирования. Широко используемое на практике тестирование программного обеспечения не позволяет установить корректность функционирования анализируемой программы, а лишь помогает выявить наличие в ней ошибок.
Поэтому для проверки правильности программных систем, цена ошибки в которых велика (жизненно важное ПО, встроенные системы), используются формальные методы верификации, позволяющие получить строгие математические доказательства отсутствия дефектов в поведении программ.
В данной работе рассматривается один из формальных методов, метод верификации моделей программ (model checking) [1]. В этом методе
проводится проверка не самой программы, а её математической модели. Модель представлена структурой Крипке (размеченной системой переходов), а проверяемая спецификация — формулой темпоральной логики. Существует множество алгоритмов проверки выполнимости темпоральной формулы на конечной модели.
Важным этапом метода является построение модели. Модели могут отражать поведение программы с разной степенью подробности, они могут строиться как вручную, так и автоматически [2]. Чрезмерно упрощённая модель может давать слишком грубое приближение реальной программы, и на ней не будут проявляться те свойства вычислений, которые присущи реальной программе. С другой стороны, при верификации чрезмерно подробных моделей приходится преодолевать эффект комбинаторного взрыва
числа состояний, из-за которого применение алгоритмов проверки выполнимости темпоральных формул становится практически неосуществимым. Поэтому для применения метода верификации моделей удобно иметь средство, позволяющее сравнивать устройство моделей программ между собой. Наиболее важными отношениями между моделями программ являются отношения симуляции, которые проявляются в том, что устройство одной модели оказывается подобным устройству другой. Это приводит к тому, что выполнимость формул некоторой темпоральной логики на одной модели неизбежно влечёт их выполнимость и на другой. Такого рода отношения подобия (симуляции) находят широкое применение при проверке правильности поведения сложных программ.
Отношения симуляции могут использоваться для проверки того, что одна модель является уточнением (или абстракцией) другой модели. Это позволяет инкрементально строить модель, постепенно уточняя её поведение [3]. Отношения симуляции могут также использоваться для вычисления инвариантов бесконечных параметризованных семейств моделей [4], для нахождения симметрии в моделях [5], для автоматического уменьшения размеров моделей [6, 7], для проверки свойств конфидициальности многопоточных программ [8].
Разнообразие отношений симуляции велико; в данной работе в качестве примера будут использоваться два отношения: строгая симуляция (сохраняющая выполнимость формул логики ЛСТЬ) и прореженная симуляция (сохраняющая выполнимость формул логики
ЛСТЬх).
Существует несколько подходов к вычислению отношений симуляции: поиск наибольшего устойчивого разбиения [9], нахождение неподвижной точки [10], теоретико-игровой подход [11], в данной работе мы будем использовать теоретико-игровой подход. В этом подходе задача проверки симуляции сводится к задаче нахождения выигрышной стратегии в конечной игре двух игроков. Теоретико-игровой подход может использоваться для проверки большого числа отношений симуляции, позволяя при
этом получать оптимальные по сложности алгоритмы.
Сравнительный анализ определений правил игр для проверки различных отношений симуляции приводит к мысли о том, что эти правила имеют много общих черт. Это наблюдение было использовано в данной работе для создания теоретико-игрового языка описания отношений симуляций на множестве моделей программ. Отношение симуляции на этом языке определяется списком формальных правил антагонистической игры. В терминах предложенного языка мы описали ряд отношений. К их числу относятся строгая симуляция, слабая симуляция, прореженная симуляция, к.2 симуляция и другие. Это показывает, что предложенный нами язык описания симуляций имеет хорошие выразительные возможности.
Нам удалось разработать универсальный алгоритм, который позволяет для любой пары моделей программ и для любого отношения симуляции, описанного на указанном теоретико-игровом языке, проверить, выполняется ли заданное отношение симуляции между этими моделями. На основе данного алгоритма было создано программно-инструментальное средство для проверки разных отношений симуляции между конечными моделями программ. В качестве языка описания моделей использовался язык верификатора КиЯМУ [12]. Поиск выигрышных стратегий проводится с использованием аппарата двоичных разрешающих диаграмм [13].
2. ЗАДАЧА ВЕРИФИКЦИИ МОДЕЛЕЙ ПРОГРАММ
В методе верификации моделей программ анализируется не сама программа, а её математической модель, которая является некоторой абстракцией исходной программы. Модель может быть представлена структурой Крипке (размеченной системой переходов), а проверяемая спецификация — формулой темпоральной логики.
2.1. Модели программ
Структура Крипке включает в себя множество состояний 5 с одним выделенным начальным
состоянием во £ 5. Состояние структуры Крипке соответствует "моментальному снимку" или глобальному состоянию вычисления программы, которую моделирует эта структура Крипке. Поскольку в общем случае число таких состояний бесконечно, то применяется абстракция: выделяется некоторое множество свойств £ (атомарных переменных), и каждое состояние в характеризуется булевым вектором Ь(в), показывающим, какие свойства верны в данном состоянии, а какие — нет. Для того, чтобы описать, как может изменяться состояние программы, используется отношение переходов Я С 5 х 5. Таким образом, мы приходим к следующему определению структуры Крипке:
Определение 2.1. Структура Крипке (размеченная система переходов, ЬТБ) — это пятёрка {Б, во, Я, £, Ь), где
• Б — конечное множество состояний,
• в0 £ Б — начальное состояние,
• Я С Б х Б — отношение переходов,
• £ — множество атомарных переменных,
• Ь : Б ^ 2е — функция разметки состояний.
Любая пара состояний (в1,в2) £ Я называется переходом. Для простоты будем писать в1 ^ в2 вместо (в1,в2) £ Я. Обычно предполагается, что отношение переходов является тотальным, т. е. для любого состояния в1 £ Б существует такое состояние в2, для которого выполняется в1 ^ в2. Для улучшения наглядности рассматриваемых примеров мы не будем придерживаться этого требования.
Вычислением системы переходов М, начинающимся в в1, является такая бесконечная последовательность состояний п = (в1,в2,...), что для любого неотрицательного г выполняется вг ^ вг+1. Обозначим пг — суффикс п, начинающийся с позиции г.
Способы построения структур Крипке для систем взаимодействующих процессов описаны в работе [1].
2.2. Темпоральные спецификации
Для задания спецификаций поведения программ часто используют темпоральную логику ветвящегося времени CTL [14] и логику линейного времени LTL [15]. Логика CTL описывает свойства деревьев вычислений, и в ней, например, можно задать свойство AG(p ^ EFq), которое гласит, что для любого вычисления, всякий раз, когда в этом вычислении встретится некоторое состояние, удовлетворяющее атомарному свойству p, то это вычисление можно продолжить до состояния, удовлетворяющего свойству q. Логика ACTL--это фрагмент CTL, в котором позволяется задавать только свойства, которые должны выполняться на всех вычислениях (а не на некоторых).
Логика линейного времени LTL позволяет описывать свойства вычислений (но не деревьев вычислений).
В логиках CTL, ACTL, LTL имеется оператор X, используемый для описания свойств, которые должны выполняться в следующем состоянии вычисления. Данный оператор не применяется для описания свойств параллельных асинхронных систем, поскольку порядок выполнения процессов в таких системах недетерменирован [16]. Будем обозначать Лх (например LTLx, CTLx) фрагмент логики Л, в котором не используется оператор X.
Более подробно темпоральные логики, используемые при верификации моделей программ, рассмотрены в работе [1].
Будем писать M |= р, если формула р выполняется на размеченной системе переходов M.
Логика линейного времени LTL поддерживается средством верификации моделей Spin [17], а логика ветвящегося времени CTL — средством NuSMV [12].
3. РАЗЛИЧНЫЕ ВИДЫ СИМУЛЯЦИЙ
Будем рассматривать отношения между размеченными системами переходов (LTS), которые проявляются в том, что устройство одной LTS оказывается подобным другой. Такие отношения могут быть охарактеризованы классом свойств, выполнимость которых они сохраняют.
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.