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

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

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

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

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

На рнс. КЗ представлена общая схема вернфикацми. Компоненты этой схемы должны удовастворять очевидным требованиям. Желательно, чтобм модель, представляюнмл систему, была достаточно выразительной, чтобы с ее помощью можно быяо представить поведение параллельных процессов и их Иег гееаенкам ие йа, мнить мигаем ° иясмэас1св ке мсяеии -,Мсвямессаат твваоьавме| аоитвпеммеи Рис. 1.3. Обшвя схема верификации 5оро ук- раых юй вы. на мы ль, пс- их взаимслейсгвне. Дяя снспм реального временн важным моментом ввлявгпя возможность включения в модель временных ограннченнй, для сгохжтическнх систем — возможность учета вероятностей событий. Янек спецнфнкацни для формулировки требований к поведению системы должен быть вырюнтельным, мощным, интуитивно понятным, позволяющнм достаточно просто выразить широкий класс важных свойств поведения системы.

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

Дедукмнеиая верл$акапзм — это проверка цравнльносгн программы, которая сводится к локазательству теорем в подходмцей логмческой системе. Это направление разрабатывается уже более 40 лет, с тех пор, как Роберт Флойд н Энтони Хоар впервые формально поставили проблему доказательства корректности программ. Вернфнкацня программ здесь проводится дедукцней нв основе аксиом н правил вывода.

Эта весьма сложнав процедура не может быть полностью автоматнзнрована, она требуег участия человека, действующего на основе предположений н догадок, использующего ннзунцню прн построении ннаврнантов н нетрнвнальном выборе альтернатив. Проверка экеквпяелткости сввзана с разработкой формальных моделей взаимодействующих процессов, выражением в рамках таких моделей как спецнфнкацнн, так н рпшнзацни, и проверкой эквивалентности поведений формалыю определенных моделей поведения. Это направление было начато работами Рабина Мнлнера разработкой нм алгебрм процессов Псчнсаеюм езаимодейслмующнт сломам (Св(айвз от" Сощщвп(свбнй Зузмщз, ССБ) около 30 лет впздд, гаева з Метод воде! сйес)ппй связан с формальной проверкой выполнення нв модели реалнзацнн свойств поведения, специфицированных на языке формальной логики.

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

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

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

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

может выполняться без участия человека, с использованием так называемой "тгзпалсгкп вазкатил кволхи", розй4зпцоп Ысйпо)ойу). Обсуднм происхождение термина пюре! сйесЫпй. В формальной логнке илжервревиявей логнческой формулы Ф называется объект, на котором формула принимает либо нстннное, либо ложное эначенне. Те интерпретации формулы Ф, на которых Ф принимает нстннное знвченне, называютсв МОДЕЛЯМИ логической формулы Ф. Напрнмер, в логике аыскпзыеаввй множествюм интерпретаций формулы Ф(рпйг) являются пли ной мо- илн ись ро гли О Определение з.й тиеноальнва линю Гся ° е. к(е1 тке ре- нязля ~ые ае- чо- ейср ыу ню )н. е.

юй наборы истинюктных значений атомарных (элементарных) высказываний р,о,г, например, <р=«тге,д 1а)зе,г «ъе>. Те наборы истинностных значений <р,о,г>, на которых Ф истинна, являются МОДЕЛЯМИ формулы Ф. Для темпоральной логики, используемой для спецификации свойств поведения систем, множеством интерпретаций ее формул является множество слезем переходов; на квяаой сисгеме переходов лз любая темпоральнвл формула Фпрннимает либо истинное, либо ложное значение. Те системы переходов, для которых темпоральнаа формула Ф петиных являются МОДЕЛЯМИ формулы Ф.

лйк(е( сйесйлй (буквально: проверка модели) — это влгоригм, прове- ряюгний, будет ли заданная логическая формула Ф истинна для данной системы переходов лг, т. е, будет лн лг моделью Ф (рис. 1.4). ик аваеегвчюкз -н аи фее тл б Риг.