2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 66
Текст из файла (страница 66)
1ОЛ. Прямер простоя системы параллельных проиессов Рассмотрим пример проатой системы (рнс. 10,1). Сисшма состоит из двух процессов, юакдый из которых пусть имеет четыре управляющих состояния (например, значения ачетчнка команд) и оперирует только одной целой переменной типа эьагс (1 байт). Подсистемы связаны двумя каналами, которые могут перелавать целые значенмя также типа звать и могут это сообщение храп»пь в буфере (т. е.
передавать не мгновенно). Число возмолщых состоя- г зз ннй этой простой системы равно (4 х 2з) х(2 ) = 2»е м10'е, т. е. сос»являет десятки миллиардов! Хош эте система очень проста, обычнме моголы вери- фию неси явим При числ стоя» смоя носи прим роще абра! трай лям ! Сима пнем (ппр! прею ные я риат» В ню ныц» верн»( ление пам»п тальк гереб рифи» милл» Расеи бое и булеи предо 1О "1 (2 од» мж (2 од» мн» го .ерить из ~ые ту- ве- Ю- табы, мы но)ж »но ив ~ые »ух »ня ре ~ые »нс ов- фиивцнн не мо~7т быль использованм для ее проверки: число ее состояний на несколько порядков превышает то, с чем мажет оперироыпь классический явный алгоритм пюбе! сЬесИлб При увеличении числа компонентов паравлельной системы и/нли увеличении числа переменных в системе происходит зкспоиеицивльный рост числа со.
стояний. Это явление известно под названием проблемы еэрыеа числа 'сосюояяюэ (зщю ехр1озюп ргоыею). можно заключить, что прн всей эффективности стандартных алгоритмов вернфиюшии шобе! сйесЫпб они могут быль применены только к очень простым системам илн к очень абстрактным упрощенным моделям параллельных сне»ем. Поэтому символьные алгоритмы обработки дискретной информации, рассмотренные в гк 9, оказались востребоваинымн для применения методов верификации воде! сйесйлб к моделям реальных, разрабатываемых на практике сисюм.
Символьная верификация вместо того, чтобы работать с явным предо»вале. инеи состояний и переходов структуры Кринке, работает с их неявным (1юрйЫ!) представлением булевыми функциямн в форме ВРВ. Этот подход предлагает решение проблемы взрыва числа состояний, поскольку символьные алгоритмы работают не с отдельными состояниями системы, а с характеристическими булевыми функциямн множеств состояний.
В названии одной из первых работ !14), в которой был разработан символьный алгоритм верификации, указывается встрономнчес гое число состояний вернфицируемых этим методом систем: "... )би н баме ..."! Явное представление подмножеств множества из 1Он состояний требует огромного объема памяти. Действителыю, пусть для запоминания одного состояния нужно только 1О байт. Тогда запоминание 1О'» состояний требует тысячу мнлляонов терабайт. Перебор такого числа состояний при выполнении алгоритмов верификации с помощью явных алгоритмов воде! сйесх!лб потребует сотен миллиардов лег.
Рассмотрим неявное представление такого множества с помощью В!)Р. Любое подмщнкество мнолюства нз 10" соспиний может быть представлено булевой функцией от 70 переменных, поскольку 10м = -2п. Таким образом, представление структуры Кринке для системы с числом состояний 10»' требует: !7 олпу булеву функцию от -70 двоичных переменных для представления множества начальных состояний„ О одну булеву функцию от -140 двоичных переменных дла представления мно~кества переходов; !7 лля каждого атомарного предиката н кюкдой подформулы проверяемой темпорюшной формулм одну булаву фущщню от -70 двоичных перемен- Гласа Ю ныц предсщаяяюшую мнвкество состояний, в которых эта формула истинна Если слояшость ВОР линейна или даже полнномиальна относительно числа переменных булевых функций, то представление в памяти этих функций н работа с ними не представляет трудности.
И действюпеяьно, именно этот "символьный" подход к представлению состояний н елгоритмы работы с ними привел к возможиссюн верификации промышленных программноаппаратных систем. Таким обрюом, использование ВРР и неявных алгоритмов обработки дискретных данных революционно юменяет возможности алгоритмов верификации, основанные на методе воде! сйесрйпф Но для того, чтобы использовать преимущества технологии ВРР в верификации, необходимо переформулировать проблему верификации в терминах манипуляций не с множествамн состояний, а с булевыми функциями, представляющими такие множества, Первый шаг на эгон пути — представление структуры Кринке булевыми функциями. 10.2.
Представление структуры Крипке булевыми функциями Для верификации структуры Кринке М = (Я, Юе, й, Ь) помощью синеаюьного алгоритма пюю!е! сйесй)пй необходимо сначала постронюь булавы функции в форме ВОР для: П множества начальных состояний М; О) множества переходов М; П лля кмкдого атомарного преднката — мвнкеств тех соспжний М, в которых он истинен. Пример 10.1 Рассмотрим, как ькикно предстампь структуру Кринке булевыми функциями. СтРУкгУРа Кйипке М (Я, Уе, й, б) (Рис. 10,2, а) имеет тРи состоаннЯ, 8=(аь юп юю), множесшо Яс начальных состояний (юе), пять переходов ((ам юю) (юс, юю),(юю, юс) (юю, юз) (юз, юз)» и т!юн кгомврных п!юеднюпх (р, Ч, г),такие что акр =(юс).
йююе "(юо юю) %ю'=(ю! юю). Выберем две булевы переменные «=(хилз) лля кодиромшия состояний. Закадируем состояния так: юе сэ00. е! сьб! юзее!О (т) К 0 а 0 0 Множ состоз ое Для и будем перех< глвее гб 1улв ис , в кото- ~кцняын. стоек ля, о числа гкцнй н но зтот работы шынно кн дис- вернфи- Вфорнуестввын гжестйз. ~левымн б е рнс. 1цй.
П)анер структуры Кршнп: а) хцнатервствчесвяя булеза функшп ее переходов; 6) шблннв нстлншктл харакгервствческой фувкцнн переходов; в) «е бвнерная решяюшм лнашгммв Мншкество нвчвльных состояний структуры Крнпке авшрмнг едннственное состояние ге.
Его код 00, позтомуь Яе =(зс(=(00((г). Для коднроввння вторых злементов в пврвх, представляющих отношения, будем использовать штрнховвнные переменные г' (х)',лз'). Опюшенне перекопе представится тшс й ы (0001, 0010, 01 00, 01 10, 1010( (т,т') . Окя бьп ке. < б<п (00,0зЦт) ,йи,-(0!,зо)( ) Час< яц<п мен< ние мар, бере Неча Со<и Все виям 1, Л< Либо 2.
то нл 3. то остап чив а ховав< ческе 072 Дмеа 10 Множесша состояний, в юторых внполилщтсн атомарные праднкагы< Йнр (00)(т) Характеристические функции дия бе, й и йгг < Х<с= *< тз Х<! л'! хг тз(л~чвхз)о-п<лз <тз «х<"<тзл<' Яз' Хаял(т)= гг тз (т) =— Хли (") хг~лз для выполнения символьной верифиющнн все зти функции прелставляются в форме ВЕЮ.
На рис.!0.2,6,е приведены таблица истинности и двоичная решмощаз диаграмма лля харш<гернстической булевой функции переходов структуры Кринке М . Очевидно, что лля анализа системы явно предстаалюь в памяти ии множество всех состояний структуры Кринке. ни ее переходы не нужно, символьная верификация проводит анализ систем, используя только неявное представление множества начальных состояний и переходов структуры Кринке с помощью булевых функций. 10.3. Представление структуры Крипке реагирующих систем булевыми функциями без предварительного явного построения структуры Крипке Приведенный выше пример показывает принципиальную возможность представления структуры Кринке булевыми функциямн. Однако, поскольку обычно символьная верификация используется для верификации систем с огромным числом состовний, приведенный выше пример с ручным кодированием состояний и переходов структурм Кринке не имеет смысла: такие структуры Кринке просто невозможно явно цредспшвть.
Прз Рас< шеи мер, стоя 4, то Эгн ч щих < ремея сгоян иа каг перел еа го огсз знш >лов 1ро кис Оказывается, что представление струшур Кринке булевой функцией может быть выполнено и без предварнтелыюго явного построения структуры Кринке. Покюкем это на простом примере. Прмыпр тй.й Рассмотрим представление булевыми функциямн структуры Кринке для решения логической юловоломки о планировании переправы через реку "фер.
мер, воли, коза и капуста", рассмотренной в гл. б, без явного построения сг» стояний структуры Кринка. Четыре булевы переменные в этой проблеме у, щ й и с обозначает нахождение соответствующего объекта на правом беро~у реки (значение иеременной равно! ) или на левом берегу (значение переменной равно 0). Состояние структуры Кринке — вектор значений переменных (у. щ й, с) . Например, состояние (0,0, 1, 1) означает, что фермер и жшк находятся на левом берегу, а коза и капуста — на правом берегу.
Начальное состояние структуры Кринке — (О, О, О, 0): все на левом берегу. Соответствующая харакюрнстическая булещь функция )(ю =,г' н зи с. Все возможные переходы лля этой системы определяются четмрьмя условиями переправы: 1. Либо только сам фермер может переправляться с одного берега на лругой. Либо фермер молмт перевезти с одного берега на другой: 2, только волка; или 3. только козу; или 4, только капусту, Зти четыре правила лепго щлмотся с помощью булевых функций, кодируюшнх соответствующие переходы в системе с помощью нештрихованных переменных (состояния до шага перехода) и штрпхованных переменных (состояния после шага перехода).
Например, первое правило говорит о том, что на каком бы берегу ни находился фермер до переправы, его пслакенне после переправы будет другим (У'ч г"), а асс остальные обьекпя рассмотрения оспшутся нагом же берегу, где н были: (х' и) л(й'нй) г (с'нс) . Обозначив заме()г) функцию, которая приравнивает все штрнхованные и нештрнхоаанные переменные из мноямства г', получим следующие характеристические функции для указанных выше правил: рлаев за Эта лр Крипш ходов 1О.4 стр) Состоя чений р =(ы~ чення чика.( мшкно (значе1 таким иа тои шения состоя ляст ь уловке Хш(те) =(У'и-зз ) издам((мбс)) ' У феймеР пейепйавллетсл сам Хлз(за) (з'и-р)л(з мю)л(ю'и ю)леаве((бс)) //везеттольковолка Хяз(з з ) — (з н ~)л(/ Я)л(Я и Я)лилие((ю с)) П виюттолько козУ Хм(т,з) (Ети-зР)л(~ис)л(с'и с)лизше((юб)) Нмзсттолько Все разрешенные правилами переходы возможны, поззому булеза функция, опнсываклцая возможные переходм в втой системе, есть дизьюишпш всех четырех хврмпернстнческих функций переходов: хл(з з) хачхлз абхаз ~хя4 Рис.
1ФД Вену хврекшристической булевой фукалки мложества лерехоясе Хяе(т, т') = (у ' и -зз') лизам((ю,б,с) ) прсблнеы:"фермер-волк-коза-капуста" не при Опера' ру соо штрих напрев ннй, в кажды мю эгб лка зу ция, мех Эта просим булева функциа задаст все 40 возможных переходсм струкгуры Кринке, представлмощей проблему. В00 характеристической функции пере- ходов уя, (г,т') для первого правила представлена на рис.!0.3. 10.4. Представление булевыми функциями структуры Крипке для программ Состояние программы — это мгновенный снимок, залмоший множество зна- чений всех переменных программм и значение счетчика команд Рс.
Пусть Р = (гп тз, тз) — множество программных переменных, принимающих зна- чения в .О» т,е.0„а РС вЂ” мншксстао всех значений программного счет- чика. Соспжние з е (РС, Р), з = (Рс ь- шэ, т~ т- 5; тэ е- 3, тэ 4- б) можно предсгвюпь предикатом, т.е. функцией из некоторого мвжмства гзначений векторов программных переменных) в мнохсество (пяе,,майе» г (Рс шз)л(тг--5)г(та=3)п(тз=б), Таким образом, состояние программы можно задать предикатом, истинным на том конкретном состоянии, на котором выполняются указанные соотно- шения.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
