Содержание к диссертации
Введение
1 Базовые определения и результаты 22
1.1 Логики 22
1.2 Примеры 32
1.2.1 Задача о монетках 32
1.2.2 Угадывание числа 35
2 Алгоритмические проблемы комбинированных логик 39
2.1 Комбинирование знании и неподвижных точек 40
2.2 Алгоритмические проблемы для комбинированных логик . 43
2.3 Асинхронные системы с забывающими агентами 40
2.4 Синхронные системы с абсолютной памятью 49
2.5 Проверка на модели приобретения знании 54
2.6 Формулы с ограниченной глубиной знаний 5G
3 Аппроксимациониый алгоритм для //-исчисления 64
3.1 Проверка на модели для //-исчисления С4
3.2 Специальная префиксная форма G5
3.3 Полиномиальная проверка на модели 67
4 Аффинное представление данных 71
4.1 Модели 72
4.1.1 Синтаксис 72
4.1.2 Семантика 73
4.1.3 От нечисловых к числовым 78
4.1.4 Пример: игра в числа 79
4.2 Ограниченные аффинные множества 80
4.2.1 Представление пропозициональных констант и действий 81
4.2.2 Операции на аффинных множествах 83
4.2.3 Оптимизация 87
4.2.4 Проверка включения 89
4.3 Векторно-аффинные множества 92
4.3.1 Представление пропозициональных констант и действий 93
4.3.2 Операции на векторно-аффинных множествах 95
4.3.3 Оптимизация 99
4.3.4 Проверка включения 101
4.4 Векторно-аффинные множества versus BDD 104
4.5 Аффинная проверка на моделях комбинированных логик 108
4.5.1 Агенты в описании моделей 108
4.5.2 Агенты и забывающие агенты 111
4.5.3 Агенты с абсолютной памятью 113
4.5.4 Представление пропозициональных констант и действий 113
4.5.5 Операции на аффинных деревьях 115
4.5.G Оптимизация 121
4.5.7 Проверка включения 122
5 На пути к реализации 125
5.1 Система проверки на модели Экзаменатор 125
5.2 Интерфейс и параметры программы 127
5.3 Эксперимент 127
Заключение 129
Комбинированные логики 129
- Алгоритмические проблемы для комбинированных логик
- Представление пропозициональных констант и действий
- Аффинная проверка на моделях комбинированных логик
- Представление пропозициональных констант и действий
Введение к работе
В настоящей главе обсуждается актуальность работы, дан краткий обзор основных результатов и открытых проблем исследуемой области, сформулированы цели диссертации, описаны полученные результаты, отмечается их новизна. В конце главы дан краткий обзор структуры диссертации.
Актуальность
На сегодняшний день в области создания систем передачи и обработки данных сложилась диспропорция темпов развития трёх её основных компонентов: микропроцессорной техники, средств телекоммуникации и разработки программного обеспечения. Согласно закономерности, замеченной основателем компании Intel Гордоном Муром, быстродействие микропроцессоров удваивается без изменения их стоимости каждые 18 месяцев, пропускная спо-собность каналов передачи данных растёт на 75 % кажділе 12 месяцев, и лишь в индустрии программного обеспечения скорость разработки программных систем растёт всего на 4-5 % в год. Это приводит к тому, что разрыв между техническими возможностями и технологиями обработки и передачи информации всё время увеличивается.
В значительной степени, это происходит из-за отсутствия удовлетворительного для промышленности решения проблемы проверки правильности программных систем и логических схем вычислительных устройств. Например, из практики разработки программного обеспечения хорошо известно, что примерно 2/3 времени, затрачиваемого на создание системы, приходится на отладку, т.е. проверку её правильности. При создании алгоритма и выборе системы программирования можно руководствоваться многочисленны ми пособиями, справочниками и пр. Проверка синтаксической правильности. программы и её трансляция в исполняемый машинный код осуществляется полностью автоматически. Но этан отладки программ, т.е. проверка семантической правильности, до сих пор плохо автоматизирован. Воспользуемся образным сравнением из [50]:
Средства отладки программы, которые входят в состав всякой развитой системы программирования, могут помочь разработчику в той же мере, в какой лопата оказывает помощь кладоискателю. Главные вопросы — где копать и стоит ли копать вообще? Здесь скорее пригодилось бы устройство наподобие металлоис-кателя. Но хороший металлоискатель — это тонкий инструмент, требующий знания его устройства и умелого обращения. Так, что кроме лопаты неплохо бы использовать и автоматические системы поиска ошибок и проверки правильности функционирования программ и вычислительной аппаратуры.
Как правило, большинством разработчиков программных систем для проверки правильности проекта практикуются старые добрые методы имитационного моделирования и тестирования. Они довольно эффективны на самых ранних стадиях отладки, когда проектируемая система всё ещё изобилует ошибками, но результативность этих методов быстро снижается, как только система становится чище.
Достойной альтернативой имитационному моделированию и тестированию являются методы формальной верификации. При имитационном моделировании и тестировании исследуются только некоторые из возможных сценариев поведения проектируемой системы, поэтому остаётся открытым вопрос о том, не содержится ли фатальная ошибка в незадействованных траекториях. Формальная верификация же обеспечивает исчерпывающий анализ всех возможных вариантов поведения системы.
В настоящее время во многих критических приложениях, где любой отказ считается недопустимым, таких как системы управления воздушным и дорожным движением, медицинская аппаратура, электронная коммерция, сети телефонных коммутаторов широко используются аппаратные и программные
Ф системы. Поэтому ещё более насущной задачей становится разработка эффек тивных методов, способствующих повышению нашей уверенности в правильности работы программных систем.
Во многих таких системах естественно возникает понятие знания в силу связи между знанием и действием. Что робот должен знать, чтобы открыть
сейф, и откуда он знает, достаточно ли он знает, чтобы открыть его? Перед
пересылкой очередного сообщения, знает ли отправитель, что получатель получил предыдущее? В какой момент экономический агент знает уже достаточно, чтобы остановить сбор информации и принять решение? Когда база данных может ответить на вопрос "Я не знаю"? Поэтому часто бывает, что правильность функционирования программной системы зависит от "знаний" её компонентов.
В настоящей работе изучаются с теоретической и экспериментальной точки зрения некоторые новые эффективные формализмы для повышения на дёжности программных систем. Особенность подхода состоит в использова нии эпистемических логик — логик знаний — для описания поведения моделей программ.
Метод верификации моделей программ
Техника верификации, получившая название проверки па модели, является одним из наиболее перспективных и широко используемых подходов к реше- # нию проблемы автоматизации отладки и проверки правильности программ.
Она была разработана в 80-х гг. Кларком и Эмерсоном в США, а также независимо Квайлом и Сифакисом во Франции. Суть проверки на модели проста, и её этапы можно описать следующим образом:
Моделирование Для проектируемой системы необходимо построить её абстрактную модель (например, конечную систему переходов), приемлемую для инструментальных средств верификации моделей программы. Как правило, это просто задача компиляции и, возможно (при ограни-. чешш по времени и объёму памяти), абстракции, чтобы избавиться от несущественных деталей.
Спецификация Эта задача состоит в формулировании свойств, которыми должна обладать проектируемая система. Обычно спецификации задаются на языке формальной логики. Для аппаратуры и программного обеспечения, как правило, применяют динамические логики, временные логики и их варианты с неподвижными точками. Важным вопросом является полнота спецификации. Метод проверки на модели даёт возможность убедиться, что модель проектируемой системы соответствует заданной спецификации, однако определить, охватывает ли заданная спецификация все свойства, которыми должна обладать система, невозможно.
Верификация Результатом вычислений алгоритма глобальной проверки на модели является множество состояний модели, в которых спецификация выполняется, а алгоритм локальной проверки на модели либо завершает работу с ответом true, означающим, что модель удовлетворяет спецификации, либо строит в качестве контрпримера некоторое вычисление (ошибочную трассу), которое показывает, почему формула не выполняется. Контрпример особенно важен для поиска тонких ошибок в сложных системах переходов. Его анализ может повлечь за собой модификацию системы и повторное применение алгоритма проверки на модели.
Процедура проверки на модели может быть реализована достаточно эффективным алгоритмом, способным работать на вычислительных машинах невысокого класса (но обычно всё-таки не на стандартных персональных компьютерах).
Хотя ограничение, связанное с конечным числом состояний модели, выглядит существенным недостатком, метод проверки на моделях применим ко многим важным классам программных систем, например, к различным коммуникационным протоколам, а многие системы с бесконечным числом состояний могут быть представлены с помощью метода абстракции как конечные модели. Например, программа с неограниченной очередью сообщений может быть верифицирована, если ограничиться рассмотрением очередей небольшого размера.
По сравнению с другими подходами в формальной верификации про грамм, метод проверки на модели обладает двумя замечательными преимуществами.
• Он полностью автоматический, и его применение не требует от иользо- " вателя никаких особых знаний в таких математических дисциплинах,
как логика и теория доказательства теорем. Всякий, кто может про вести моделирование проектируемой системы, вполне способен осуществить и проверку этой системы.
• Если проектируемая система не обладает желаемым свойством, то результатом проверки на модели будет контрпример, который демонстрирует поведение системы, опровергающее это свойство. Эта ошибочная трасса даёт бесценную информацию для понимания причины ошибки, равно как и важный ключ к решению возникшей проблемы.
Эти два замечательных достоинства, а также открытие символических методов проверки на моделях, позволяющих проводить исчерпывающий неявный перебор в пространстве с астрономически большим числом состояний, совершили революционный переворот в области формальной верификации и перевели её из чисто академической дисциплины в дееспособную практическую технологию, которая потенциально может быть внедрена во многие промышленные процессы разработки в качестве ценного дополнительного метода для проверки правильности проектируемых систем.
Достаточным свидетельством тому, что в промышленности широко признан огромный практический потенциал метода проверки на модели, служит большое число исследователей и разработчиков, которые создают оригинальные средства проверки на модели и занимаются их применением в большинстве крупных компаний но производству современных полупроводниковых устройств и процессоров. На сегодняшний день в мире действуют уже свыше двадцати систем верификации программ, построенных по принципу проверки на моделях. Ф Простота принципа проверки на модели не вырождается в банальность, поскольку методы проверки программ различаются выбором программной логики для спецификации свойств программ, выбором алгоритма проверки формул в конечных моделях и выбором формата представления данных, т.е. моделей и формул. Имеется большое разнообразие формальных языков спецификаций, алгоритмов их проверки и структур представления данных. Программные логики оказались полезным средством для выражения раз личных свойств параллельных систем. Традиционно они включают динами ческие логики, временные логики и их варианты с неподвижными точками [30, 14]. Разнообразие программных логик, используемых для спецификации систем, объясняется не-только тем, что разные логики описывают принци- пиально разные свойства моделей, но и различной сложностью проверки на модели каждой из них. Можно, конечно, избрать для спецификации свойств программы наиболее мощную по выразительной силе логику, но это грозит обернуться тем, что она может оказаться неразрешимой или её формулы невозможно проверить на модели. Поэтому так важно исследовать теорети-чески алгоритмические свойства различных логик. Смысл всякой формулы программной логики принято определять но отношению к размеченному графу переходов. Такие структуры называются моделями Крипке.
С помощью динамических логик можно специфицировать свойства систем, выполняющиеся в результате каких-либо действий. Методы проверки на модели спецификаций, определённых в таких логиках, легко сводятся к проверке на модели темпоральных логик или логик с неподвижными точками, поэтому на практике специальные верификаторы для моделей, чьи свой ц ства выражены в динамических логиках, не распространены.
Темпоральные логики позволяют описывать порядок событий во времени без привлечения времени в явном виде. При всём многообразии изученных темпоральных логик, большинство из них содержит оператор вида G , обращающийся в истину в настоящий момент времени, если р всегда истинно в будущем. Чтобы заявить о том, что события е\ и Є2 никогда не могут происходить одновременно, достаточно записать формулу G(—"Єї V —1Є2). Темпоральные логики обычно классифицируются в соответствии с тем, является ли структура времени линейной (например, LTL — Linear Temporal Logic) или ветвящейся (например, CTL — Computational Tree Logic).
С изобретением в начале 80-х гг. Кларком и Эмерсоном алгоритмов проверки на модели для темпоральных логик использование этих логик для анализа поведения распределённых систем удалось автоматизировать. Алгоритм, разработанный Кларком и Эмерсоном для логики ветвящегося времени CTL, имел полиномиальную сложность как относительно размеров модели, определяемой рассматриваемой программой, так и относительно длины её спецификации в темпоральной логике. Позднее Кларк, Эмерсон и Систла предложили улучшенный вариант алгоритма, имеющий линейную сложность относительно произведения длины формулы на размер графа переходов. Ал- горитм был реализован в системе верификации ЕМС, которая была широко распространена и использовалась для проверки ряда сетевых протоколов и последовательных схем. Сначала системы верификации моделей были способны проверять графы переходов, содержащие от 105 до 106 состояний со скоростью около 100 состояний в секунду для типичных формул. Несмотря на такие ограничения, верификаторы были успешно использованы для обнаружения ранее неизвестных ошибок в нескольких опубликованных электронных схемах.
Однако темпоральные логики обладают ограниченной выразительной силой: в этих логиках, например, невозможно выразить существование выигрышной стратегии в классе всех конечных игр, таких как параметризованные шахматы и шашки.
Наиболее мощная пропозициональная программная логика — это -исчисление с неподвижными точками (/ С) [29]. Свойства моделей программных систем, определимые в динамических или темпоральных логиках, легко выразить с помощью /z-исчисления.
Недавно в семейство программных логик добавились эпистемические логики [18], в частности, пропозициональная логика знаний для п агентов PLK„ (Propositional Logic of Knowledge) и пропозициональная логика общих знаний для п агентов PLCn (Prepositional Logic of Common Knowledge). Они позволяют специфицировать такие системы, в которых необходимо проверять утверждения, касающиеся знаний параллельных процессов, которых принято называть агентами. С помощью логик знаний особенно удобно описывать свойства систем, в которых действия распределённых параллельных процесії
Y сов зависят от информации, которой они располагают. К таким программным
системам относятся, например, коммуникационные протоколы [23], особенно в ненадёжной среде, и программы управления роботами, получающими информацию от окружающей среды [16]. Проверка на модели систем, специфицированных эпистемическими логиками, позволяет исследовать в этих си- _ стемах знания, основанные на неполной информации. Иными словами, мож но, меняя доступность той или иной информации, проверять как меняется у агента представление о мире и о других агентах. Например: достаточно ли процессу в системе с разделяемыми ресурсами наблюдать параметр занятости ресурса, чтобы знать, когда он освободится, или необходимо иметь доступ к локальной информации остальных процессов (например, к информации о состоянии вычислений). Примером коммерческих систем проверки на моделях, в спецификациях которых используются логики знаний, могут служить программы компании Time-Rover [54], чьим клиентом является, например, NASA.
Однако особенно полезными оказывается комбинации логик знаний с темпоральными логиками или динамическими логиками действий с неподвижными точками, поскольку они позволяют описывать эволюцию знаний агентов во времени или их изменение и результате каких-либо действий. При рассмотрении временных аспектов знаний возникают системы, различающиеся "разумностью" агентов, действующих в системах. Например, часто рассматриваются забывающие агенты, которые не помнят историю развития coll бытии в системе, а имеют лишь информацию о её текущем состоянии. В противоположность им можно определить агентов с абсолютной памятью, различающих состояния системы, основываясь на запомненных ими истории данных. Кроме того, могут быть синхронные агенты, помнящие, "который час" и асинхронные, не знающие времени. Агенты, чьи знания не зависят от времени, называются обычными агентами.
Подробный обзор состояния теории и практики "классической" проверки моделей программ на конец 1990-х годов можно найти в [10, 50], а теории логик знаний — в [18].
і Обзор смежных результатов
Свойства различных комбинированных логик в системах с разнообразными агентами изучаются в течение последних двадцати лет. Например, в 1986 г. в работе [22] Дж.Хальперном и М.Варди изучена задача разрешимости для комбинаций временных логик LTL и CTL с логиками PLKn и PLCn в (а)синхронных системах как забывающих, так и с абсолютной памятью. В частности, показана полнота задачи в данных классах временной сложности1:
PRS FAS
CTL-C„, п 2 П} ЕХРТШЕ
CTL-Kn, п 2 неэлементарное ЕХРТШЕ
CTL-Ki = CTL-Ci двойная экспонента ЕХРТШЕ
В [33] в 1998 г. Р.ван дер Мейденом доказано, что задача проверки на модели формул PLCn в системах с абсолютной памятью
• PSPACE-nojum для синхронных систем и
• неразрешима для асинхронных системах.
В работе [34] в 1999 г. Р.ван дер Мейденом и Н.В.Шиловым была изучена задача проверки на модели для комбинаций PLKn и PLC„ с LTL в синхронных системах с абсолютной памятью. В статье показано, что проверка на модели для синхронных систем с абсолютной памятью в случае двух агентов
#
• является PSPACE-nomiou для LTL-C2 без UNTIL;
• верхняя и нижняя границы неэлементарны для LTL-K2;
• неразрешима для LTL-Сг.
В статье [34] были предложены древовидные структуры данных для проверки на модели логики линейного времени и знаний с ограниченной глубиной знаний. Эти структуры данных очень удобны для представления эво- Ф люции и обновления знаний. Они являются деревьями, чья высота равна 1PRS — синхронные системы с абсолютной памятью (Perfect Recall Synchronous Systems), FAS — асинхронные забивающие системы (Forgetful Asynchronous Systems)
if максимальной вложенности операторов знаний. В статье [34] продемонстри ровано, что задача проверки на модели для LTL-Kn в синхронной семантике абсолютной памяти может быть сведена к задаче пустоты автоматов Бюхи с входами, являющимися бесконечными последовательностями таких деревьев. Однако перечисленные работы исследуют комбинации только темпораль _ пых логик с логиками знаний. Комбинации же динамической логики с непо движными точками позволяют выразить более широкий спектр свойств муль-тиагентных систем. Например, при проверке на модели свойства существования выигрышной стратегии2, можно узнать какой минимальной информацией должен располагать агент, чтобы выиграть в конечной игре. Алгоритмические свойства именно таких комбинаций и изучаются в диссертации.
С практической точки зрения интересен вопрос: возможна ли автомати- • ческая проверка на модели для LTL-Kn? Некоторый опыт с древовидными структурами данных описан автором диссертации в [47]. В этом эксперимен талыюм исследовании
• входная конечная среда специфицирована в языке Multi Agent System Language;
• входная LTL-Kn формула не должна иметь негативных/позитивных вхождений модальности знаний Ki/Si для любого агента г Є [1..п];
• инструментом проверки на модели стала программа SMV — верификатор формул LTL в моделях с конечным числом состояний [8, 10].
В 2003 году в Австралии под руководством Р.ван дер Мейдена был раз-, работан прототип системы проверки на моделях МСК [53]. С его помощью можно проверить на модели
1. с асинхронными забывающими агентами формулы логик CTL и LTL в
комбинации с логиками знаний PLKn и PLC„;
2. с синхронными забывающими агентами формулы подмножества логики LTL, содержащее единственный оператор X, и подмножества логики
2невыразимое в CTL и LTL
fk CTL, содержащее операторы AX и EX, в комбинации с логикой знаний
PLKn;
3. с синхронными агентами с абсолютной памятью формулы подмножества логики LTL, содержащее единственный оператор X, в комбинации с логикой знаний PLKn.
Отметим, что первый и второй случай можно свести к проверке на модели формул //-исчисления, и только в третьем случае проявляется специфика проверки комбинации логик знаний и времени. Кроме того, переходы между состояниями в моделях тривиальны: позволяется только прибавлять константу к переменной модели, возможно, по условию. Недостатком МСК является то, что используются опять-таки только темпоральные комбинации логик знаний и почти не реализована проверка самых интересных систем, а именно — синхронных с агентами с абсолютной памятью. По результатам теорети-ческих исследований в настоящей диссертации реализован прототип системы проверки на модели более выразительных логик, чем логики в МСК.
Вторая составляющая проверки на модели — алгоритмы проверки выполнимости спецификации — представлена большим разнообразием методов. Особенно важны алгоритмы проверки на модели формул //-исчисления, как наиболее выразительной из пропозициональных программных логик. Однако даже самые эффективные из них экспоненциальны относительно размера формулы [И], поэтому целесообразно рассматривать фрагменты //-исчисле- 6 ния, имеющие полиномиальную сложность проверки на модели. В 1993 г. А.
Эмерсон, С. Джатла и П. Систла впервые изучили фрагмент //-исчисления, который допускает полиномиальную проверку на конечных моделях [15]. В настоящей работе предложен новый фрагмент, несравнимый по выразительной силе с фрагментом Эмерсона-Джатлы-Систлы.
Основной недостаток метода проверки на модели — это "комбинаторный взрыв" в пространстве состояний, который возникает, когда система состоит из компонентов, переходы в которых выполняются параллельно. В таком случае с увеличением количества процессов число глобальных состояний системы возрастает экспоненциально. Эта проблема возникает в системах, состоящих из многих компонентов, взаимодействующих друг с другом, а так же в системах, обладающих структурами данных, способными принимать большое количество значений (примером может служить маршрут передачи данных в логических схемах). В первоначальных реализациях алгоритмов проверки на модели отношения переходов явно представлялись списками смежности, а множества состояний задавались явным перечислением. Для параллельных систем с малым числом процессов количество состояний обычно было сравнительно невелико, и такой подход чаще всего был вполне оправдан, но для больших систем он был явно неприемлем.
Однако в конце 80-х гг. благодаря использованию двоичных разрешающих диаграмм — структур данных для представления булевых функций — размеры систем переходов, допускающих верификацию методом проверки на модели, поразительно возросли. Новые структуры данных позволили компактно представлять системы переходов и быстро осуществлять их преобразования. В 1987 г. К.МакМиллан показал, что, используя, символьное представление графа переходов, можно верифицировать очень сложные системы [31]. Новое символьное представление было основано на упорядоченных двоичных разрешающих диаграммах (OBDD) Бриана [4]. Представление в виде OBDD является канонической формой для булевых формул, обычно существенно более компактной, нежели конъюнктивные и дизъюнктивные нормальные формы. Для манипуляций с OBDD были разработаны эффективные алгоритмы. Применяя первоначальный вариант алгоритма Кларка и Эмерсона проверки на модели для CTL и новое представление графов переходов, можно прове- сти верификацию некоторых систем, содержащих более 1020 состояний. С тех пор многочисленные улучшения, внесённые другими учёными в технологию верификации на основе OBDD, позволили выполнить ряд экспериментов с числом состояний, достигающим 10120. Однако формат представления данных в виде OBDD не всегда оказывается эффективным (известны случаи, когда конъюнктивные нормальные формы являются всё-таки более эффективным представлением данных [32]).
Неявное представление в виде OBDD вполне подходит для моделирования последовательных схем и протоколов, состояния которых кодируются булевскими переменными, но для систем с целочисленными состояниями такое представление оказывается не совсем естественным. В настоящей работе для широкого класса как раз таких программных систем предложен более естественный и эффективный формат представления данных.
Итак, суть символической проверки на модели состоит в том, чтобы проверять свойства моделей не в каждом отдельном состоянии (как в явных алгоритмах), а сразу на множестве состояний, что позволяет при подходящей кодировке множеств состояний проверять очень большие модели. В связи с этим разрабатывались различные представления множеств состояний. Остановимся здесь на представлениях, существенно использующих при кодировании тот факт, что элементами пространства состояний являются целые числа.
В 1994 г. Б. Бугло и П. Волпер предложили периодические множества для представления множеств состояний [2]. В этой работе периодические множества используются только для вычисления множества достижимых состояний так, что они скорее предназначаются для комбинированного символически-явного подхода в проверке на моделях. Модели в [2] это машины с конечным числом состояний, параметризованных неограниченными целыми переменными, и со следующими операциями: присваивание константы, сложение константы с переменной и проверка пусковых линейных неравенств. Основным недостатком такого представления является то, что оно не допускает полностью символической проверки на моделях: вычисленное множество достижимых состояний может оказаться слишком большим для проверки спецификации модели во всех его элементах.
В 1999 г. Т. Бултан, Р. Гербер и В. Пух разработали систему для символической проверки бесконечных моделей, представляя множества состояний формулами арифметики Пресбургера [7]. Они использовали программу Omega Library [52] для символических манипуляций с формулами Пресбургера. Модели, проверяемые с помощью этой системы, также можно описать формулами арифметики Пресбургера. К достоинствам такого способа представления данных относится то, что можно проверять сколь угодно большие и даже бесконечные модели, но недостатком является тот факт, что сложность оперирования формулами Пресбургера вычислительно дорога: она экспоненциально зависит от размера формул. Кроме того, для некоторых бесконечных моделей алгоритм проверки спецификации может не завершаться.
Формат данных, предложенный в настоящей работе, позволяет осуществлять полностью символическую проверку на широком классе моделей, размер данных во много раз меньше размера модели (в отличие от OBDD для этого класса моделей) и алгоритмы манипулирования ими имеют квадратичную сложность относительно размера формулы (в отличии от формул Пресбур-гера).
Цели и основные результаты диссертации
Целями диссертации являются
• теоретическое исследование проблемы проверки моделей для новых, более выразительных, комбинаций логик знаний и действий;
• теоретическое исследование новых эффективных алгоритмов и новых, более эффективных, символических форматов представлений данных для логик действий и логик знаний;
• экспериментальная реализация новой системы проверки моделей для комбинированных логик знаний и действий на моделях.
В рамках этих целей в диссертации исследованы некоторые алгоритмические свойства новых комбинаций пропозициональной логики знаний с пропозициональными динамическими и временными логиками, расширенными неподвижными точками. В мультиагентных системах изучены выразительная сила, проверка на модели и разрешимость для попарных комбинаций пропозициональных логик
(1) элементарной динамической логики (EPDL),
(2) временной логики на деревьях, расширенной действиями (Act-CTL),
(3) //-исчисления (/хС)
(а) логикой знаний для п агентов (PLKn),
Ц (b) логикой общих знаний для п агентов (PLCn).
Акцент сделан на задаче проверки на модели комбинированных логик в следовой семантике. Особо рассмотрены два крайних случая: асинхронные конечные системы с забывающими агентами и синхронные конечные системы с абсолютной памятью. В диссертации обобщены деревья знаний из [34]. Также показана возможность сведения задачи проверки на модели для ло гики Act-CTL-Kn к задаче проверки формул логики Act-CTL в моделях, где состояниями являются деревья знаний. Эти результаты расширяют результаты статьи [34] и тем самым вносят вклад в исследования задач проверки на модели. Ранее они были опубликованы в [38, 39, 40, 42].
Далее, в диссертации описан полиномиальный алгоритм проверки на модели для фрагмента //-исчисления, вычисляющий верхнюю и нижнюю аппроксимацию семантики формулы. Ранее этот алгоритм был опубликован в
» [41].
В диссертации для кодировки множеств состояний и переходов проверяемой модели предлагается использовать новый формат представления данных, а именно: аффинные мноэюсства, векторпо-аффинные множества и, для кодировки моделей, чьими состояниями являются деревья — векторпо-аффинные деревья. Класс моделей, для которых возможна такая кодировка, довольно широк. В него попадают все конечные модели, не допускающие перемножения переменных друг на друга (умножение на константу допустимо). В частности, модели, описывающие шахматы и шашки, входят в данный класс.
По результатам теоретических исследований был выполнен машинный эксперимент: реализована программа Экзаменатор — прототип системы проверки моделей
1. с асинхронными забывающими агентами, специфицированными формула ми //-исчисления в комбинации с логикой знаний PLKn;
2. с синхронными агентами с абсолютной памятью, специфицированными формулами логики CTL, расширенной действиями, в комбинации с логикой знаний PLK„.
«f Все полученные результаты являются новыми. Результаты, касающиеся
теоретических исследований комбинированных логик знаний и действий, а также алгоритма проверки фрагмента формул д-исчисления, получены автором в сотрудничестве с научным руководителем Н.В.Шиловым. Вклад автора состоял в исследовании алгоритмических свойств асинхронных муль- тиагентных систем, адаптации понятий, определений и утверждений, отно сяіцихся к fc-деревьям, для проверки на модели формул комбинированной логики знаний и действий в синхронных системах с абсолютной памятью, а также в доказательстве корректности аиироксимационного алгоритма проверки на модели формул //-исчисления. Теоретическое исследование новых аффинных представлений данных и реализация прототипа инструмента проверки мультиагентных систем выполнены автором полностью самостоятельно. В частности, но сравнению с упоминавшейся выше программой проверки МСК [53], Экзаменатор позволяет проверять более сложные свойства моделей, специфицированные с помощью более мощных логик.
Предполагается, что основные понятия, относящиеся к теории и практике проверки моделей программ, читателю известны.
Оставшаяся часть работы организована следующим образом.
В главе 1 даются определения и результаты, используемые в диссертации: в разд. 1.1 даются определения базовых логик, а разд. 1.2 посвящен поясняющим сквозным примерам.
Все последующие главы содержат только идеи или эскизы доказательств утверждений и теорем диссертации, а полные доказательства вынесены в при ложение А.
В главе 2 рассматриваются алгоритмические проблемы комбинированных логик. В разд.2.1 определяются исследуемые комбинированные логики. Алгоритмические проблемы для комбинированных логик для систем общего вида исследуются в разд.2.2. В разд.2.3 изучаются асинхронные системы с забывающими агентами. В разд.2.4 определяются синхронные системы с абсолютной памятью и показаны их симуляционные возможности. Разд.2.5 посвящен проверке на модели комбинированных логик в этих системах. В разд.2.0 более подробно исследуется задача проверки на модели для формул этих логик с ограниченной глубиной знаний.
В главе 3 обосновывается апироксимационный алгоритм для фрагмента
//-исчисления: в разд.3.1 обсуждается сложность входных параметров задачи проверки на модели для //-исчисления, в разд.3.2 вводится специальная префиксная форма формул //-исчисления, а в разд.3.3 представлен собственно апироксимационный алгоритм.
- В главе 4 предлагается аффинное представление данных. Синтаксис и семантика языка описания класса моделей, для которых возможны аффинные представления, изложены в разд.4.1 и там же приведён пример модели. В разд.4.2 описываются собственно аффинные множества: представление множеств состояний, переходов между ними и операции над множествами. Разд.4.3 посвящен аналогичному описанию векторно-аффинных множеств. В разд.4.4 сравниваются два кодирования данных на примере простой модели — векторно-аффинное представление и BDD-иредставление. В разд.4.5 изложены идеи аффинной проверки на моделях комбинированных логик, в частности, определяются аффинные деревья знаний и манипуляции с ними.
В главе 5 содержится краткое описание прототипа системы проверки на моделях Экзаменатор формул комбинированных логик и небольшого экспериментального теста: задачи об угадывании числа для различных входных параметров.
В заключении перечислены основные результаты и выводы.
Алгоритмические проблемы для комбинированных логик
Допустимые действия агента для перехода между состояниями — это все запросы Ь цщ для непересекающихся L,Rc [1..N + 1] с \L\ = Л, попутно увеличивающие значения счётчика на единицу. Пусть единственная информация, доступная агенту в состоянии (т.о. дающая возможность различать состояния) — это результат взвешивания. Агент должен приобретать знания о номере фальшивой монеты из последовательности, начинающейся в начальном состоянии и состоящей из М запросов и М соответствующих результатов. Комбинация PDL[24] и PLK[18] оказывается вполне естественной для выражения возможности угадывания фальшивой монеты: где все недетерминированные выборы U... пробегают все множества L, R С [1..Лг+1] так, что Lf]R = 0 и \L\ = \R\. Эта формула выражает тот факт, что существует последовательность взвешиваний, такая, что агент будет знать номер фальшивой монеты и при этом длина этой последовательности не больше М, т.е. значения счётчика меньше или равны М.
Для простоты обсуждения зафиксируем значения параметров: N = Ъ и М = 2. В этом случае имеется 240 состояний17 и 140 действий18 (на рис. 1.1 приведены примеры состояний и переходов между ними). Естественно предположить, что агент помнит последовательность сделанных запросов взвешивания и последовательность соответствующих результатов взвешивания, так как он приобретает знания о номере фальшивой монеты из этих последовательностей. Более того, агент не может различить две последовательности состояний тогда и только тогда, когда он совершил одинаковые иоследова телыюсти запросов и прочитал одинаковые результаты вдоль этих последовательностей. Назовём это свойство памяти агента гипотезой синхронной абсолютной памяти. Вообще, гипотеза синхронной абсолютной памяти — это свойство агента помнить последовательность выполняемых действий и последовательность соответствующей различающейся информации для про-, межуточных состояний, и его способность различать последовательности состояний в соответствии со своими "воспоминаниями". Агент знает некоторый факт тогда и только тогда, когда этот факт верен во всех неразличимых ситуациях. Рис. 1.2 иллюстрирует эволюцию и приобретение знаний в предположении синхронной абсолютной памяти.
Хотя задача о монетках является красивым примером выразительных возможностей и естественности комбинированной логики знаний и действий, она, к сожалению, не совсем удобна для иллюстрации деталей проверки на модели формул логики знаний с ограниченной глубиной, аппроксимацион-ного полиномиального алгоритма для //-исчисления и аффинной проверки моделей. Поэтому в качестве чисто иллюстративного примера будем использовать простую задачу угадывания числа, похожую на задачу о монетках в смысле приобретения знаний. Формально задачу можно описать так:
Задумывается натуральное число меньшее N + 1 и большее 0 и стартовое число S. Можно выполнять сложение или вычитание чисел 10, 5 или 1 с числами, начиная со стартового, без выхода за границы отрезка [1..ЛГ]19. Возможно ли угадать это число не более чем за М арифметических действий?
Здесь Лг 1, 0 S N и М 0. Назовём эту задачу GN(N,S,M) (Guess-Number). Агент в этой задаче угадывает число Num, зная, что оно где-то между нулём и iV-f-1. Кроме того, ему известно стартовое число. Вначале он может осуществлять арифметические действия сложения или вычитания со стартовым числом S и числами 10, 5 или 1, а затем повторять эти действия с результатами, и получать информацию о знаке сравнения с задуманным числом. Пусть есть число Store Є [I-.JV]. Действие агента а()П) заключается в складывании числа Store с числом п Є {1,5,10}, имеющим знак Є {+, —}. Информация о результате сложения представлена четырьмя знаками результата: , , = или out, что означает, что результат последнего арифметического действия соответственно меньше, больше, равен задуманному числу или выходит за границы промежутка [1..7V]. Если знак результата out, то число Store не меняется. Как и в задаче о монетках, введём счётчик действий Cnt, принимающий натуральные значения из [0..iV]20 и увеличивающий своё значение на 1 в результате того же действия Я(0,п). В начальном состоянии знак результата равен ini и Cnt = 0.
Итак, агент действует в пространстве [0. JV] х [1..N] х { , , =, out, ini} х [L.iV], где первый множитель — значения счётчика Cnt, второй — накопительная переменная Store, третий множитель — знак результата Sign и последний множитель — задуманное число Num. Допустимые действия агента для перехода между состояниями — это все действия а(0)„) для п Є {1,5,10} и 0 Є {+,—} Информация, доступная агенту в состоянии — это знак результата и, в начальном состоянии — значение стартового числа. Агент может приобрести знания о задуманном числе из последовательности, начинающейся в начальном состоянии и состоящей из М действий и М соответствующих знаков результатов. Формула для угадывания числа аналогична формуле из задачи о монетках: где все недетерминированные выборы U... пробегают все числа п Є {1, 5,10} и знаки действий 0 Є {+, —}.
Зафиксируем значения параметров: Аг = 100, S = 20 и М = 3. В этом случае имеется 5050000 состояний21 и 6 действий (некоторые состояния порождаются действиями, представленными на рис. 1.3). Предполагаем, что агент помнит стартовое число, последовательность арифметических действий и последовательность соответствующих знаков результатов, так как он приобретает знания о задуманном числе из этих последовательностей. Более того, агент не может различить две последовательности состояний тогда и только тогда, когда он совершил одинаковые последовательности арифметических действий и прочитал одинаковые знаки результатов в этих последовательностях, начав с одного и того же стартового числа. Значит, для этой задачи тоже действительна гипотеза синхронной абсолютной памяти. Рис. 1.4 иллюстрирует эволюцию знаний угадывающего агента с абсолютной памятью.
Заметим, что, обладая абсолютной памятью, агент может не только угадать число22, но и определять промежуток, в котором оно находится, с каждым шагом всё уточняя его. Строгое формальное описание синхронной среды с абсолютной памятью для этой задачи приведено в разделе 2.4.
Представление пропозициональных констант и действий
Аффинное представление атомов и их отрицаний выглядит как в таб.4.1. Аффинное представление булевской комбинации Р этих атомов (в виде набора аффинных представлений атомов), соответствующее их несводимой дизъюнкции, можно получить, преобразуя Р к нормальной форме (отрицания есть только у атомов) и применяя затем к атомам следующие операции: конъюнкция (таб.4.2) и дизъюнкция (таб.4.3)3. Полезна также следующая оптимизация: если к = т в (ж, [к, т]), то (х, [к, т]) преобразуется в (к, 0). После всех преобразований аффинное представление пропозициональной константы Р принимает вид набора аффинных представлений атомов:
В процессе символической проверки на модели над пропозициональными константами осуществляются операции конъюнкции, дизъюнкции и вычисление предусловия действий. После этих операций получаются множества, определяемые набором линейных двучленов вида ах-\-Ь с целыми коэффициентами an b на отрезке целых чисел [с .. d\. В дальнейшем такие выражения будем называть атомами, а их наборы — ограниченными аффинными мно-эюествами. Представим атом в виде записи с двумя полями: где cf — это коэффициенты атома и Dom представляет область определения аргумента.
Для атома / = (ах + 6, [тгп,тах]) получим следующее представление: f.cf = (a,b) и f.Dom = [тгп,тах]. В структуре Кринке MA = ([TI..N],IA,CA,VA)I ассоциированной с аффинным представлением, атом / выполняется в состояниях d Є [n..iV] таких, что d = f-cf\ х + /.с/2 при х Є f.Dom, т.е. такие d Є CA{J) Тогда ограниченное аффинное множество Р — это список атомов, и на этом списке определены следующие операции: P.add[atom) (добавить атом к представлению Р), P.remove(atom) (удалить атом из представления Р). Р = Ui(fi) выполняется в тех состояниях структуры МА, В которых выполняются составляющие его атомы, т.е. СА{Р) = UiCU(/i). Представление допустимых атомарных переходов имеет следующий вид: (ах + b), где, как и в представлении пропозициональных констант, а и b — целые, что означает, что переменной присваивается значение этого выражения- при некотором значении переменной х из области определения. Кроме того, необходимо ввести специальный символ all для представления действия all. А = {(Pi, ai),..., (Рт ят)} это аффинное представление допустимых действий, где Pi — аффинное представление пропозиционального условия пуска, а а{ — аффинное представление атомарного перехода (такое представление возможно для действий моделей, описанных на языке VEC в силу утверждения 23).
Эта запись означает недетерминированный выбор из атомарных переходов но условию. Она равносильна следующей программе А на языке PDL [24]: A = (Pi?; а\) U ... U (Рт?; ат). Представим действие А как список условных атомарных переходов CondAct, где: В ассоциированной структуре Крипке MA такое представление условных атомарных переходов а определяет следующие отношения переходов: (х, у) Є Li{) х Е Сл(а.guard) Л у = a.cfi х + а.с/2, если a.cf ф all, иначе (х,у) Є ІА{О) & х Є Сд(а.guard)Лу Є [п..АГ], если a.cf = all. Представление недетерминированного действия A = UjOj определяет отношение переходов такое, что (х,у) Є Li(A) = Заг- Є А : (х, у) Є ІА(Щ) Корректность аффинных представлений пропозициональных констант и действий модели непосредственно следует из их определений и определения семантики языка VEC и утверждения 24: Утверждение 25 Для каэюдой аффинной модели S, описанной па языке VEC, ассоциированная с S структура Крипке Ms — (As, Is, Cs, Vs) совпадает со структурой Крипке MA — {DA,IA,CA,VA), ассоциированной с ее аффинным представлением, т.е. Ds = DA, IS = Li u Cs = С A Пусть Р, Q, R будут ограниченными аффинными множествами, представляющими некоторые множества состояний ассоциированной структуры Крипке, а значит и состояний модели. 1. Объединение: R = Р U Q. Это обычное объединение множеств Р и Q. Этот случай сложнее предыдущего, так как нужно найти общие значения атомов, составляющих множества, для каждого из множеств Р и Q. Пусть P = Fl)CfiiQ = G\JСд, где С/ и Сд — множества констант (т.е. двучленов с нулевым коэффициентом при переменной и пустой областью определения). Пусть Solve(f(x),g(y)) — это процедура, которая находит все решения дио-фантова уравнения f(x) = д{у) в виде аффинных множеств x(z) и y(z), где z — целое, т.е. если z = к, то f(x(k)) = д{у{к)). Эта процедура выполнима за время, логарифмически зависящее от коэффициентов функций f(x) и д(у). Вычисление предусловия действия A = uyLitQitcii) зависит от его контекста в проверяемой формуле //-исчисления, т.е. от того, какая из подформул [А]Р или (А)Р встречается в формуле. Вообще говоря, [А]Р = f)i(Qi — [щ]Р) и (А)Р = \Ji(Qi Л {щ)Р)- Пусть true — это сокращение для пропозициональной константы, истинной во всех состояниях модели, т.е. true = (х, [n..N]), a false — сокращение для пропозициональной константы, всюду ложной: false = (0,0). В силу семантики формул //-исчисления для действия all, детерминированных переходов аг- с ai.cf ф all и пропозициональной константы Р, верно следующее
Аффинная проверка на моделях комбинированных логик
Таким образом, векторно-аффинный лес высоты 1 — это множество Trl(P) = {(v, Ii(v),..., IN(V)) I v Є Р]. Для аффинных векторов Ц(у)(і Є [1-.АГ]) можно вычислить аффинные вектора, неотличимые от них каждым из агентов, т.е. аффинный лес высоты два является набором векторно-аффинных деревьев Tr2(P) = {(v,Trl(h(v)),... ,Trl(IN(v))) I г; Є Р}. Таким образом, рекурсивно можно построить векторно-аффинное дерево любой высоты. Получаем множество деревьев с рёбрами, помеченными агентами, и с вершинами, помеченными аффинными векторами, представляющими множества состояний. Векторно-аффинное дерево является iV-арным деревом высоты к. Векторно-аффинное дерево t кодирует лес обычных деревьев знаний, в корнях которых наблюдаемые каждым агентом неременные пробегают всевозможные множества значений, определяемые их аффинным представлением в корне дерева. Количество деревьев в таком лесу может достигать размера модели, а число вершин в каждом из них может быть неэлементарно, т.е. порядка 22 / .
Например, если все агенты "глупые", т.е. не могут отличить каждое состояние модели от любого другого, то пропозициональная константа true, истинная во всех состояниях порождающей модели М, описывается единственным векторно-аффинным деревом высоты к, каждая вершина которого равна вектору ігием = (Di,...,Dn) и их количество — 5Df=0iV1. Количество обычных деревьев знаний в лесу, описывающем ту же константу, равно размеру модели, причём каждое из них является (N х Л/)-арным деревом, значит, число вершин в каждом из них равно Хл=о(- х 1- Л)г-Представим векторно-аффинное дерево высоты к таким образом: high = к; trec root : vector; agent : [0..N]; trees : array [1..N] of tree; Здесь high — высота дерева, root — аффинный вектор в корне, agent — им помечено ребро, ведущее к дереву, а если оно не поддерево, то agent = О, trees — массив поддеревьев. Получаем, что векторно-аффинный лес зиапий высоты к векторно-аффинного множества Р — это список векторно аффинных деревьев Тгк, с корнями, равными векторам множества Р. На этом списке определены операции добавления P.add и удаления P.remove аффинных деревьев. Пусть ЕА = (А4, л,» A,IA,CAIVA) — среда, ас социированная со векторно-аффинным представлением. В модели на дере вьях TRk(EA) = (DTRk(EA), 1ТПк(ЕА),СТпк(ЕА)), ассоциированной с векпюрпо аффипиым представлением деревьев, Агт? (Ед) — множество всех деревьев высоты не больше к, а аффинное дерево t выполняется в состояниях d Є DTR,,{EA) таких, что d.root Є C t.root), т.е. тогда d Є Стпк(ЕА)(ї)- Заметим, что для среды Es = (As, s,-. SiIsiCs,Vs), ассоциированной с моделью S, и d Є СтлА(Ел)(0 верно также, что d.root Є Cs(t.root) и, следовательно, d Є Ргл (Е5)(0- Это влечёт корректность представления пропозициональных констант. Вычисление предусловий происходит с использованием только векторных аффинных действий порождающей модели и векторных переходов но знани ям, определённым в параграфе 4.5.2 так, что в специальной записи переходов между деревьями нет необходимости. Поэтому 1тик определяется с использованием векторно-аффинных представлений отношений переходов Acts и неразличимости Inds аналогично разделу 2.G.
Корректность векторно-аффинных представлений деревьев пропозициональных констант и действий модели непосредственно следует из их определений, определения семантики языка Agent-VEC: Утверждение 33 Для всякой мулыпиагеитпой синхронной среды S с аген тами с абсолютной памятью, описанной па языке Agent-VEC, ассоциированная с пей модель TRf;(Es) = (DTRk(Es) TRk(Es) TRk(Es)) совпадает с моделью TRk(EА) = (DTRk(EA)JTRk(EA),CTR EA)), ассоциированной с векторно-аффинным представлением ее деревьев, т.е. DTRk(Es) = TRk(EA) lTRk(Es) = hR E TRkiEs) = CTRk{EA) Пусть Р, Q, R будут аффинными лесами высоты к, представляющими некоторые множества состояний модели, причём Р состоит из деревьев tp = (vP, Tn(vp),..., TrN(vP)), a Q — из деревьев g = (vQ, TTI(VQ), ..., Тгл-(г;0)). 1. Объединение: R = PUQ. Это обычное объединение лесов Р и Q. Joint(P, Q): Вход: аффинные леса Р и Q. 1. forall р Є Р R.add(tP); 2. forall Q Є Q R.add(tQ); Выход: аффинный лес R. Корректность этого алгоритма непосредственно следует из определения векторно-аффинных деревьев знаний и операции объединения множеств. 2. Пересечение: R= Р П Q. В пересечении будут содержаться деревья с корнями, являющимися пересечением векторно-аффинных множеств корней, чьи поддеревья также пересекаются, т.е. R — {(и/г,Тгі,... ,Тгдг) VR = tp.root П tQ.root и ТГІ = Tri{tp.root) f)Tri(tQ.root)(i Є [1..Л7"]), где tp Є Р и tQ Q}. Пересечение кор--ней деревьев, являющихся аффинными векторами, вычисляется алгоритмом из раздела 4.3.2, а пересечение поддеревьев определяется рекурсивно.
Представление пропозициональных констант и действий
На сегодняшний день в области создания систем передачи и обработки данных сложилась диспропорция темпов развития трёх её основных компонентов: микропроцессорной техники, средств телекоммуникации и разработки программного обеспечения. Согласно закономерности, замеченной основателем компании Intel Гордоном Муром, быстродействие микропроцессоров удваивается без изменения их стоимости каждые 18 месяцев, пропускная спо-собность каналов передачи данных растёт на 75 % кажділе 12 месяцев, и лишь в индустрии программного обеспечения скорость разработки программных систем растёт всего на 4-5 % в год. Это приводит к тому, что разрыв между техническими возможностями и технологиями обработки и передачи информации всё время увеличивается.
В значительной степени, это происходит из-за отсутствия удовлетворительного для промышленности решения проблемы проверки правильности программных систем и логических схем вычислительных устройств. Например, из практики разработки программного обеспечения хорошо известно, что примерно 2/3 времени, затрачиваемого на создание системы, приходится на отладку, т.е. проверку её правильности. При создании алгоритма и выборе системы программирования можно руководствоваться многочисленны- ми пособиями, справочниками и пр. Проверка синтаксической правильности. программы и её трансляция в исполняемый машинный код осуществляется полностью автоматически. Но этан отладки программ, т.е. проверка семантической правильности, до сих пор плохо автоматизирован. Воспользуемся образным сравнением из [50]:
Средства отладки программы, которые входят в состав всякой развитой системы программирования, могут помочь разработчику в той же мере, в какой лопата оказывает помощь кладоискателю. Главные вопросы — где копать и стоит ли копать вообще? Здесь скорее пригодилось бы устройство наподобие металлоис-кателя. Но хороший металлоискатель — это тонкий инструмент, требующий знания его устройства и умелого обращения. Так, что кроме лопаты неплохо бы использовать и автоматические системы поиска ошибок и проверки правильности функционирования программ и вычислительной аппаратуры.
Как правило, большинством разработчиков программных систем для проверки правильности проекта практикуются старые добрые методы имитационного моделирования и тестирования. Они довольно эффективны на самых ранних стадиях отладки, когда проектируемая система всё ещё изобилует ошибками, но результативность этих методов быстро снижается, как только система становится чище.
Достойной альтернативой имитационному моделированию и тестированию являются методы формальной верификации. При имитационном моделировании и тестировании исследуются только некоторые из возможных сценариев поведения проектируемой системы, поэтому остаётся открытым вопрос о том, не содержится ли фатальная ошибка в незадействованных траекториях. Формальная верификация же обеспечивает исчерпывающий анализ всех возможных вариантов поведения системы.
В настоящее время во многих критических приложениях, где любой отказ считается недопустимым, таких как системы управления воздушным и дорожным движением, медицинская аппаратура, электронная коммерция, сети телефонных коммутаторов широко используются аппаратные и программные системы. Поэтому ещё более насущной задачей становится разработка эффек тивных методов, способствующих повышению нашей уверенности в правильности работы программных систем.
Во многих таких системах естественно возникает понятие знания в силу связи между знанием и действием. Что робот должен знать, чтобы открыть сейф, и откуда он знает, достаточно ли он знает, чтобы открыть его? Перед пересылкой очередного сообщения, знает ли отправитель, что получатель получил предыдущее? В какой момент экономический агент знает уже достаточно, чтобы остановить сбор информации и принять решение? Когда база данных может ответить на вопрос "Я не знаю"? Поэтому часто бывает, что правильность функционирования программной системы зависит от "знаний" её компонентов.
В настоящей работе изучаются с теоретической и экспериментальной точки зрения некоторые новые эффективные формализмы для повышения на дёжности программных систем. Особенность подхода состоит в использова нии эпистемических логик — логик знаний — для описания поведения моделей программ.
Техника верификации, получившая название проверки па модели, является
одним из наиболее перспективных и широко используемых подходов к реше нию проблемы автоматизации отладки и проверки правильности программ.
Она была разработана в 80-х гг. Кларком и Эмерсоном в США, а также независимо Квайлом и Сифакисом во Франции. Суть проверки на модели проста, и её этапы можно описать следующим образом:
Моделирование Для проектируемой системы необходимо построить её аб страктную модель (например, конечную систему переходов), приемлемую для инструментальных средств верификации моделей программы. Как правило, это просто задача компиляции и, возможно (при ограничешш по времени и объёму памяти), абстракции, чтобы избавиться от несущественных деталей.
Спецификация Эта задача состоит в формулировании свойств, которыми должна обладать проектируемая система. Обычно спецификации задаются на языке формальной логики. Для аппаратуры и программного обеспечения, как правило, применяют динамические логики, временные логики и их варианты с неподвижными точками. Важным вопросом является полнота спецификации. Метод проверки на модели даёт возможность убедиться, что модель проектируемой системы соответствует заданной спецификации, однако определить, охватывает ли заданная спецификация все свойства, которыми должна обладать система, невозможно.
Верификация Результатом вычислений алгоритма глобальной проверки на модели является множество состояний модели, в которых спецификация выполняется, а алгоритм локальной проверки на модели либо завершает работу с ответом true, означающим, что модель удовлетворяет спецификации, либо строит в качестве контрпримера некоторое вычисление (ошибочную трассу), которое показывает, почему формула не выполняется. Контрпример особенно важен для поиска тонких ошибок в сложных системах переходов. Его анализ может повлечь за собой модификацию системы и повторное применение алгоритма проверки на модели.
Процедура проверки на модели может быть реализована достаточно эффективным алгоритмом, способным работать на вычислительных машинах невысокого класса (но обычно всё-таки не на стандартных персональных компьютерах).
