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

В главе 2 вводятся темпораяьные логики ЬТЬ, СТЬ и СТЬь и рассматривается их использование для спецификации свойств поведения реагирующих сис- Главы 3 н 4 посвящены изложению алгоритмов проверки модели для сдучдев, когда проверяемые саойспа системы вырюкены формулами логик.СТЬ и ЬТЬ. В главе 5 научаются системы переходов как модели реагирующих систем. Глава 6 посвящена рассмотрению свойств реагирующих систем и шг классификации; безопасносш, жишюти и справедливости. В главе 7 описываются некоторые примерм верификации с помощью представленной ранее методики проверки модели.

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

го метода. Данную главу можно изучать независимо от других глав, но этот материал является основным для.рассмотрения в слезблошей, 10 гпгее, символьных алгоритмов верификации, позволяющих анализировать систамы д астрономическим числом состояний — !О™ и более. В амме !1 изучаются подходы к анализу количественных свойств дискрш.- ных систем — вероятностных систем и систем дискретного времени. Здесь рассматривается, как проварить свойства, выраяпюмые утверждениями типа: "с вероятностью, не меньшей 0.99, на переданный пакет будет получено подтверждение не более чем через 6 единиц времени". Наконец, шааа !2 посввщена проблемам верификации систем реального времени. Пракшческвя часть курса состоит из двук компонентов.

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

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

Благодарности Материал книги основан, прежде всего, на фундамеевльной монографии Э. Кларка, О. Грамберга и Д. Пеледа !341 которая во многих университетах мира является баммым учебником двя курсов по верификации и пкх!е! сйесвлй. В кинге использованы также материалы из руководств, оригинальных статей и многочисленных учебных материалов, доступных в Интернете. Недавняя монография Крисгела байера н.

Питера Катоена по принципам линзе! сйесЫМ ! 19! также была использовав при подпповке книги. Автор вырвквет огромную благодарноеть июм людям, которые предостввилн в Интернете в открытом доступе свои статьи, курсы лекций, слайды презентаций на зту тему. Всех их трудно перечислить, но особую благодарность хотелось бы выразить Марте Квяткопской (Мыта Ки(архозчз(га) из Бирмннгемского университета, Борису Коневу из Ливерпульского университета, Юрию Лифшицу из Калифорнийского технологического университета, Питеру Катоену ()поз!-Рююг Квгоеп) нз университета Аахена, Киму Ларсену (К)ш бцЫзцапг( !.жзеп), Полю Петерсону (Ран! Рейагвзоп), Пьеру Валперу (Рмтге гт'о(рег) и многим другим.

Автор читает курс с этим названием в Санкт-Петербургском политехническом университете уже (О лет. Изложение множества вопросов, казавшихся асными, многократно перерабатываъкь после того, как на экзаменах выяснялось, что эти вопросы вызывали затруднения у студентов.

За эту обратную связь автор приносит благодарность своим студеншм. Ихпание книги полдержано Я. Ю. Карповым, за что автор приносит ему осо. бую благодарность. главА 1 Проблема верификации В атой главе обосновываешя нсобходимосп, верифиищни программ. Приводятся примеры тшкелых последствий программных ошибок в системах для критических применений, от кон!шел все больше зависят жизнь и здоровье людей, использующих технику.

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

Сложность промышленных программных систем все время возрастает, Например, ОС М!симой Рйпдомз 3.1, разработанная в 1992 г., содержит около 3 млн строк кода, Мююзой тт!одопа 98— 18 или строк, йедНа! (лонх6.2(2000г.) — около 20млн строк, йедНа! ! блох 7. ! (2001) — уже 30 млн строк, Мюговой !т'шдои'з ХР (2002) — 40 млн строк Мысленно охватить функционирование таких систем не, в состоянии ни один человек даже при использовании современных технологий н методов абстрагирования и управления сложнооп ю. Сложность разрабатываемого прогрмемного обеспечения подошла к границе его понимания и, следовательно, его управляемости.

Число потенциальных ошибок в программных системах постоянно растет. Например, в ОС %г!в)овн 95, по оценкам М!сюзой, до сих пор осшежл несколько тысяч ошн- 14 Глава г бок. Но эта ОС используется в бытовых персональных компьютерах, от нее не зависят жизни людей. Только сумасшедший шктавнт эту ОС в бортовую систему управления самолетом илн даже автомашиной, Особенно подвержены сшибкам параллельные, распределенные н многопоточные программы, которые характерны лля бортовых систем управления. Хорошо известно, что даже в тех случаях, когда функционирование кшкдой из параллельных взаимодействующих компонентов системы абсолютно ясно, человеку трудно понять работу всей параллельной системы, процессы в которой взаимозависимы.

Как пишет Лесли Лампорт, "очень легко ошибиться, когда делаешь утверждения о последовательности событий, происходящих в параллельных программах" 1941. Причина этого, по-видимому, в том, что человек в кюкдый момент может лумать только об одной вещи. Параллельные системы, которые работают правильно "почти всегда", годаии могут сохранвть тонкие ошибки, проввляющиеся в редких, исключительных снгуациях. Такие ошибки обычно невозможно обнаруюпь тестированием. "Существует обширный печаяьный опыт того, что пвраллельные программы весьма упорно сопротивляютсв серьезным усилиям по выявлению в них ошибок"; — писали Сьюзен Овицки и Леслн Лампорт еще 25 лет тому назад [1211. В результате все чаще компании подвергшотся штрафным санкциям и вынужаены выплачивать неустойки за последствия ошибок, проявившихся после передачи готовой системы заказчику.

Человек не любит рассказывать о своих ошибках. Разработчики программ обычно не спешат уведомлять всех о своих неудачах. Ни одна компания, производжцая программы и компьютерную аппаратуру, не склонна без особой надобности объявлять об ошибках в своих продуктах н их последствиях, Это одна из причин того, что ошибки в программных и аппаратных системах происходят значительно чаще, чем мы об этом узнаем. Только в случаях, имеющих серьезные последствия ошибочного поведения программ, проводится аныгнз причин ошибок и возникших из-за них потерь, Те результаты такого анализа, которые становятся широко известными, показывшот, что материальные последствия ошибок в программных н аппаратных системах управления могут бмть весьма значительными, порой приводящими к полному провалу дорогостоящих проектов и лаже к.

ркюрению компанийрвзработчиков ПО н аппаратуры. Вот некоторые наиболее впечатляющие примеры последствий ошибок в программах. О 4 июнл 1996 г. при первом запуске на 39-й секунде после старта взорвалась ракета "Ариан 5". "Ариан 5" — зто аналог российской ракегыноснтеля "Протон", которая разработана н производится Европейским космическим агентством. Бортовая сиеюма ракеты "Ариан 5" использовала ПО предыдущей версии, "Ариан 4", но архитектура аппаратной части была модифицирована. После проведенного тщазвльного расследования было установлено, что причина аварии — ошибка в навигационной программе бортового компьютера.