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

Вывод отчета заключается в том, что традиционное тестирование приносит мало пользы при разработке тысого сорта ПО, шжволяя проверить только ничтожную долю поведений системы. В отличие от тестирования, верификаццв позволила здесь систематически проанализировать полное пространство состояний системы, найти сущеепюнные ошибки рюработкн в нескольких версиях продукта. Возможность нахождения ошибок на ранних стадиях разработки позволила компании сзкономшь значгггельные средства. Авторы пишут, что стоимость испраяшения одной ошибки, оставшейся в ик продукте после разработки, составляла бы сотни тысяч долларов. В [144] приведены результаты верификации стандартного арбитра шины Рийиебш. Пугь новых методов верификации к признанию в промышленности не был прост. Например, для того чтобы убедить скептиков.разработчиков бортовых , систем в необходимости использования верификации как важнейшего этапа технологии разработки, группе из Исследовательского центра Ашез корпорации НАБА выполнила специальное исследование [б7).

В его рамках был проведен фориальный анализ с помощью системы верификации Яр!и многопроцессного ПО бортовой системы управлениа космическим аппаратом в проекте Оеербрасе 1 для полста к Марсу. Было обнарулсено множество ошибок рюрабстки, не выявленных методами, использующимися в стандартной технологии разработки ПО. По признанию разработчиков, четыре из этих ошибок окюались критическими, Они могли проявляться очень редко, но их мкь никновение привело бы к опшзу системм (ш[ззюп-!гй[ег епогз). Все они были не примитивными описками нли логическими ошибками, хармггернымн дия последовательных программ. Эти ошибки проявлялись лишь в результате непредвиденных разработчиками перекрытий операций параллельно протекающих процессов.

В цеицю Ашез продолжаются интенсивные исследования в этой облжгн [55). Результаты подобного, нсследованив были представленм недавно фирмой йоскмей Сойим, мировым лидером в разработке авиационной электроники, мобильных и борговых коммуникационных сипим для коммерческих н военных применений [108]. Годовой объем продвк компанией этих систем составляет несколько миллиардов долларов.

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

Все основнме производители программных и аппаратных систем; 1пге1, 1ВМ, !Чогш!, Могого[а, НР, Садепсе, рюкна ыые лив.ров. нны был ~вых ора- иро- яро- оекгбок тех'ши ыли лля ~ния мой ики, зль- гнк- зен!. ных ги в :елн НЕС, Вой (лйз, б!еюещ (лсепС Тесйвойгй(ез, бнп и многие другие имеют в своем составе ~Руины, выполняющие верификацию проектов. Несколыю лет нюад компания 1пм! дшке объявлялв о приеме нв работу каждого, закончившего обучение по программе РЬ.О. в области формаяьиой вернфиг кации.

1.б. Инструменты верификации Многие крупные компании-производители схем н встроенных систем разработали свои системы верификации, которые встроены в технологический производственный цикл. На рынке существует несколыю коммерческих систем верификации, поддерживаемых разработчиками, например, СЬгузайз, Яупорзуз, Чегузуз, Саг)епге. Разработанный фирмой Мюгозой верификатор Бщг!с Оптег Чепйег постввяяекя вместе с системой поддержки разработки драйверов для ОС Ч!ик)отгз ()Ч!лоопа Пгвег Вече!оршеш КЬ). Построенный верифнкатор может нспользоватьсв кмкдым разработчиком драйверов дяя этой ОС.

