УСКОРЕННЫЙ  СПОСОБ  ФОРМИРОВАНИЯ  КОМПОЗИЦИИ  СТРУКТУР  КРИПКЕ

Чистяков  Геннадий  Андреевич

аспирант,  Вятский  государственный  университет,  г.  Киров

E-mail: 

Мельцов  Василий  Юрьевич

канд.  техн.  наук,  доцент,  Вятский  государственный  университет,  г.  Киров

E-mail: 

ACCELERATED  METHOD  FOR  FORMING  COMPOSITION  OF  KRIPKE  STRUCTURES

Chistyakov  Gennadiy  A.

postgraduate,  Vyatka  State  University,  Kirov

Meltsov  Vasiliy  Yu.

candidate  of  technical  sciences,  assistant  professor,  Vyatka  State  University,  Kirov

АННОТАЦИЯ

В  работе  предлагается  эффективный  способ  построения  модели  параллельного  алгоритма  путем  объединения  моделей  одиночных  процессов.  Отличительной  особенностью  способа  является  высокий  уровень  параллелизма:  применение  модифицированной  каскадной  схемы  вычислений  и  выявленных  точек  распараллеливания  позволяет  значительно  понизить  асимптотическую  оценку  его  временной  сложности.  Способ  может  быть  использован  при  разработке  программных  комплексов  для  верификации  алгоритмов,  программ  или  аппаратных  систем  посредством  техники  проверки  моделей.

ABSTRACT

This  paper  proposes  an  effective  way  to  build  a  model  of  the  parallel  algorithm  by  combining  models  of  single  processes.  A  distinctive  feature  of  the  method  is  the  high  level  of  parallelism:  application  of  the  modified  cascade  circuit  and  identified  points  of  parallelization  can  significantly  reduce  the  asymptotic  time  estimate.  The  method  can  be  used  in  the  development  of  program  complexes  for  verification  of  algorithms,  software  or  hardware  systems  with  model  checking  techniques.

Ключевые  слова:  верификация;  проверка  моделей,  структура  Крипке.

Keywords:  verification,  model  checking,  Kripke  structure.

В  связи  с  постоянно  возрастающей  сложностью  компьютерных  управляющих  систем  последние  десятилетия  активно  развивается  альтернативный  обычному  тестированию  подход  к  проверке  корректности  алгоритмов  и  программ  —  формальная  верификация.  Одним  из  наиболее  перспективных  направлений  данного  подхода  является  техника  проверки  моделей  или  model  checking.

В  отличие  от  тестирования,  которое,  как  правило,  в  полном  объеме  проводится  над  уже  готовым  программным  продуктом,  методология  проверки  моделей  позволяет  выявить  практически  все  ошибки  функционирования  системы  уже  на  самых  ранних  этапах  проектирования  [2,  с.  5].  Данный  факт  особенно  важен  при  разработке  параллельных  алгоритмов,  к  надежности  которых  часто  предъявляются  повышенные  требования.  Методология  предполагается  выполнение  трех  этапов:  построение  модели  объекта  верификации,  спецификацию  требований,  предъявляемых  к  алгоритму,  и  проверку  соответствия  модели  этим  требованиям  [1,  с.  28].

Существенной  особенностью  техники  model  checking  является  возможность  практически  полной  автоматизации  процесса  верификации.  В  противоположность  прочим  формальным  методам  (проверка  эквивалентности,  дедуктивная  верификация  и  т.  д.),  требующим  значительного  участия  человека-эксперта,  такой  результат  достигается  за  счет  унификации  процесса  анализ.  К  негативным  следствиям  подхода  следует  отнести  значительное  увеличение  размеров  решаемой  задачи,  и,  соответственно,  общего  времени,  затрачиваемого  на  верификацию  [5,  c.  62]  Другими  словами,  все  формальные  методы  балансируют  между  степенью  зависимости  от  эксперта  (препятствие  для  автоматизации;  данные  могут  быть  представлены  максимально  компактно)  и  вычислительной  сложностью  (можно  автоматизировать;  большой  объем  данных).  Model  checking  позволяет  исключить  (в  некоторых  случаях  —  свести  к  минимуму)  участие  человека  в  процессе  верификации. 

