2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010).djvu), страница 8

1.4. Системы переходов квк повели темпоральных формул Поскольку система переходов валяется выделаю верифицируемой системы (проюкола, программы, схемы и т. п.), то часто термин ваде! сйесЫпй понимают как 'проверки на модели". В лнгературе можно встретить как ту, так и другую тракговку, хотя исследователи, впервые разработавшие алгоритм воде! сйесй(пй, имели в виду первую. Для выполнения верификации методом воде! сйесЫпй нужно построить для программной системы адекватную модель с конечным числом состояний, представить ее на вхолном азыке автоматизированной системы верификации, а таске выразить подлежащие проверке свойства формулами темпоральиой логики.

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

Возникмошая при этом проблема называется проблемой взрыва числа сосьтоллай (я!вы ехрймюп ргоЫеш). То, что меюд воде! сйесЫкй сегодня успешно применяется к разрабатываемым реальным системам, валяется следствием того, что были созваны методы эффективного представления данных (так называемые снмжзльные методы) н соответствующие алгоритмы верификации, позволяющие в значительной степени решить проблему взрыва числа состояний и выполюпь методом любе! сйесй(пй верификвцюо систем с громадным числом состояний — )Оке и более.

Всем этим вопросам посвящены слелующие рюделы книги. 1.4. Тестирование и вериФикация Наиболее очевидным н широко распространенным методом проверки правильности систем является тестирование — проверка рабаты построенной системы а различных реальных снзуацивх, при рюличных исходных ланных. Тестирование имеет множество преимуществ: О проверяется реавьная система, а не ее модель; (э проверка может быть выполнена в реальной среде с реальными интерфейсами; (э проверять можно реальные наиболее опасные или часю используемые режимы работы снстемм.

В то же время у тестирования есть и недостатки: 0 тестирование очень трудоемкий процесс; шы еи- жн нтм для гий, шн, ной гью :ис- ний кло мой эбе! юге ре бпй зрелой ~ых. мыс П тестирование выполняется на поздних этапах разработки системы. когда модули системы уже реализованы, поэтому исправление найденных ошибок очень дорого, прн исправлении часто вносятся другие ошибкш П все реакции системы при выполнении тестов доикны быть заранее зафиксированы; П тестированием можно провершь лишь очень немногие траектории вычисления системы (а нх обычно бесконечное числой П тестирование сложных систем трудно автоматизируется, обычно тестирование выполняется с помощью низкоквалифицированных программнстовтесшров, сопоставляюших реакцию тестируемой сисгемы с желаемой реакцией; П тестирование не макет гарантировать правильность сиегемы: знаменмгый тезис Э.

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

Однако и у верификации есть раа недостатков: П главным недостатком верификации является то, что проверяется не реальная система, а ее абстрвктнав модель. Такая модель мшкет быть неадекватной, не сохранять существенных черт исходной системы, и в этом случае проверка спецификации лля модели не выявит ошибок, имеющихся в реальной системе. С другой стороны, в модели могут появиться свойства, которых в реальной системе не существует. Таким образом, ценность резуяьтатов, полученных при верификации, напрямую зависит от адекватности модели и, следовательно, от уровня профессионализма человека, строящего модель; П язык специфиющнн свойств сисгемы может быть неполным, недостаточным для формулировки всех желаемых требований к поведению системы. Выполнение любого множества проверок системы в этом случае не гарантирует ее правилыкктн; С) сама автоматизированная снстема мрнфнкацнн макет содершпь ошибки; ьу поскольку невозможно формально определнть, что означает "наянсе ошсушсшене оилгбок", вернфнкацня так же не может 'пщантнровать абсолютной правильности сисгемы, как н тестнрованне; (У несмотря на то, что сущсственнш часть процесса вернфнвшнн обычно автоматнзнрована, выполнение верификации требует достаточно высокой квалификации персонала.

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

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

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

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

ые из заых ых гн.)с 1а- чь~не ,в но ,ме яи-- ц)н ~ые ре ~но ис- зба 1.6. Примеры успешной вериФикации систем Методы верификации, объединенные под общим названием воде! сйесапб, быстро прогрессируют. Еще совсем недавно, в книге С. Ойшхй М. )шауеп', Р. Мшгдпо!1 "рппбашепш!з о( Зойчгые Епб!пеег(пб", изданной в 2003 г., метод шоде1 сЬесЫпб харакшрнэоввлся как "новый метод верификации, который позволяет получить доказательство коррекгности в некоторых простых случавх".

Однако уже сегодня этот подход к верификации изменил технологию промышленной разработки ПО. Применение методов формальной шрификации как этапа в промышленной технологии разработки программных систем началось в конце 90-х годов прошлого века именно с метода любе! сЬесапб, который оказался чрезвычайно удобным и эффективным (созг екесбте) иа практике.

Приведем не. сколько примеров. В работе !21] на основе опыта использования верификации в двух разработках аппаратуры (ЯРО ыодуль паматн и маркерный контроллер) был сделан вывод о возможности промышленного использования этой техники длв. повышения уровня доверия к разработанным продуктам. В работе (80) Дж. Холзмаин (Оешгд По!ппапп) перечисляет ряд значизипьных результатов, которые к тому времени (более 10 лет назад) быки достигнуты в области верификации реаяьных систем с помощью сисшмы верификации Зр(п.

Среди представленных примеров — СжпЬпдйе ппй рпносо1, 1ЕЕЕ (пб(са1 ).шц Сои!го( ргонко1, Ы.С 302.2, фрапиенты больших протоколов ХТР н ТСРЛР. Другие примеры успешной верификации — контроллеры, тказоустойчивые системы, протоколы доступа к шинам, протоколы контроля ошибок а аппаратуре, криптографические протоколы, протокол Ебюшш Сой(зйш Вто)бшгсе, протоколы самосгабнлизации. Монография [113) приводит примеры верификации систем с более чем 1О™ состояний с помоппю симвсльнмх алгоритмов системы верификации ЗМЧ. После завершения одного нз проектов в компании 1лсЬЬеед Мыт!и было отмечено: "Формальная верификация позволила найти несколько тонких ошибок, которме, скорее всего, были бы упущены в процессе традиционного тестирования". В отчете 2002 г, компании 1лсепг Тесйпо!об(ез рассказывается об опьпе использования корпоративного верифнкатора Чепбой для систематической верификации библиотеки обрабапги вызовов протокола СОМА лля беспроводнык коммуникаций.