2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 38
Текст из файла (страница 38)
как это описано в сь 4. Если язык, принимаемый этим автоматом, пуст (т. е. процесс сечет не завершится или ие проходит бесконечный цикл с особой мепсой ассерс), то исходное требование удовлепюряегся — нежелательных поведений у анализируемой системы процессов нет. Если юык непустой, то он содержит пещь жиля, которые в системе нежелательны. Это будет найдено в случае, если процесс сечет зввершится (т. е. придет в свое завершающее состою)не и в ини останеюя или будет проходить цикл с ыеткой *ссерс), Выходом сисшмы верификации являешя или утверждение, что исходное требование удовлетворяется нли, если оно ие удовлетворяется, Зр!и выдает примеры нюкелателыннь поведений: запускается интерактивный снмулятор, который позволяеп шш)наяьио представить последователыакть шагов выпоянеиия алгоритмое мщйм лей и посылаемых при этом сообщений, приводящих к ошибочной траекгорни поведения (см.
Рис, 5.12). Модели, представленные на языке.ргоше!а, всегда ограниченные. Поэтому ° се свойства корректности автоматически становятся формально разрешимыми внутри ограничений, которые установлены размером программы и вычислительными ресурсами, доступными вернфикатору. Очевилно, что асс системы верификации имеют физические ограниченна, которые определяются объемом памяти, скоростью процессора и т. п. В системе Зрш используются несколько приемов, позволяющих бороться с проблемой "взрыва числа состояний" н увеличнгь размер тех сисшм, дяя которых возможен нсчеряиь вакхцнй внвлгм.
Число состояний сисгемы переходов растет экспоненцнально с ростом числа процессов н ростом числа переменных. Существуют различные методы борьбы с этой проблемой. Один из них — это использование эффективных методов представления данных с помощью бинарных решмощнх диаграмм (ВОО) и методов символьной верификации, о чем пойдет речь в гл. 9 и 10. Другое решение используется в системе Зр(и; здесыюлного преобразования системы процессов в структуру Кринке не производитса: проверка выполнения свойств системы производится "на лету" (оп-йе-йу), только для части построенной системы переходов, которая постепенно достраивается в ограниченной области памяти.
Другой метод уменьшениа числа состояний асинхронной композиции моделей при их верификации — зто так называемая "редукции частичных порядков" (рапншй оп)ег шдпсбоп). Редукция частичных порядков состоит в том, что при верификации часть всех возможных путей (всех полимх порядков частично упорядоченного множества операторов параелельной системы) отбрасываекя. Например, интерлнвинг (перекрытие) операторов, работмощих с локальными даннымн в каждом процессе, можно моделировать только одной последовательностью их выполнения; все остальные перестановки выполнения этих операторов будут эквивалентны с точки зрения любого проверяемо. го свойства.
Этот прием позволяет системе верификации Бр(п существенно снижать сложность проверяемых моделей паршшельных систем. $.7. Построение структуры Крипке Юя программ высокого уровня Вебщем случае, программы не являются системами с конечным числом солющщ(ь Вещественные переменные, динамические структуры данных, диемвившское схплание параллельных потоков, указатели — все это требует потенциально бесконечного числа состояний. Поэтому корректность программ, написанных на языках высокого уровня, в общем случае доказать невозможно.
Например, такаа частная проблема верификации, квк проблема осталова, якеяется аагоритмическн неразрешимой. Для верификации программ необходимо построение конечной модели системы с помощью процесса абстракции. В такой модели некоторые свойства программы, содержащей параметры с бесконечной областью определения, не сохраняются. Очевидно поэтому, что не все реальные свойства программ иогуг быть проверены с помощью метода воде! сйесЫпй. Построенная для верификации модель должна быль достаточно мала, побы ее мшкно было анализировать с помощью систем верификации, но в то же время достаточно содераатчлыщ чтобы отразить существенные свойства шжедения программы.
С др ходи врон решь В по сзед~ быль (еррз реал! иуяо зюй прог( свой то лр резул рию ~ нсхоз даннг ходи< (мене строе проке впали Пелся ции, ~ грамь дуюш приьк Удбй кации свойс мы м~ томат затер центр руемо маши~ числе| ~ числа г борь:мсто(В(У()) '(ругов ктемы гнення гн по- грани- иоде- юрядм, что в час. ггбрацнх с здной юлне- яемогенно и со, диЙует про. ь не- лема зсте Ютаа я, не ~ мог ас- ана> согмы.
С другой стороны, в модели всегда пояшшются свойствц которых нет в иг ходной программе. Абстрагирование обычно выполняется чеяовеком, этот процесс требует опыта, креативности, пониианив сути проблемы, которая решается с помощью алгоритма. В последнее время ведется интенсивная работа по сознанию методологии последовательного угочняющего процесса абстрагированиа, который может быть автоматизирован. Например, в рабоге [34] описан метод автоматическо. го построения по реаяьной программе Я такой ее аппроксимации (о(Я) (оррег арргоишагюп), которая попускает большее количество поведений, чем реальная программа Если любое свойспю программы Я, выршкенное формулой чг некоторого ограниченна темпорвльной логики, выполняется для згой аппроксимации ло, то это свойство цг выполняется и для исходной программы Я, потому что все поведенля Я присутствуют н в Ао .
Если же свойство чг не выполняется на абстрактной модели, и выджтся контрпример, то проверкой контрпрнмера на программе Я можно получить один нз двух результатов. Если выланный контрпример представляет ошибочную траекторию поведения программы Я, т. е. проверяемое свойство не выполняется для исходной программы, то необходимо эту программу исправить. Если же выданный контрпример представляет поведение, которого не существует в нцкодной программе, то в этом случае необходимо построить более точную (менее абстрактную) аппроксимацию программы, чтобы зто поведение в построенной аппроксимации не присуютвовало.
Построение более точной аппроксимации также можно выполнить автоматически и для нее повторить анализ. Подобный подход используетса в несхольких опьпиых системах верификации, которые могут автоматически стронгь абстрактное представление программ непосредственно ю их записи иа языках высокого уровня для последующего айалнза этого абстршггного представления. Рассмотрим несколько примеров. УАЗМ (т'ш Апобгег Зойнцге Моде! с(мс(сег) — шшдемический пакет верификации, разработанный в университете г.Торонто.
Он позволяет прове)ипь свойства, вырмкенные в логике СТС у программ, написанных на С, Программы маус включать и рекурсивные процедуры. Верифшштор использует автоматическую технику абстракции. Латаразйр(пбег (ерй). Этв система была рюработана в исследовательском центре Ашез ХАЗА. Система проверяет выполняемый )ага.байткод анализируемой программы.
Эту систему можно рассматривать как виртуальную )ага машину, систематически исследующую все потенциальные траектории вычислений анализируемой программы, написанной на )ага. В пакете )РР про. Слева Э верястся только ограниченный набор свойств прогреми — достижишють неаоторых состояний, блокировки процессов н необработанные исключения. С 1999 г. система применялась дяя проверки свойств многих академических и промышленных разработок, и особенно полезным свойством этого пакета разработчики счмпиот нахождение возникающих в параллельных взаимодействукицих процессах тонких ошибок, не выявляемых стшцпртными методами тестирования и отладки.
Я чМ вЂ” этот пакет Разработан фирмой "Майкрософт" для верификации драйверов, написанных на С. С помшцью пакета проверакптл свойства безопасности, т.е. те, которые могут быль найдены на конечных траекюриях программ (см ез. б). Разработчиками построено около 60 типовых шаблонов— правил — параметрически настраиваемых формул темпоральной логики, которые должны проверяться лля вновь разрабатываемых драйверцв, работающих под управлением ОС 99(пбомз. В этих шаблонах зафиксированы требования к сценариям взаимодействия внешних устройств с ОС %1пдовм.
$.8. Заключение В абстрактную модель (струкгуру Кринке) перевод из реальной системы обычно неформален н чшце всего неоднозначен. Структура Кринке — это система переходов с конечным числом сосюяний, поэтому очевидно, что в структуре Кринке многие свойства системы, содервшщей параметры с бесконечной областью определения; не сохраняюгсж Следовательно, в общем случае не все свойства реальных систем могут быль проверены в такой модели.
Поэтому зта техника верификации более удобна в применении к системам, в которых главную роль играет поток управления, а не обработка данных, поскольку обычно обрабатываемые даннме приниммот значения из бесконечной области определения, и построить адекватную модель таких программ обычно значительно труднее. С помощью техники тоде! сйесЫпй проверяется ие правильность преобразования данных, а сеойсмеа лоееДекня программ, и с этой точки зрения для большого класса систем возможно построить такую модель (обычно зто так называемый снищюлизацмонлый скелеш лараллелылгй грхмрпммы), чтобы существенные аюйсзва поведения, интересующие разработчика, сохранялись в модели. При построении молелн Кринке ля лля реальной смстемы Я необходимо решить следующий вопрос: что опрелеяяст шаг эволюции сиогемы, т. е.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