Вследствие  вышесказанного,  основными  требованиями  к  применяемым  в  методе  проверки  моделей  структурам  данных  выступают  регулярность,  универсальность  и  простота,  возможно,  в  ущерб  размерам.  В  наибольшей  степени  отвечающим  данным  условиям  способом  представления  объекта  верификации  является  модель  Крипке  —  абстрактная  структура,  включающая  совокупность  множества  состояний  системы  и  переходов  между  этими  состояниями  [4,  с.  148].  Фактически,  данную  структуру  можно  считать  расширением  конечного  автомата,  в  котором  отсутствуют  пометки  на  переходах,  поскольку  основной  целью  является  описание  конечным  образом  бесконечных  последовательностей  состояний  (т.  е.  вычислений)  при  произвольных  входах.  Таким  образом,  причины  переходов  —  конкретные  внешние  события,  существенные  в  модели  конечного  автомата,  —  не  требуют  рассмотрения.  Теоретически  такие  события  могут  быть  учтены,  но  при  верификации  чаще  всего  важно  проверить,  существует  ли  некорректное  поведение  алгоритма  при  любых  последовательностях  внешних  событий.  И  только  когда  такое  поведение  найдено,  можно  искать  его  причину  [1,  с.  72].

Формально  структура  Крипке  может  быть  определена  как  пятерка 

  [1,  с.  70],

где: S —  конечное  непустое  множество  состояний;

—  непустое  множество  начальных  состояний;

  —  тотальное  отношение  на S ,  т.  е.  множество  переходов,  удовлетворяющих  требованию:    (из  любого  состояния  есть  переход);

·      —  конечное  множество  атомарных  предикатов;

·       —  функция  пометок  (каждому  состоянию  отображения    сопоставляет  множество  истинных  в  нем  атомарных  предикатов).

Подмножество  атомарных  предикатов,  принимающих  истинное  значение  в  некотором  состоянии,  можно  считать  символом,  помечающим  это  состояние  структуры  Крипке,  и  сигнализирующим  о  факте  выполнения  в  нем  определенных  условий.

Построение  структуры  Крипке,  эквивалентной  анализируемому  параллельному  алгоритму,  требует  выполнения  следующих  действий.

·Выделить  множество  существенных  для  процесса  верификации  свойств  анализируемого  алгоритма.

·Для  каждого  процесса  алгоритма  необходимо  сформировать  собственную  модель,  т.  е.  соответствующую  структуру  Крипке.

·Определить  правила  получения  новых  атомарных  предикатов  из  комбинации  существующих.

·Сформировать  модель  параллельного  алгоритма  путем  асинхронной  композиции  структур  Крипке  отдельных  процессов,  принимая  во  внимание  возможность  появления  новых  атомарных  предикатов  при  определенной  комбинации  существующих.

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

1.  Принять  за  результирующую  систему  переходов  граф  структуры  Крипке,  эквивалентной  начальному  процессу  алгоритма.  Считать  начальный  процесс  обработанным.

2.  Если  обработаны  не  все  процессы  алгоритма,  то  выбрать  произвольным  образом  модель  еще  необработанного  процесса  и  перейти  к  пункту  3.  Иначе  перейти  к  пункту  7.

3.  Инициализировать  пустую  временную  структуру.

4.  Поочередно  рассмотреть  все  возможные  пары  (декартово  произведение)  состояний  из  результирующей  системы  переходов  и  системы  переходов  выбранной  модели.  Если  композиция  этих  состояний  может  быть  достигнута  в  ходе  выполнения  алгоритма,  то  добавить  данное  состояние  во  временную  структуру.

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

6.  Сопоставить  результирующей  системе  переходов  временную  структуру.  Считать  выбранный  процесс  обработанным.  Перейти  к  пункту  2.

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

8.  Преобразовать  неотмеченную  систему  переходов  в  структуру  Крипке.  Для  этого  сопоставить  состоянию  системы

·     элементы  из  соответствующего  множества  атомарных  предикатов,  исключая  дублирующие;

·     элементы,  получаемые  в  результате  применения  к  соответствующему  множеству  атомарных  предикатов  правил,  используемых  для  образования  новых  предикатов  из  комбинации  существующих.

9.  Получена  композиция  моделей  одиночных  процессов  —  структура  Крипке,  эквивалентная  объекту  верификации.  Алгоритм  завершен.

