ПРОБЛЕМНО-ОРИЕНТИРОВАННАЯ
ПРОВЕРКА МОДЕЛЕЙ

В Новосибирском научном центре СО РАН сосредоточены институты-"гиганты" (ИЯФ, ОИГГМ и т.д.), просто большие или средние, но среди них есть и "малыши". Один из таких небольших научных коллективов — Институт систем информатики им. А.П.Ершова. В числе основных его направлений — исследования по верификации распределенных систем. В данном случае рассказывается только об одном подходе к проблеме, который получил название "проблемно ориентированная проверка моделей".

Н.Шилов
кандидат физико-математических наук, ИСИ СО РАН

"Компьютерная наука занимается изучением вычислительных машин не более чем астрономия занимается изучением телескопов". Э.Дейкстра.

Трудная задача

Однажды, во время подготовки задач школьной олимпиады по математике, для обсуждения была предложена трудная головоломка. Никто из членов жюри не смог решить ее сразу, поэтому головоломку не включили в список задач.

Вот она: "Дано 15 монет, из них одна — фальшивая, которую можно отличить только по весу. Кроме того, есть одна гирька, равная по весу настоящей монете. Возможно ли найти фальшивую монету за три взвешивания на чашечных весах?". Среди членов этого жюри был программист-торетик. Для себя он наметил два подхода к решению головоломки: человеко-ориентированный и машинно-ориентированный. Человеко-ориентированный подход был задуман очень просто: теоретик предложил эту головоломку студентам. А вот машинно-ориентированный подход был не столь прост.

Теоретик сделал важное наблюдение: поиск монеты можно промоделировать игрой двух партнеров, где один пытается найти фальшивую монету, а другой — осуществляет взвешивание монет. Игра заканчивается, как только фальшивая монета найдена. Стратегия — это правила ходов игроков, цель которых — как можно быстрее завершить игру. Раунд — это пара последовательных ходов партнеров в игре. Тогда олимпиадную головоломку можно переформулировать так: существует ли в игровой модели стратегия из трех раундов?

Игровая модель понравилась теоретику, так как ее легко запрограммировать. Но еще необходимо было разобраться, как выразить понятие выигрышной стратегии так, чтобы это было понятно компьютеру. Вот тут-то и пришла на помощь современная компьютерная наука. В ней, во-первых, есть языки программирования, которые описывают преобразования данных. А во-вторых, есть языки спецификаций, которые описывают свойства данных и преобразований. Примеры языков программирования известны многим, начиная со школы: это Бэйсик, Си, Паскаль и т.п. А вот примеры языков спецификаций известны только "широкому кругу узких специалистов". Но программист-теоретик использовал один из них для машинно-ориентированного решения. А именно: понятие выигрышной стратегии было сформулировано на языке Пропозициональной Динамической Логики (ПДЛ).

Проверка значений данных в модели, которые удовлетворяют спецификации, называется проверкой модели. Первыми поняли значение методов проверки моделей зарубежные исследователи Э.Кларк, А.Эмерсон и Дж.Сифакис. Произошло это в начале 1980-х годов. Может быть, самая популярная реализация метода проверки моделей — это пакет программ SMV, созданный американским ученым К.Макмилланом.

И теперь уже все готово для машинно-ориентированного решения олимпиадной головоломки: игровая модель, ПДЛ-спецификация существования выигрышной стратегии и пакет проверки моделей SMV. Однако программист-теоретик пошел другим путем. Он использовал методику, созданную вместе с коллегами для исследований по проверке свойств моделей распределенных систем.

Распределенные системы

Что такое распределенная система? Это несколько устройств, обменивающихся сообщениями друг с другом. Например, распределенную систему образуют два компьютера, один из которых (клиент) посылает запросы на выполнения определенных действий, а второй (сервер) — сообщает о результатах этих действий. Глобальная распределенная система интернет объединяет миллионы компьютеров-серверов и компьютеров-клиентов. Распределенная система может включать и живых людей. Поэтому лучше говорить не об устройствах, а о взаимодействующих агентах. В современном мире надежность распределенных систем становиться критическим моментом стабильности. Например, если правила обмена сообщениями между клиентами-покупателями и сервером e-магазина не обеспечивает секретности банковских pin-кодов, то это может привести к банкротству и покупателей, и e-магазина.