Эта работа была отмечена Биллом Гейтсом в его торжественной речи на сткрьпни конференции ООРЯ.А в 2002 г. квк серьезное дости:кение компании. Существуют также системы верификации, распространяемые свободно. Они разработаны с исследовательскими цеяями, главным обрезом, е универсмгетах. Это система ЗМЧ, разработанная в университете Карнеги-Меллон, система ()РРАА(., разработанная и совместно поддерживаемая уннверснтещми Уппсалв и Аалборгв, система РЕ(ЗМ, ратрабошннял в Бнрмингемском университете, система Бр!и, разрабочннная в Вей (лбз, и многие другие. Примеры верификации в данной книге будут приведены на взыке Ргоюе1а — входном языке инструментаяьной системы верификации Зр!л, разработанной Джерардом Холзманном, работавшем в то время в Вей (лйз.

Система бр!и достаточно проста, она используется во многих университетах мира для обучения студентов анализу параллельных процессов и практическим мегодаы верификации. В то же время с помощью этой системы были вернфициромшы используемые на практике протоколы коммуникации, стандарты протоколов, модули операционных систем, бортовые системы управления. Приведем в заключение ссылки на некоторые свободно распространяемые инструменты верификации. (2 БРйч — Вей 1вьз — (параллельные взаимодействующие прпцессы) Ьпрпусш.бей-!айз.сош)сю(сз/мйвг(зр!пl (2 ПРРААŠ— ()ррза)а 1)пвегзйу и Аа!Ьогй Пп!чегзйу (системы реального времени) Ьцр:/Ачпм,досз.пп.зе(боса(пшч(вррея(( П Ч)З вЂ” (/и! Вегйе)еу, 0п! Сойпвдо Ьцрг//т!зйсо1опкЬ»дв/-т!з/ П ККОХОЗ вЂ” ПЧК1А (системы реального времени) Ьц(х//пмтбппа1рез. Ь/тазу/ст(р/зойтте/9!ьс4иопоз,йпп1 П НУТЕСН вЂ” Сотне(! (/с!тат!гу (линейные гибридные системм) Ьпр://ттт,Ьевзгпйег.сош/топ!Ьа/ЬугесЬ.Лтт1 П ЗМЧ вЂ” Сашей(е Мейоп (/п(тем!!у (ЗутЬо!ю Моде! Чег(йкяи» ) Ьцр://ичит.сз.стнлдн/-шсде1сйееЬ/мвт.йцп1 П ЗТер — ЗтпКогд (/п!тем!гу (Зшпрсгд Тетра/а/ Рготег) Ьцр://тВ'ю"ыер.згю(огд.ю!и/ 1.7.

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

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

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

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

Тестирование и верифиющия валяются взаимно дополняющими подходами к повышению степени доверия к системе. 1.8. Замечания ся гр)я- ой !ь)'т :м и ге гх со ъ На форуме АСМ (Ьцр://саг)еи.пс1лс.пй/В)зйз/) собрана информация о тысячах случаев отказа техники по причине ошибок, допущенных при разработке ахюмнпмированных систем, от олгаза системы бронирования билетов буЬег до гибели ребенка в автоматизированном туалете. Подробный анализ причины аварии ракеты "Ариан" и обсуждение возможных действий по выявлению е программах подобной ошибки приводятся в [172]. Описание неполадок бортовой системы зонда Гюйгенс приведено в [178]. Проблемы с советскими станциямн "Фобос-1" н "Фобос-2" описаны в [175]. Анализ ошибок в процессорах АМО РЬепоп (Вмсе)опа) и Оргегоп и нх возможных причин приведен в [176].

Ссылка [18Ц указывает на текст, посвященный изложению проблем с системой управлеииа в аппарате Тйегас-25. Информацию об ошибке в программе наведения ракеты Раггюг можно найти в [!7Ц. Выводы комиссии по расследованию причин "дружественного огня" изложены в [177]. Некорректность параллельной программы разделения множеств доказана в [165], там же определены классы исходных множеств, на которых программа работает искоррекпю.

Протокол «/.СЛ.упсй, рассматриваемый в ягой главе, приведен в [105], анализ его некорректностей описан в кинге [79]. Впервые задача верификации программ была вютавлена Робертом Флойдом (КоЬегг Р1оуб) в [50] н формализована как проблема доказательства теорем на основании аксиом и правил вывода Энтони Хоаром (С.А.К.Ноаге) в [68]. Метод воде! сйесилб для верификации параллельных систем с конечным числом состояний был впервые предкожен в 1981 г. Эдмундом Кларком (Ряйпшгб Пвгйс), профессором университета Карнеги-Меллона, и его аспирантом Алленом Эмерсоном (А1!еп Вшмзоп). В работе [29] они писали: 'Тлобальный граф переходов параллельной системы может рассматрнватьса как конечная структура Кринке, и может быть построен эффективный алгоритм для определенна того, яваястся ли эта структура моделью заданной формулы (т.е.

определения того, сопгвстствует ли программа ее спецификации)". Ими жс гквев з был введен н термин пин!е) сйесипй. Дмозеф Снфакис ()озерй Б!(вк(з), основатель и директор лаборатории ЧЕК(МАО, французского исследовательского щщтра по разработке встроенных систем, был руководючлем научной группы, разработавшей первую систему автоматической верификации методом проверки модели [129].

Эти работы в немалой степени способствовали тому, что именно во Франции сушесщует лучшва в мире авионика и технологии разработки бортовых информационных и управляющих систем. Недавно в технологию фирмы 3Ъа)ез, крупнейшей компании по производству авиационной электроники, внедрен инструментарий дяя разработки систем на основе моделей, твк называемые мО(з гоо1з (моде( Оптеп ()ете)оршепг тоо!з). Именно с этой компанией Российский авиапром заключил многомиллионные контракты на поставку авионики [95].