Обзор современных систем и методов верификации формальных моделей

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

Повний опис

Збережено в:

Бібліографічні деталі
Дата:	2012
Автори:	Колчин, А.В., Летичевский, А.А., Потиенко, С.В., Песчаненко, В.С.
Мова:	Russian
Опубліковано:	Інститут програмних систем НАН України 2012
Назва видання:	Проблеми програмування
Теми:	Формальні методи розробки програмного забезпечення
Онлайн доступ:	http://dspace.nbuv.gov.ua/handle/123456789/86641
Теги:	Додати тег Немає тегів, Будьте першим, хто поставить тег для цього запису!
Назва журналу:	Digital Library of Periodicals of National Academy of Sciences of Ukraine
Цитувати:	Обзор современных систем и методов верификации формальных моделей / А.В. Колчин, А.А. Летичевский, С.В. Потиенко, В.С. Песчаненко // Проблеми програмування. — 2012. — № 4. — С. 75-88. — Бібліогр.: 74 назв. — рос.

Репозитарії

Digital Library of Periodicals of National Academy of Sciences of Ukraine

id	irk-123456789-86641
record_format	dspace
spelling	irk-123456789-866412015-09-25T03:01:56Z Обзор современных систем и методов верификации формальных моделей Колчин, А.В. Летичевский, А.А. Потиенко, С.В. Песчаненко, В.С. Формальні методи розробки програмного забезпечення Приведен обзор автоматических методов проверки правильности формальных моделей программных систем. Рассмотрены проверяемые свойства, методы редукции и современные инструментальные средства проверки моделей. 2012 Обзор современных систем и методов верификации формальных моделей / А.В. Колчин, А.А. Летичевский, С.В. Потиенко, В.С. Песчаненко // Проблеми програмування. — 2012. — № 4. — С. 75-88. — Бібліогр.: 74 назв. — рос. 1727-4907 http://dspace.nbuv.gov.ua/handle/123456789/86641 519.686 ru Проблеми програмування Інститут програмних систем НАН України
institution	Digital Library of Periodicals of National Academy of Sciences of Ukraine
collection	DSpace DC
language	Russian
topic	Формальні методи розробки програмного забезпечення Формальні методи розробки програмного забезпечення
spellingShingle	Формальні методи розробки програмного забезпечення Формальні методи розробки програмного забезпечення Колчин, А.В. Летичевский, А.А. Потиенко, С.В. Песчаненко, В.С. Обзор современных систем и методов верификации формальных моделей Проблеми програмування
description	Приведен обзор автоматических методов проверки правильности формальных моделей программных систем. Рассмотрены проверяемые свойства, методы редукции и современные инструментальные средства проверки моделей.
author	Колчин, А.В. Летичевский, А.А. Потиенко, С.В. Песчаненко, В.С.
author_facet	Колчин, А.В. Летичевский, А.А. Потиенко, С.В. Песчаненко, В.С.
author_sort	Колчин, А.В.
title	Обзор современных систем и методов верификации формальных моделей
title_short	Обзор современных систем и методов верификации формальных моделей
title_full	Обзор современных систем и методов верификации формальных моделей
title_fullStr	Обзор современных систем и методов верификации формальных моделей
title_full_unstemmed	Обзор современных систем и методов верификации формальных моделей
title_sort	обзор современных систем и методов верификации формальных моделей
publisher	Інститут програмних систем НАН України
publishDate	2012
topic_facet	Формальні методи розробки програмного забезпечення
url	http://dspace.nbuv.gov.ua/handle/123456789/86641
citation_txt	Обзор современных систем и методов верификации формальных моделей / А.В. Колчин, А.А. Летичевский, С.В. Потиенко, В.С. Песчаненко // Проблеми програмування. — 2012. — № 4. — С. 75-88. — Бібліогр.: 74 назв. — рос.
series	Проблеми програмування
work_keys_str_mv	AT kolčinav obzorsovremennyhsistemimetodovverifikaciiformalʹnyhmodelej AT letičevskijaa obzorsovremennyhsistemimetodovverifikaciiformalʹnyhmodelej AT potienkosv obzorsovremennyhsistemimetodovverifikaciiformalʹnyhmodelej AT pesčanenkovs obzorsovremennyhsistemimetodovverifikaciiformalʹnyhmodelej
first_indexed	2025-07-06T14:08:13Z
last_indexed	2025-07-06T14:08:13Z
_version_	1836906862237188096
fulltext	Формальні методи розробки програмного забезпечення © А.В. Колчин, А.А. Летичевский, С.В. Потиенко, В.С. Песчаненко, 2012 ISSN 1727-4907. Проблеми програмування. 2012. № 4 75 УДК 519.686 А.В. Колчин, А.А. Летичевский, С.В. Потиенко, В.С. Песчаненко ОБЗОР СОВРЕМЕННЫХ СИСТЕМ И МЕТОДОВ ВЕРИФИКАЦИИ ФОРМАЛЬНЫХ МОДЕЛЕЙ Приведен обзор автоматических методов проверки правильности формальных моделей программных систем. Рассмотрены проверяемые свойства, методы редукции и современные инструментальные сред- ства проверки моделей. Введение Потребности современной про- мышленности провоцируют рост сложно- сти программных систем. Параллельность (возможность одновременных переходов в нескольких подпроцессах) и асинхрон- ность (отсутствие ограничений на относи- тельную длительность осуществления пе- реходов, зависящую от многочисленных неконтролируемых факторов) являются естественными чертами практически всех программных комплексов, при этом мно- гие исследователи считают их самыми сложными и запутанными (в смысле числа различных типов составляющих) созда- ниями человека [1]. Методы тестирования не обеспечивают исчерпывающего анализа всех возможных вариантов поведения сис- тем, тем самым, не могут гарантировать отсутствие нарушения свойств, которыми должны обладать разрабатываемые систе- мы. Промышленность затрачивает 40–75% трудовых ресурсов на тестирование и ва- лидацию [2, 3]; доля дефектов в требова- ниях составляет 40–50% обнаруженных на стадии тестирования [4]. При разработке систем со сложной моделью поведения становится невозможным обходиться без автоматизации проверки правильности – верификации. Верификацией называется проверка свойств формального описания модели. В качестве математических объектов моде- лирования систем часто используются транзиционные системы, сети Петри, ко- нечные, временные и гибридные автоматы, алгебра процессов и др. В качестве приме- ров проверяемых свойств можно назвать свойства живости, безопасности, полноты и непротиворечивости. В работе Хоара сформулирована [5] наиболее грандиозная задача верификации программ, известная как «Grand challenge» – создание верифи- цирующего компилятора. Различают два основных подхода к формальной верифи- кации: логический вывод (logical inference) и проверка моделей (model checking). Логический вывод базируется на технике доказательства теорем. Для дока- зательства правильности программ приме- няются аксиоматические подходы, напри- мер методы Хоара [6] и Флойда [7]. Обыч- но они автоматизированы частично, используются в интерактивном режиме и требуют участия эксперта. Примеры таких систем – HOL (High Order Logic), Isabelle [8], PVS [9]. Существуют так же статические методы проверки пра- вильности модели. Как правило, в осно- ве таких методов лежит поиск типичных ошибок по некоторым шаблонам (напри- мер, [10]), а так же принципы синтаксиче- ского анализа переходов на предмет выявления потенциальных нарушений. К проблемам статического анализа можно отнести отсутствие проверки достижи- мости, вследствие чего такие методы об- наруживают либо слишком большое число ложных ошибок, либо могут пропускать фактические. Инструменты автоматиче- ской верификации на основе статического анализа применяются достаточно широко, поскольку не требуют специальной подго- товки от пользователя и достаточно удоб- ны в эксплуатации. Большинство доказав- ших свою эффективность на практике та- ких методов часто включают в состав ком- пиляторов, на их основе усовершенствуют семантические правила языков програм- Формальні методи розробки програмного забезпечення мирования, а так же стили и стандарты разработки ПО [11]. Второй подход, проверка модели, предполагает систематическое исчерпы- вающее исследование математической модели [12]. Метод был впервые предло- жен в 1981 г. Эдмундом Кларком и его ас- пирантом Алленом Эмерсоном для вери- фикации параллельных систем с конечным числом состояний. Они рассматривали глобальный граф переходов параллельной системы как конечную структуру Крипке, и предложили эффективный алгоритм для определения того, является ли данная структура моделью заданной формулы темпоральной логики. В последствии Эд- мунд М. Кларк, Аллан Эмерсон и Джозеф Сифакис в 2007 году были удостоены пре- мии Тьюринга за «их роль в развитии про- верки моделей – высоко эффективную технику верификации программ, широко применяемую при разработке как про- граммного, так и аппаратного обеспече- ния» [13] (в сфере информационных тех- нологий премия Тьюринга имеет статус, аналогичный Нобелевской премии в ака- демических науках). Проверяемые свойства обычно за- даются в виде формулы темпоральной логики. Темпоральная логика есть класси- ческая логика, расширенная темпоральны- ми модальностями [14]: операторы необ- ходимости и возможности ◊. Оператор интерпретируется как "всегда" ("always"), оператор ◊ – "со временем" ("eventually"), такие операторы позволяют специфициро- вать события во времени без введения яв- ного понятия времени. Традиционные ло- гики могут специфицировать свойства, описывающие мгновенные состояния сис- тем, темпоральные же логики применяют для проверки динамических свойств пове- дения моделей недетерминированных ре- активных систем. Различают линейные и ветвящиеся темпоральные логики. В ли- нейной состояние системы в каждый мо- мент времени определяется однозначно, тогда как в ветвящейся состояние в сле- дующий момент времени определяется не- детерминированным образом и процесс может иметь несколько продолжений. Динамические свойства систем так же мо- гут быть представлены временными авто- матами, которые функционируют в реаль- ном времени, совершая переходы из со- стояния в состояние. При этом переходы совершаются мгновенно, и, пока автомат находится в каком-либо состоянии, время непрерывно увеличивается. Однако авто- мат может находиться в состоянии до тех пор, пока не нарушены ограничения этого состояния. Временные автоматы являются обобщением конечных ω-автоматов (авто- матов Бюхи и Мюллера) [15]. Автоматы Бюхи используются для моделирования конечных параллельных процессов, а про- блема верификации сводится к проблеме языковых включений [16]. Теории и технике верификации, объединенной названием "model checking", посвящена огромная литература, от моно- графий и вводных обзоров до многочис- ленных слайдов университетских курсов [12, 17–32], проводятся специализирован- ные конференции [33]. В последнее время метод широко используется для проверки свойств полноты, непротиворечивости и безопасности как программного, так и аппаратного обеспечения промышлен- ных систем. Важной проблемой формальной проверки моделей является проблема раз- решимости. Так, при моделировании вре- мени как непрерывной сущности, модель имеет уже бесконечное число состояний. Например, счетчиковая машина Минского уже всего с двумя счетчиками может мо- делировать машину Тьюринга, в которой проблема достижимости терминального состояния (останова) из некоторого ини- циального состояния в общем случае явля- ется неразрешимой [34]. Многие работы, посвященные проверке моделей с беско- нечным числом состояний накладывают различные ограничения как на описание поведения модели, так и на проверяемые свойства, применяют техники абстракций и символьного моделирования [21–26, 28– 32, 36, 37]. Основной проблемой верификации все же есть проблема комбинаторного взрыва числа состояний модели. Как пра- вило, состояние проверяемой модели включает большое количество атрибутов 76 Формальні методи розробки програмного забезпечення 77 и процессов. Даже если число процессов конечно и все атрибуты могут принимать лишь конечное число значений, общее число состояний может быть очень бо- льшим. Основными источниками взрыва числа состояний являются число компо- нент (процессов) модели и интерливинг между ними, а так же степень недетерми- низма их поведения и используемые ти- пы данных, включающие большое число значений. Реальные системы обычно па- раллельны, а число состояний моделей параллельной системы растет экспонен- циально с числом компонент. Так, опыт верификации промышленных систем по- казал, что оценочное число состояний, как правило, превышает . Очевидно, что при таком количестве достижимых со- стояний проверка модели путем наивного перебора практически не осуществима. Решению проблемы посвящено множест- во различных технологий – разработаны методы частичного порядка для элими- нации избыточного интерливинга, исполь- зуются методы определения симметрии при проверке эквивалентности состояний, исследуются информационные зависимо- сти для поэтапной верификации состав- ляющих компонент, применяются техники абстракции, факторизации, аппроксима- ции, символьного моделирования; к про- цессу верификации активно привлечен пользователь (эксперт предметной облас- ти) – его «подсказки» используются для направленного поиска, построения абст- ракций, накладывания ограничений на пространство поиска; используются си- муляторы, интерактивные режимы и пр. Однако, существующие методы имеют ряд недостатков и, к сожалению, на сего- дняшний день не существует приемлемого для промышленности универсального ре- шения данной проблемы. Неудачное упо- рядочение атрибутов в худшем случае экс- поненциально увеличивает число OBDD узлов, известно так же, что вне зависимо- сти от способа упорядочения, булева функция, представляющая любое из двух средних выходных значений n-битного умножителя, имеет экспоненциальную сложность OBDD-представления [38]. Верификаторы, не имеющие канони- ческой формы состояний модели, испы- тывают трудности с проверкой эквива- лентности, что порождает дополнитель- ный комбинаторный взрыв либо по раз- меру используемой памяти, либо по вре- мени, затраченному на сравнения состоя- ний. Методы построения абстракций пло- хо автоматизируются, часто приводят к ложным результатам (т.н. false negatives или false positives), которые нуждаются в уточнениях и, как следствие, в повтор- ных запусках экспериментов; критерии для завершения процесса уточнений, как правило, основаны на эвристиках или требуют участия эксперта. Статические методы выявления зависимостей преуве- личивают фактические информационные связи, что отражается на эффективности абстракций. 10002 Проверяемые свойства формальных моделей Типичными распространенными ошибками в моделях большинства про- граммных и аппаратных систем, как правило, являются: выход за пределы допустимых значений (переполнение бу- фера, неправильная индексация), пере- полнение и потеря значимости в арифме- тических операциях, обращение к неини- циализированным атрибутам, неодно- значная реакция на воздействующие сиг- налы, недостижимость функционально- сти, тупики, зацикливание, а так же нару- шение условий безопасности и живости поведения системы, сформулированных для проверки. Современные системы ве- рификации предлагают формулировать желаемые свойства моделей в виде формул темпоральной логики [39]. При этом проверяемые свойства могут зада- ваться как в виде линейных, так и вет- вящихся темпоральных логиках, напри- мер, таких, как: − MTL (metric temporal logic) – пропозициональная логика с ограничен- ными операторами, включает темпораль- ные операторы until, next, since и previous; − TPTL (timed temporal logic) – Формальні методи розробки програмного забезпечення пропозициональная логика полупорядка, которая использует только темпоральные операторы until и next; − RTTL (real-time temporal logic) – логика с явными таймерами; − XCTL (for explicit-clock temporal logic) – пропозициональная логи- ка с явными таймерами, в которой времен- ные ограничения содержат только сравне- ние и добавление; − MITL (metric interval temporal logic) оперирует неотрицательными веще- ственными числами в качестве домена времени, интерпретируется через последо- вательности временных наблюдений; − RTCTL (for real-time computation tree logic) – пропозициональ- ная логика разветвленного времени для синхронизированных систем, являет- ся расширением CTL с точечным пред- ставлением строго монотонного реально- го времени; − TCTL (timed computation tree logic) – пропозициональная логика с менее ограниченной семантикой, является рас- ширением CTL с точечным представлени- ем строго монотонного реального времени. Последующие версии этой логики исполь- зуют интервальную семантику времени и синтаксис полупорядка с примитивами сравнения и добавления констант. Для ре- шения задач верификации распределенных систем на основе временных логик созда- ются языки, позволяющие описывать вре- менные спецификации системы. При этом подходе возникает проблема разрешимо- сти языка, которая зависит от временного домена и операций над временными пере- менными [30]. Наиболее используемыми в совре- менных системах верификации логиками ввиду их универсальности являются LTL, CTL, а так же их объединение CTL. LTL (Linear Temporal Logic) LTL построен из набора пропози- циональных переменных, классических логических связок ¬, ∨, ∧, ⇒ и темпораль- ными операторами: • X для выражения следующего со- стояния (neXt); • G всегда (Globally); • F когда-нибудь в будущем (Future); • U до тех пор, пока (Until). Семантика формул LTL определя- ется на пути поведения системы перехо- дов. Формула истинна на пути, если и только если она истинна в начальном со- стоянии этого вычисления. Семантика темпоральных операторов приведена далее [40]. Унарные операторы: X φ neXt: φ должно выполнятся в сле- дующем состоянии. G φ Globally: φ должно выполнятся на всем дальнейшем пути. F φ Future: φ должно выполниться когда- нибудь на пути. Бинарные операторы: ψ U φ Until: ψ должно выполнятся до тех пор, пока не выполнится φ, при этом φ должно когда-нибудь выполнится. ψ R φ Release: φ выполняется до первого состояния, в котором выполняется ψ, или всегда, если ψ не выполняется. Примеры формул LTL для записи некоторых свойств: G(q⇒XG¬q) – q встретится в будущем не более одного раза, Fq∧G(q⇒XG¬q) – q встретится в бу- дущем точно один раз, G(p⇒Fq) – на р всегда будет реакция q. Две темпоральные формулы φ и ψ эквива- лентны, записывается φ ≡ ψ, когда они вы- ражают одно и то же свойство. Иными словами, φ ≡ ψ означает, что для любого состояния пути σ утверждение σ\|=φ верно тогда и только тогда, когда верно σ\|=ψ. Операторы U, F и G можно определить бесконечной формулой с помощью допол- нительного оператора Х: pUq ≡ q ∨ p∧Xq ∨ p∧Xp∧XXq ∨ … Fq ≡ q ∨ Xq ∨ XXq ∨… Gq ≡ q ∧ Xq ∧ XXq ∧… А также рекурсивно конечной формулой: pUq ≡ q ∨ p∧X(pUq) ; 78 Формальні методи розробки програмного забезпечення 79 Gq ≡ q ∧ XGq ; Fq ≡ q ∨ XFq. Пара операторов X и U образует темпора- льный базис LTL. Действительно: F φ = true U φ ; G φ = false R φ = F φ ; ψ R φ = ( ψ U φ) . Иногда используются так же не- стандартные операторы. В некоторых сис- темах вводится бинарный оператор weak until (записывается W), семантика которо- го схожа с оператором until, но условие остановки не требуется: ψ U φ = F φ∧(ψ W φ) ; ψ R φ = φ W (ψ∧φ) ; φ W ψ = ψ R (ψ∨φ) ; φ W ψ = (φ U ψ) ∨G φ . Существуют также два важных свойства моделей, которые можно выразить с помощью линейной темпо- ральной логики: свойства безопасности (safety), которые утверждают, что что-то плохое никогда не случится (G φ), и свойства живости (liveness), которые используются для выражения того, что что-то хорошее будет периодически случаться (GFψ). Для нарушения свойств безопасности можно построить контр- пример конечной длины, тогда как для свойств живости префикс каждого контрпримера можно продолжить беско- нечным путем. Для проверки выполнимости LTL формулы на модели современные системы верификации пользуются тем, что любую LTL формулу можно транслировать в ав- томат Бюхи [16]. Автоматом Бюхи называ- ется пятерка ),,,,( 0 TFsSA ρ= , где S – множество состояний, – началь- ных состояний, а – допускающих состояний, SS ⊆0 SF ⊆ STS →×:ρ недетерминиро- ванная функция переходов и T – алфавит над множеством переходов. Выполнение A над бесконечным словом это последовательность , где ...21aaw = ...10ss 00 Ss ∈ и ),( 1 iii ass −∈ρ , для всех . Выполне- ние является принимающим, если существует допускающее состояние, которое повторяется бесконечно часто, т. е. для некоторого существует бесконечно много таких i, что 1≥i ...10ss Fs∈ ssi = . Бесконечное слово w принимается автома- том A, если существует допускающее выполнение A над w. Множество беско- нечных слов, которые принимаются A, обозначается L (A). Варди и Волпер показали [16], что такой автомат принимает только те (бес- конечные) последовательности состояний, которые удовлетворяют заданной LTL формуле. Автомат, соответствующий свойству может иметь состояний, где n – число подформул (темпоральных опе- раторов) в формуле свойства. Таким обра- зом, размер произведения автоматов, кото- рый определяет общую сложность метода, пропорционален , где N – число достижимых состояний модели. )(2 nO )(2 nON ⋅ Линейная темпоральная логика LTL является подмножеством CTL. CTL* (Computation Tree Logic) CTL* [41] формулы включают в себя кванторы путей и темпоральные операторы. Определены два вида кванто- ров: A («для всех вычислительных путей») и E («для некоторого вычисли- тельного пути»). Такие кванторы, задан- ные для некоторого состояния, опреде- ляют, что для всех путей или для неко- торого пути, берущего начало в этом со- стоянии, выполняется некоторое свойст- во. Темпоральные операторы описывают свойства пути на всем дереве. Некото- рые системы проверки моделей предпо- лагают, что свойства модели специфици- рованы во фрагменте логики CTL* на- зываемой ACTL, которая исключает воз- можность описать существование пути. При этом отрицание ограничено до уровня атомарных формул, а квантификация пу- тей ограничена квантором всеобщности. http://en.wikipedia.org/w/index.php?title=Safety_(temporal_property)&action=edit&redlink=1 http://en.wikipedia.org/w/index.php?title=Liveness&action=edit&redlink=1 Формальні методи розробки програмного забезпечення Методы и системы проверки формальных моделей Для сокращения пространства ана- лизируемых состояний разработано мно- жество методов редукции, их можно раз- делить на два вида – точные, которые га- рантируют итоговый результат и эвристи- ческие, которые уменьшают время провер- ки, но при этом не гарантируют точности результатов. К точным можно отнести та- кие методы, как: Методы частичного порядка. Проектирование и тестирование парал- лельных систем усложняется тем, что ком- поненты могут взаимодействовать множе- ством зачастую непредусмотренных спо- собов. Интерливинг (перестановка выпол- нения действий параллельно работающих компонент) является одним из источников комбинаторного взрыва вариантов поведе- ния верифицируемой модели. Точки со- общения (доступ к общим ресурсам) асин- хронно работающих сообщающихся меж- ду собой и внешней средой процессов мо- гут быть определены статически, основы- ваясь на структурном синтаксическом описании верифицируемой модели; такая информация может быть использована для ограничения числа перестановок путем исключения незначимых с точки зрения проверяемых свойств. Использование ме- тода частичного порядка для элиминации избыточного интерливинга описано в 1994 году в работе Peled [42], подробное описа- ние метода и его адаптацию в различных верификаторах можно найти так же в [43– 46]. Необходимо отметить, что такая тех- ника статического определения точек ин- терливинга не подходит для случая сим- вольного моделирования, так как можно задать состояние (начальное, либо постро- ить динамически в процессе обхода), включающее условие зависимости атрибу- тов разных процессов, при этом оставляя их синтаксически «локальными». Использование симметрий при проверке эквивалентности состояний. На практике часто встречаются модели, содержащие множество однотипных про- цессов, например, телекоммуникационные задачи, в которых участвуют N телефонов. Как правило, в таких случаях стоит во- прос: выполняется ли требуемое свойство для всех N, и каковым должно быть это значение для доказательства (опроверже- ния). Известно, что в общем случае про- блема не разрешима [47, 48]. Однако, при некоторых ограничениях, можно восполь- зоваться перестановкой экземпляров про- цессов при проверке эквивалентности со- стояний. Так, система Merφ [48, 49] вводит специальный тип данных (scalarset) и ог- раничивает операции над ним (сравнения вида «равно» и «не равно», а так же индек- сацию и присваивания). Такое ограниче- ние влечет неупорядоченность элементов данного типа, что позволяет модифициро- вать функцию проверки эквивалентности состояний добавлением проверок допол- нительных состояний, порождаемых путем перестановок атрибутов модели по прин- ципу их принадлежности к процессам, а так же хранению значения идентификато- ров процессов. Таким образом, отношение проверки эквивалентности ослабляется, и достигается сокращение числа анализи- руемых состояний. Методы использования симметрии описаны так же в [50, 51]. Сжатие состояний. Каждый про- цесс модели может содержать большое ко- личество атрибутов, в то время как один переход изменяет лишь несколько атрибу- тов. Так называемый state compression ме- тод [52] экономит память в ходе выполне- ния проверки свойств, используя указатели на состояния тех процессов, которые не изменялись в последнем переходе на пути вычисления. Таким образом, одинаковые части в различных состояниях модели не дублируются. Сопутствующим методом является возврат к точке выбора ветви по- ведения. Так, если из некоторого состоя- ния существует допустимый детерминиро- ванный переход, не нуждающийся в ин- терливинге с другими процессами, и таким образом, не ветвящий пространство пове- дения верифицируемой модели, то такое состояние не является точкой выбора. Ал- горитм обхода при одном шаге назад вос- станавливает состояние модели, являю- щееся точкой выбора, при этом достигает- ся эффект «сворачивания» (collapsing) ли- нейных участков поведения модели. 80 Формальні методи розробки програмного забезпечення 81 Абстракции на основе исследова- ния зависимостей. Такие методы успешно практикуется в компиляторах, где инфор- мационные связи исследуются, как прави- ло, статически. Например, локализирован- ная редукция Куршана [53] представляет собой итеративную технику, которая на- чинает проверку с небольшим подмноже- ством релевантных L-процессов, которые топологически близки к спецификациям проверяемых свойств в графе зависимости переменных. Все остальные переменные проверяемой программы абстрагируется путем замены недетерминированными присваиваниями. Если обнаруживается, что порожденный таким образом контр- пример ложный, вводятся дополнитель- ные переменные для элиминации такого контрпримера. Так же описание методов редукции, основывающихся на информа- ционных зависимостях можно найти в [54–56]. В работе [57] описан метод «рас- слоения» (slicing) целью которого является уменьшение исходной формальной модели путем удаления тех переходов (операторов программы), которые не влияют на прове- ряемые свойства. Для этих целей строятся (статически) графы потока управления (control flow graph) и программы (program flow graph). Основываясь на информаци- онных связях в этих графах, создаются их проекции, сохраняющие такие поведения программы и значения переменных, кото- рых достаточно для верификации прове- ряемых свойств. Метод оказывается по- лезным и эффективным при отладке фор- мальных моделей. В работах [37, 58] описан метод символьного моделирования, в котором состояния представляются формулами многосортного исчисления предикатов первого порядка; для их преобразования используется предикатный трансформер. В работе [59] описан метод ослаб- ления эквивалентности состояний за счет игнорирования незначимых значений ат- рибутов. Под «незначимым» на некотором состоянии понимается значение атрибута, которое не используется ни одним перехо- дом, а так же не различается ни одним из проверяемых свойств на всех состояниях, достижимых из этого состояния. Такие аб- стракции состояний строятся «на лету», таким образом, метод не чувствителен к зависимостям атрибутов, которые обу- словлены недостижимыми переходами. Абстракции предикатов. В по- следнее время популярной техникой про- верки моделей стала техника построения абстракций с последующим уточнением. Уточнения подразумевают повторные за- пуски эксперимента для устранения лож- ных поведений. Такой подход часто назы- вается Counter-Example Guided Abstraction Refinement (CEGAR), и составляет основу для многих популярных верификаторов (см., например, [22, 24, 25, 35, 36, 54]). В основе метода абстракции предикатов по- ложена техника удаления данных, при этом отслеживаются только определенные предикаты над данными. В абстрактной модели каждый предикат представляется булевской переменной, в то время как подлинные значения переменных элими- нируются. Далее приведен пример (рис. 1), описанный в работе [24] поясняющий ме- тод абстракции предикатов. Рис. 1. Программа P Пусть дана программа P с тремя перемен- ными: x, y с диапазоном допустимых зна- чений {0,1,2}, и reset {TRUE, FALSE} (см. рис. 1). Множество атомарных формул Atoms(P) = {(reset=TRUE, (x = y), (x < y), (x = 2)}. Имеются два кластера формул, FC1 = {(x = y), (x < y), (y = 2)} и FC2 = {(reset = TRUE)}. Соответствующие им кластеры переменных {x, y} и {reset}. Зна- чения (0,0) и (1,1) первого кластера в од- ном классе эквивалентности потому что все атомарные формулы в кластере FC1 выполняются одинаково: (0,0) \|= f если и только если (1,1) \|= f. Домен {0,1,2}x{0,1,2} разделен на пять классов эквивалентности по этому критерию: Формальні методи розробки програмного забезпечення 0 = {(0,0), (1,1)}; 1 = {(0,1)}; 2 = {(0,2),(1,2)}; 3 = {(1,0), (2,0), (2,1)}; 4 = {(2,2)}. Домен {TRUE, FALSE} имеет два класса эквивалентности – один включает FALSE, другой – TRUE. Так определяются функ- ции абстрагирования h1:{0,1,2}2 {0,1,2,3,4} и h → 2 = {TRUE, FALSE} {TRUE, FALSE}. Функция h → 1 определяется следующим образом: h1(0,0) = h1(1,1) = 0, h1(0,1) = 1, h1(0,2) = h1(1,2) = 2, h1(1,0) = = h1(2,0) = h1(2,1) = 3, h1(2,2) = 4. Вторая функция h2 тождественна h2(reset) = reset. После определения функций отображения применяются стандартные методы экзи- стенциальной абстракции [21, 60]. Однако необходимо отметить, что при таком под- ходе стоит проблема числа возможных аб- стракций. Например, метод, описанный в работе [60] для диапазона допустимых значений конкретной модели Dс = {0, 1, 2} x {0, 1, 2} и абстрактной Da = {0, 1}x{0, 1} имеет 49 = 262144 функций отображения h из Dc в Da. В развитии этой работы [25], авторы предложили использовать класте- ры переменных, и соответственно функ- цию отображения для каждого кластера отдельно: h = (h1, h2). Число функций ото- бражения из {0, 1, 2} в {0, 1} равно 23, та- ким образом, имея два кластера, общее число возможных вариантов построения абстракции для данного примера сокраща- ется до 64. Метод предполагает три (повто- ряющихся) этапа: 1) построение абстрак- ции, 2) проверка свойств, 3) анализ контр- примера для уточнения абстракции. Пример. Рассматривается модель управления светофором (рис. 2) и свойство для доказательства f = AGAF(state = red); используемая функция абстракции h(red) = = red и h(green) = h(yellow) = go. Рис. 2. Модель светофора Mc и его абстракция Ma Легко видеть, что Mc \|= f в то время как Ma \|≠ f, потому что существует бесконеч- ный путь {red, go, go, …}, который опро- вергает это свойство. Если абстрактный контрпример не соответствует поведению конкретной модели, его называют лож- ным. В приведенном примере таковым яв- ляется путь {red, go, go, …}. Таким образом, метод может выда- вать ложные контрпримеры, истинность которых проверяется на конкретной моде- ли. Если при такой проверке оказывается, что контрпример недопустим, модель уточняется (строится новая, более деталь- ная абстракция), и процедура проверки по- вторяется. Некоторые методы используют абстракции, определяемые пользователем, как, например [17, 20–22]. Популярные эвристические методы используют такие техники проверки моде- лей: Накладывание ограничений на пространство поиска. Чаще всего прибе- гают к ограничению на длину пути, а мак- симальное значение фиксируется изна- чально. Так же используют [61] такие ви- ды ограничителей, как время, число ветвей и др. Многие верификаторы используют заданные пользователем специальные состояния («fairness constraints», «hints», «restricted states») [17, 20] для отсечения ветвей анализируемого поведения. Аппроксимации. В работе [62] строится бинарный вектор длины, равной количеству различных предикатов в пере- ходах модели. Пройденные состояния ха- рактеризуются только этим вектором, что 82 Формальні методи розробки програмного забезпечення 83 позволяет говорить о покрытии предика- тов. В работе [24] авторы предлагают под- ход, аналогичный локализированной ре- дукции Куршана, при котором элимини- руются переменные, находящиеся в графе зависимости на дистанции, превышающей заданную. В работе [63] описана техника аппроксимации bit hashing, которая позво- ляет не различать состояния, близкие по их бинарному представлению. Направленный поиск. В работе [64] предложен метод автоматического на- правления поиска нарушения свойств мо- дели, в основе которого лежит структур- ный анализ переходов модели и проверяе- мых свойств. В работах [65, 66] помимо спецификаций поведения системы, на вход подается сценарий тестирования, называе- мый обычно целью теста (test purpose), та- кой сценарий задается пользователем в ви- де последовательности сообщений, кото- рыми обмениваются компоненты модели (например, в виде MSC [66]) или регуляр- ного выражения [67] и может быть исполь- зован в качестве направления при поиске труднодостижимых состояний. Использо- вание эвристических методов направления поиска для обнаружения ошибок так же описаны в [68, 69]. За последние два десятилетия раз- работано множество различных как ком- мерческих, так и свободно распространяе- мых систем верификации для программ- ных и аппаратных систем. Большое число верификаторов разрабатывается из-за от- сутствия удовлетворительного для про- мышленности универсального метода про- верки правильности разрабатываемых сис- тем. Различные верификаторы решают уз- коспециализированные проблемы, напри- мер, проверку свойств, специфических для языков реализации систем. Как правило, верификаторы имеют собственные специ- альные языки спецификаций и методы проверки моделей. Ниже приведены крат- кие описания наиболее популярных систем верификации. – Cadence SMV (Symbolic Model Verifier) [29] – разработка Cadence Berke- ley Laboratories для символьной верифика- ции моделей. Проверяет требования кор- ректности, выраженные в CTL. SMV снабжен двумя языками моделирования – Verilog и расширенным SMV. Для фор- мального задания систем переходов ис- пользуется структура Крипке – модель, которая имеет конечное множество со- стояний и переходов между ними, причем каждое состояние помечено некоторым множеством истинных в этом состоянии предикатов. Структура Крипке K – это четверка K = (S, I, R, L), где S – конечное непустое множество состояний; I – непус- тое множество начальных состояний; R ⊆ S x S – множество переходов; L: S→2AP – функция разметки, АР – конечное множе- ство атомных утверждений (атомных пре- дикатов). Путь в структуре Крипке – лю- бая бесконечная цепочка π = s0s1s2s3…, та- кая, что s0∈I и (si,si+1)∈R. За последние десятилетия структу- ры Крипке признаны адекватной моделью реагирующих дискретных систем управле- ния, параллельных и распределенных ал- горитмов [32]. Для сжатия проверяемого множества состояний используются сим- вольные способы представления моделей – двоичные разрешающие диаграммы (BDD, Binary Decision Diagrams) [38]. Алгоритмы верификации моделей с помощью BDD могут быть значительно эффективнее яв- ного перебора состояний в том случае, ко- гда BDD системы переходов модели и промежуточных результатов остаются компактными [29]. – NuSMV (New Symbolic Model checker [23, 70]). Символьный верифика- тор моделей, разработанный как общий проект Formal Methods Group в ITC- IRST, the Model Checking group в Carnegie Mellon University, the Mechanized Reasoning Group в University of Genova и Mechanized Rea- soning Group в University of Trento. NuSMV – это обновленная версия SMV, был разра- ботан в качестве системы с открытой ар- хитектурой для верификации моделей, ко- торая может быть использована для про- верки промышленных разработок, как ядро составных верификационных инструмен- тов и как основа для тестирования других технологий формальной верификации. NuSMV производит верификацию, Формальні методи розробки програмного забезпечення комбинируя техники использования BDD и проверку моделей, основанную на SAT (SAT-based model checking). Проверяет требования корректности, выраженные в CTL*. По сравнению с SMV обеспечивает такие возможности как взаимодействие конечных автоматов, анализ инвариантов, реализация методов декомпозиции. – VCEGAR (Verilog Couter Example Guided Abrstaction Refinement [36, 71]). Предназначен для проверки моделей аппа- ратного обеспечения; использует язык Ver- ilog для описания поведения модели. Реа- лизует метод абстракции и уточнений пре- дикатов, который разработан для проверки моделей ПО, и реализован в SLAM. Разра- батывается при поддержке General Motors Collaborative Research Lab at CMU, Naval Research Laboratory, Semiconductor Re- search Corporation и др. Использует Ca- dence SMV, NuSMV. – BLAST (Berkeley Lazy Abstraction Software Verification Tool [19, 72]). Вери- фикатор С программ. Использует метод абстракции предикатов. Строит абстрак- ции на лету с требуемой точностью. – SLAM – развитие BLAST, разра- ботка Microsoft Research [73]. Производит верификацию кода, написанного на языке C. Требования корректности задаются на специализированном языке SLIC. Продукт ориентирован на верификацию драйверов. Так же необходимо отметить разработку той же группы разработчиков Terminator, которая предназначена для проверки за- цикливания программ. – CBMC [27, 74] – верификатор, который обеспечивает возможность огра- ниченной проверки моделей (Bounded Model Checker) для языков ANSI-C и C++. Он осуществляет такие проверки, как вы- ход за границы массивов (переполнение буфера), безопасность указателей, исклю- чения и утверждения, сформулированные пользователем. – VeriSoft [45] разработан для про- верки свойств параллельно работающих процессов. Его отличительной особенно- стью является использование так называе- мого поиска «без состояний» (stateless), запоминаются только переходы текущей трассы. При этом используются техника выборочного поиска (selective search), в основу которого положен метод частично- го порядка. Так как состояния не запоми- наются, и как следствие, циклы не обна- руживаются, накладываются ограничения на глубину поиска. Проверяются пользова- тельские свойства (выраженные пропози- циональными формулами), а так же нали- чие тупиков, отклонений (когда процесс не выполняет ни одного наблюдаемого пере- хода в течении некоторого времени, за- данного пользователем) и ливлоков (когда выполнение очередного наблюдаемого пе- рехода некоторого процесса заблокирова- но на протяжении некоторого числа пере- ходов). Верификатор успешно применялся в тестировании целевого кода ряда про- мышленных проектов. – SPIN [18, 52] – инструмент формальной верификации распределенных систем. Ис- пользует прямой перебор, проверяя свой- ства модели в оперативном режиме. Разра- батывался в Bell Labs в группе в Computing Sciences Research Center, начиная с 1980. С 1991 года находится в свободном распро- странении. SPIN – это популярный инст- румент с открытым кодом, используемый во многих организациях мира, в 2001 году был награжден ACM престижной премией System Software Award. SPIN имеет три основных режима работы: режим симулятора, позволяющий осуществлять быстрое прототипирование со случайным, управляемым или интерак- тивным моделированием; режим верифи- катора, способный строго доказать истин- ность требований корректности, указан- ных пользователем; режим аппроксима- ции, который способен подтверждать пра- вильность больших по объему протоколов с максимальным покрытием пространства состояний. SPIN поддерживает высокоуровне- вый язык PROMELA (PROcess MEta LAnguage), с помощью которого можно специфицировать описание программных систем. Этот язык поддерживает только дискретные типы данных, а также функ- ции работы с многопоточностью. 84 Формальні методи розробки програмного забезпечення 85 SPIN может быть использован для отслеживания ошибок логического дизай- на в операционных системах, протоколах обмена данными, системах переключате- лей, параллельных и распределенных ал- горитмах. Для выражения проверяемых свойств SPIN использует линейную тем- поральную логику (LTL); обеспечивает прямую поддержку для использования языка С как части спецификации модели. Это делает возможным проведение прямой верификации уровня реализации специфи- кации программного обеспечения, исполь- зуя SPIN как драйвер и логический инст- румент для верификации высокоуровне- вых темпоральных свойств. Инструмент поддерживает динамические рост и уменьшение количества процессов, ис- пользуя технику эластичных векторов со- стояний (rubber state vector technique); под- держиваются так же синхронизированный и буферизированный обмены сообщения- ми, а также общение через разделяемую память. SPIN работает оперативно (on- the-fly), таким образом, избегая необхо- димости построения глобального графа состояний, или структуры Крипке, в ка- честве предпосылки для верификации каких-либо свойств системы. Для опти- мизации верификации используется тех- ника частичного порядка (partial order reduction), а так же техника слияния со- стояний (statement merging) – которая производит слияние внутренних (нена- блюдаемых) переходов процесса для ре- дукции количества достижимых состоя- ний модели. Для эффективного хранения состояний используется компрессия со- стояний (разновидность «byte-sharing»), а так же техника аппроксимации bit hashing. Теоретическое обоснование для SPIN, можно найти в [18, 52]. Метод аппроксимации bit hashing детально обсу- ждается в [63]. На основе SPIN реализо- вано множество верификаторов для про- верки специфик доменов. Создатели ут- верждают, что он приспособлен для ре- шения крупномасштабных задач. – Merφ [48, 49] является инстру- ментом формальной верификации распре- деленных систем, использует прямой пе- ребор состояний модели, которые пред- ставлены значениями всех атрибутов. От- личительной особенностью является метод использования симметрий при проверке эквивалентности состояний. Метод эффек- тивен при наличии повторяющихся ком- понент (процессов) модели, число которых заранее неизвестно. Ввиду ограничений на размер оперативной памяти, применяется техника записи состояний модели на жест- кий диск. Заключение Данная работа представляет собой обзор современных методов автоматиче- ской проверки свойств формальных моде- лей. Рассмотрены точные и эвристические методы редукции пространства поиска. Так же приведен обзор современных попу- лярных инструментальных средств вери- фикации. 1. Brooks F. No Silver Bullet – Essence and Ac- cidents of Software Engineering // Proc. of the IFIP10–th World Computing Conf. – 1986. – P. 1069–1076. 2. Nelson M., Clark J., Spurlock M. Curing the Software Requirements And Cost Estimating Blues // Program manager. – 1999. 3. Rashinkara P., Paterson P., Singh L. System- on-a-Chip Verification – Methodology and Techniques // Kluwer Academic Publishers. – 2001. – 392 P. 4. Boehm B., Basili V. Software Defect Reduc- tion Top 10 List // IEEE Computer. – 2001. – Vol. 34(1). – P. 135–137. 5. Hoare T. The verifying compiler: A grand challenge for computing research // J. ACM. – 2003. – Vol. 50(1). – P. 63–69. 6. Hoare C.A.R. An axiomatic basis for com- puter programming // Communications of the ACM. – 1969. – Vol. 10, N 12. – P. 576–585. 7. Floyd R. Assigning meaning to programs // Proc. of Symposium in App. Mathematics // J.T. Schwartz, ed. Mathematical Aspects of Computer Science. – 1967. – Vol. 19. – P. 19–32. 8. Nipkow T., Paulson L., Wenzel M. Isa- belle/Hol: a proof assistant for higher–order logic // LNCS 2283, Springer–Verlag. – 2002. – 218 p. Формальні методи розробки програмного забезпечення 9. Owre S., Shankar N. Writing PVS Proof Strategies // Design and application of strate- gies/ Tactics in Higher Order Logics. – 2003. – P. 1–15. 10. http://www.klocwork.com 11. Кулямин В. Методы верификации про- граммного обеспечения // Всероссийский конкурсный отбор обзорно–аналитических статей по приоритетному направлению "Информационно телекоммуникационные системы". – 2008. – 117 с. 12. http://en.wikipedia.org/wiki/Model_checking 13. http://awards.acm.org/homepage.cfm?srt=all &awd=140 14. Emerson E. Temporal and modal logic // J. van Leeuwen editor: Handbook of Theoretical Computer Science, Elsevier. – 1990. – P. 997–1072. 15. Wolfgang T. Automata on infinite objects // Handbook of theoretical computer science. – 1990. – P. 133–191. 16. Sistla A., Vardi M., Wolper P. The comple- mentation problem for Buchi automata with application to temporal logic // Theoretical Computer Science. – 1987. – N 49. – C. 217–237. 17. Barner S., Glazberg Z., and Rabinovitz I. Wolf – bug hunter for concurrent software us- ing formal methods // In Computer Aided Verification. – 2005. – P. 153–157. 18. Ben–Ari. M. Principles of Spin // Springer Verlag. – 2008. – 216 p. 19. Beyer D., Henzinger T., Jhala R., Majumdar R. The software model checker BLAST // Int. J. Software Tools Technol Transfer. – 2007. – N 9. – P. 505–525. 20. Bloem R., Ravi K., and Somezi F. Symbolic guided search for CTL model checking // In Design automation conference. – 2004. – P. 29–34. 21. Burch J., Clarke E., McMillan K., and oth. Symbolic model checking: 10^20 states and beyond // Information and Computation. – 1992. – Vol. 98, N 2. – P. 142–170. 22. Chaki S. A Counterexample Guided Abstrac- tion Refinement Framework for Verifying Concurrent C Programs // Doctoral Thesis. Carnegie Mellon University. – 2005. – P. 253. 23. Cimatti A., Clarke E. M., Giunchiglia E., and oth. NuSMV 2: An Open-Source Tool for Symbolic Model Checking // In Proc. of Int. Conf. on Computer–Aided Verification, Co- penhagen, Denmark. – 2002. – P. 359–364. 24. Clarke E., Grumberg O., Jha S. et al. Coun- terexample–guided abstraction refinement // Computer Aided Verification. – 2000. – P. 154–169. 25. Clarke E., Grumberg O., Jha S., and oth. Counterexample-guided abstraction refine- ment for symbolic model checking // Journal of the ACM. –2003. – Vol. 50. – № 5. – P. 752–794. 26. Clarke E., Jain H., Kroening D. Verification of SpecC using predicate abstraction // Formal Methods in System Design. – 2007. – Vol. 30. – P. 5–28. 27. Clarke E., Kroening D., Lerda F. A tool for checking ANSI–C programs // Tools and Al- gorithms for the Construction and Analysis of Systems / Ed. by K. Jensen, A. Podelski. LNCS 2988. – 2004. – P. 168–176. 28. Dams D. Abstraction in software model checking: principles and practice (Tutorial) // In Proc. of SPIN'02, LNCS 2318. – 2002. – P. 14–21. 29. McMillan K. Symbolic Model Checking // Kluwer Academic Publishers. – 1993. – 216 p. 30. Бурдонов И., Косачев А., Пономаренко В., Шнитман В. Обзор подходов к верифика- ции распределенных систем. – М.: ИС- ПРАН. – 2006. – 61 с. 31. Jhala R., Majumdar R. Software model checking // ACM Comput. Surv. – 2009. – Vol. 41(4). – 54 p. 32. Карпов Ю.Г. Model Checking. Верифика- ция параллельных и распределенных про- граммных систем. – БХВ-Петербург. – 2010. – 552 с. 33. http://spinroot.com/spin/workshops/index.html 34. Минский М. Вычисления и автоматы. – М.: Мир, 1971. – 368 с. 35. Henzinger T., Jhala R., Majumdar R., and Sutre G. Lazy abstraction // In Proc. of the 29th ACM Symposium on Principles of Pro- gramming Languages. – 2002. – Vol. 37. – P. 58–70. 36. Jain H., Kroening D., Sharygina N., and Clarke E. VCEGAR: Verilog counterexample guided abstraction refinement // In Tools and Algorithms for the Construction and Analysis of Systems '07. – 2007. – 4 p. 37. Летичевский А.А., Годлевский А.Б., Лети- чевский А.А. (мл.), Потиенко С.В., Песча- ненко В.С. Свойства предикатного транс- формера системы VRS. // Кибернетика и системный анализ. – 2010. – № 4. – С. 3–16. 38. Bryant R. Graph–based algorithms for Boo- lean function manipulation // IEEE Transac- tions on Computers. – 1986. – Vol. 35. – P. 677–691. 39. Pnueli A. The temporal logic of programs // In proc. of the 8th IEEE Symposium on Founda- tion of Computer Science. – 1977. – P. 46–57. 86 Формальні методи розробки програмного забезпечення 87 40. http://en.wikipedia.org/wiki/Linear_temporal _logic 41. http://en.wikipedia.org/wiki/Computational_tr ee_logic 42. Peled D. Combining partial order reductions with on-the-fly model checking // J. of Formal Methods in System Design. – 1996. – Vol. 8(1). – P. 39–64. 43. Gerth R., Kuiper R., Peled D., Penczek W. A partial order approach to branching time logic model checking // Information and Computation. – 1999. – Vol. 150(2). – P. 132–152. 44. Godefroid P. Partial-order methods for the verification of concurrent systems – an ap- proach to the state–explosion problem // Lec- ture notes in computer science, Springer- Verlag. – 1996. – Vol. 1032. –143 p. 45. Godefroid P. Software model checking: the VeriSoft approach // Formal methods in sys- tem design, Springer science. – 2005. – Vol. 26. – P. 77–101. 46. Peled D. Partial order reduction: linear and branching temporal logics and process alge- bras // POMIV '96: Proc. of the DIMACS workshop on Partial order methods in verifi- cation. NY, USA: AMS Press, Inc. – 1997. – P. 233–257. 47. Apt K., Kozen D. Limits for automatic verifi- cation of finite-state concurrent systems // In- formation Processing Letters. – 1986. – Vol. 22. – P. 307–309. 48. Ip C., Dill D. Better Verification through Symmetry // Formal Methods in System De- sign. – 1996. – Vol. 9. – P. 41–75. 49. Ip C., Dill D. Verifying Systems with Repli- cated Components in Murphi // Int. Conf. on Computer-Aided Verification. – 1996. – P. 147–158. 50. Miller A., Donaldson A., and Calder M. Symmetry in temporal logic model checking // ACM Comput. Surv. – 2006. – Vol. 38. – 37 p. 51. Nilsson M. Structural Symmetry and Model Checking // Ph.D. thesis, Uppsala University, Uppsala, Sweden. – 2005. – 157 p. 52. Holzmann G. The SPIN Model Checker: Pri- mer and Reference Manual. – Addison- Wesley Professional. – 2003. – 596 p. 53. Kurshan R. Computer-Aided Verification of Coordinating Processes // Princeton Univer- sity Press. – 1994. – 270 p. 54. Gupta A., Wang C., Kim H. Hybrid CEGAR: combining variable hiding and predicate ab- straction // Proc. IEEE/ACM Int. Conf. on computer-aided design. – 2007. – P. 310–317. 55. Kesten Y., Pnueli A. Control and data abstrac- tion: The cornerstones of practical formal ver- ification // Int. J. on Software Tools for Tech- nology Transfer. – 2000. – Vol. 2(4). – P. 328–342. 56. Lind–Nielsen J., Andersen H., Behrmann G. and oth. Verification of large state/event sys- tems using compositionality and dependency analysis // Journal of Formal Methods in Sys- tem Design. – 2001. – Vol. 18(1). – P. 5–23. 57. Krinke J. Program Slicing // In Handbook of software engineering and knowledge engi- neering. – Vol. 3. – 2005. – P. 307–332. 58. Годлевский А.Б. Предикатные трансформе- ры в контексте символьного моделирова- ния транзиционных систем // Кибернетика и системный анализ. – 2010. – № 4. – С. 91–99. 59. Колчин А.В. Автоматический метод дина- мического построения абстракций состоя- ний формальной модели // Кибернетика и системный анализ. – 2010. – № 4. – С. 70–90. 60. Clarke E. Grumberg O., Long D. Model checking and abstraction // In ACM Transac- tions on programming languages and systems. – 1994. – Vol. 16(5). – P. 1512–1542. 61. Jussila T. On Bounded Model Checking of Asynchronous Systems // Doctoral Thesis. Helsinki University of Technology, Labora- tory for Theoretical Computer Science. Re- search report A97. – 2005. – 136 p. 62. Ball T. A theory of predicate–complete test coverage and generation // In FMCO'2004: Symp. on Formal Methods for Components and Objects. SpringerPress. – 2004. – P. 1–22. 63. Holzmann G. An analysis of bitstate hashing // For-mal Methods in Systems Design. – 1998. – P. 301–314. 64. Peranandam P., Weiss R., Ruf J., Kropf T. and Rosenstiel W. Dynamic guiding of bounded property checking // In IEEE Inter- national High Level Design Validation and Test Workshop. – 2004. – P. 15–18. 65. Bourdonov I., Kossatchev A., Kuliamin V., and Petrenko A. UniTesK Test Suite Archi- tecture // In Proc. of FME 2002, LNCS 2391, Springer-Verlag. – 2002. – P. 77–88. 66. Grabowski J., Hogrefe D. SDL and MSC- Based Specification and Automated Test Case Generation for INAP // Telecommunication Systems J. – 2002. – Vol. 20(3,4). – P. 265–291. 67. Летичевский А.А., Колчин А.В. Генерация тестовых сценариев на основе формальной модели // Проблеми програмування. – 2010. – № 2–3. – С. 209–215. Формальні методи розробки програмного забезпечення 68. Edelkamp, S., Leue S. and Lafuente A. Di- rected explicit-state model checking in the validation of communication protocols // In- ternational j. on software tools for technology transfer. – 2003. – N 5. – P. 247–267. 69. Lafuente A. Directed Search for the Verifica- tion of communication protocols // PhD the- sis, University of Freiburg. – 2003. – 157 p. 70. http://nusmv.irst.itc.it 71. http://www.cs.cmu.edu/~modelcheck/vcegar 72. http://mtc.epfl.ch/software–tools/blast 73. http://research.microsoft.com/slam 74. http://www.cs.cmu.edu/~modelcheck/cbmc Получено 12.09.2011 Об авторах: Колчин Александр Валентинович, кандидат физико-математических наук, научный сотрудник, Летичевский Александр Александрович, кандидат физико-математических наук, старший научный сотрудник, Потиенко Степан Валериевич, кандидат физико-математических наук, научный сотрудник, Песчаненко Владимир Сергеевич, кандидат физико-математических наук, доцент. Место работы авторов: Институт кибернетики имени В.М. Глушкова НАН Украины. Тел. (044) 200 8423, e-mail: kolchin_av@yahoo.com, e-mail lit@iss.org.ua, e-mail stepan@iss.org.ua, Херсонский государственный университет, доцент кафедры информатики Тел. (095) 324 1557, e-mail: vladimirius@gmail.com 88

Обзор современных систем и методов верификации формальных моделей

Репозитарії

Схожі ресурси