Осознавая значение распределенных систем, Международный телекоммуникационный союз ITU (International Telecommunication Union) в 1976-2000 гг. разработал специальный язык SDL (Specification and Design Language) для проектирования распределенных систем. Он имеет математически точные правила, которые позволяют реализовать все его конструкции на современных языках программирования. Эти правила называются операционной семантикой. Но плата за силу языка — сложность операционной семантики. Только описание ее занимает более 500 страниц. Серьезный недостаток SDL — отсутствие средств описания свойств. В результате получается, что у нас есть возможность спроектировать на этом языке систему покупки товаров через интернет, но нет возможности специфицировать свойство, что обмен сообщениями между покупателями и e-магазином обеспечивает тайну банковских pin-кодов.

Особенности сибирской науки

Теперь немного истории. В 1980-е годы Советский Союз приступил к созданию национальной телекоммуникационной сети нового поколения. В проекте предполагалось использовать язык SDL на всех этапах разработки. Для этого были нужны новые машинно-ориентированные методы анализа свойств распределенных систем. Группа сотрудников Института систем информатики (ИСИ) Сибирского отделения Российской академии наук пришла к выводу, что самое перспективное — проверять свойства на моделях.

После нескольких лет поисков сотрудники ИСИ представили в 1992 г. научной общественности язык REAL. Он состоит из двух равноправных частей: исполняемых спецификаций и логических спецификаций. Исполняемые спецификации очень близки к языку SDL и служат для создания моделей распределенных систем. А логические спецификации — это вариант пропозициональной динамической логики (ПДЛ) и служат для спецификации свойств моделей. К 1994 г. была разработана операционная семантика REAL. Отличительная особенность этой семантики — краткость. Достаточно сказать, что описание всей семантики занимает всего 25 страниц. (Сравните с сотнями страниц семантики SDL.)

Для проверки свойств моделей распределенных систем на помощь пришла "старая" идея классифицировать те свойства, которые чаще всего возникают на практике. Еще в 1980-х годах зарубежные ученые М.Чанди и Дж.Мишра, З.Манна и А.Пнуели заметили, что многие свойства распределенных систем, могут быть отнесены к четырем классам. Для этих классов они разработали простые шаблоны (схемы) для конструирования эскизов доказательств, которые сводят доказательство свойств из этих классов к доказательству большого числа свойств, выразимых в самых простых терминах пропозициональной динамической логики. Эскизы доказательств легко могут быть сконструированы вручную одновременно с эскизным проектом распределенной системы. А вот доказательство свойств, выраженных на языке ПДЛ, может оказаться непростым делом, так как они могут использовать очень емкие понятия.

"Новая" идея ученых из ИСИ состояла в том, что свойства, которые возникают после применения шаблонов доказательств, надо проверять при помощи простого метода проверки моделей для самых простых формул ПДЛ. Так как этот подход использует классификацию на классы проблем и метод проверки моделей, то за ним закрепилось название "проблемно-ориентированной методики проверки моделей". Эту методику можно считать основным результатом исследований 1996-2000 гг. по проверке свойств моделей распределенных систем на языке REAL.

Методика была опробована на примерах реальных распределенных систем. В частности, именно она была использована программистом-теоретиком для машинно-ориентированного решения олимпиадной головоломки. Но самый популярный пример — это пример, в котором пассажир покупает железнодорожный билет в кассе-автомате. Свойство системы "касса-пассажир", которое нужно проверить, состоит в следующем: при соблюдении правил покупки касса выдаст билет пассажиру до нужной ему станции.

Ошибки, которые были обнаружены и исправлены в результате применения проблемно-ориентированной методики проверки этого свойства на моделях системы, были двух сортов: отсутствовала "чистка мусора" и не соблюдались временные ограничения. Пример "чистки мусора": после обслуживания пассажира касса должна аннулировать все сигналы от случайно нажатых клавиш. Пример временных ограничений: после приема очередной монеты, касса должна высветить остаток суммы на индикаторе быстрее, чем пассажир успеет еще раз взглянуть на индикатор и опустить лишнюю монету.

Кстати, у настоящей российской кассы-автомата на клавиатуре есть три "магические" клавиши "П", "Д" и "Л" — "ПДЛ". Но пропозициональная динамическая логика тут не при чем. Смысл этих клавиш — это три вида тарифов, принятые на российской железной дороге: "Полный", "Детский" и "Льготный". Как говаривал Козьма Прутков: "Если на клетке слона написано "Буйвол" — не верь глазам своим"...

стр. 10