Следует  заметить,  что  условие  достижимости  композиции  состояний,  используемое  на  шаге  4  алгоритма,  связано  с  анализом  особенностей  взаимодействия  отдельных  процессов.  Так,  например,  не  достижимыми  будут  являться  композиции  состояний,  невозможные  вследствие  блокирования  потоков  управления  из-за  ограничений  примитивов  синхронизации.  Структура  подобного  анализа  в  значительной  степени  зависит  от  языка  описания  алгоритма.  В  связи  с  этим  извлечение  информации  о  взаимодействии  процессов  следует  производить  на  этапе  обработки  команд  отдельных  процессов,  а  для  эффективного  хранения  и  использования  полученных  сведений  целесообразно  оперировать  специализированными  структурами  данных.

Асимптотическая  оценка  предлагаемого  алгоритма  может  быть  определена  следующим  образом.  Пусть  верифицируемый  алгоритм  содержит n  процессов,  каждый  из  которых  состоит  из  a_i  команд.  Обозначим  через    число  состояний  получаемой  структуры  Крипке  в  худшем  случае  (достижимы  все  композиции  состояний).  Для  хранения  информации  о  взаимодействии  процессов  воспользуемся  любой  достаточно  быстрой  древовидной  структурной  данных,  позволяющей  выполнять  операции  поиска,  удаления  и  добавления  за  логарифмическое  время  (АВЛ-дерево,  красно-черное  дерево  и  т.  д.).  Тогда  верхняя  асимптотическая  оценка  предлагаемого  алгоритма  составит —  число  объектов,  способных  повлиять  на  достижимость  композиции  состояний  (процессы,  переменные  в  общей  памяти  и  т.  д.).  Множитель    обусловлен  необходимостью  проверки  наличия  конфликта  добавляемой  композиции  состояний  по  каждому  из    объектов  внутри  каждого  из    процессов.

Предлагаемый  алгоритм  характеризуется  высокой  степенью  параллелизма.  Во-первых,  обработка  моделей  процессов  может  выполняться  с  применением  модифицированной  каскадной  схемы.  Во-вторых,  для  определения  достижимости  одной  композиции  состояний  не  требуется  информация  о  достижимости  других  композиций.  Поэтому  выполнение  шага  4  алгоритма  может  быть  разнесено  на  несколько  процессоров,  что  позволит  снизить  асимптотическую  оценку  до  функции   —  число  используемых  процессоров.  При  этом  следует  соблюдать  ограничение  —  номер  обрабатываемого  процесса.  Иными  словами,  максимальное  количество  задействованных  процессоров  определяется  числом  состояний  в  объединяемых  на  каждом  шаге  структурах. 

Вследствие  высокого  уровня  параллелизма,  предлагаемый  алгоритм  может  быть  эффективно  реализован  на  многопроцессорных  (многоядерных)  системах.  Применение  рассмотренного  ускоренного  способа  формирования  композиции  структур  Крипке  позволит  значительно  сократить  время,  требуемое  для  построения  модели  верифицируемого  алгоритма  или  программы.  Способ  нашел  применение  в  программном  комплексе  для  верификации  параллельных  алгоритмов  с  помощью  методов  логического  вывода  [3,  с.  44—46].

Список  литературы:

1.Карпов  Ю.Г.  MODEL  CHECKING.  Верификация  параллельных  и  распределенных  программных  систем.  СПб.:  БХВ-Петербург,  2010.  —  560  с.

2.Кларк  Э.,  Грамберг  О.,  Пелед  Д.  Верификация  моделей  программ.  Model  Checking.  М.:  МЦНМО,  2002.  —  416  с.

3.Мельцов  В.Ю.,  Чистяков  Г.А.  Структура  системы  верификации  параллельных  алгоритмов  на  основе  методов  логического  вывода  /  Вят.  гос.  ун-т.  Киров,  2012.  —  55  с.  —  Деп.  в  ВИНИТИ  РАН  12.11.2012,  №  412-В2012

4.Baier  C,  Katoen  J.-P.  Principles  of  Model  Checking.  Cambridge:  The  MIT  Press,  2008.  —  994  p.

5.Estivill-Castro  V.,  Rosenblueth  D.A.  Model  checking  of  transition-labeled  finite-state  machines  //  Int.Conf.on  Advanced  Software  Eng.  and  Its  Applications,  Held  as  Part  of  the  3rd  Int.Mega-Conf.on  Future-Generation  Inform.Tech.FGIT  (Jeju  Island,  South  Korea;  8=10  December,  2011).  South  Korea,  2011.  —  pp.  61—73.