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

Проблемы с прелставпеннем булевых функций..., 9.2. Бинарные решающие днвгранмы 9.3. Свойства бинарных решающнх диаграмм ...................,.................................,........ 308 9.4. Операцнн над В00 .. . 312 9.5. Проблема булевой выполннмостн (БАТ) н бннарные ршшнощне днаграммы ....328 9.6. Применения В00 к решенню лагнческмх н комбннаторных задач ...,...........,.....

330 9.7. Использование В00 в анакнзе н сннгезе логических схем 9.8. Конечные структуры данных н В00 Прелставленне отношений с помощью харакгернстнческнх булевых функций ..................,.............................,..„„............347 Операцнн над отношеннямн ............., .....................„„... 349 9 9. Символьные н неявные алгоритмы обработкн данных .......................................

355 Прнмер символьного алгоритма: анализ достпжимастп на графе ...............,....... 356 930. Бинарные решшощне лнаграммы с подвшеннем нулей.......,......,................... 358 9.11. Закшоченне..., ..............,..., ................................................... 363 9.12. Замечання, .....................,.........364 9.13. Задачи к главе 9... 366 Глава 10. Свмвольвав аервфвкаввв ......-........,........367 10.1. Необходимость символьных методов в аернфнкацнн 368 102. Представление структуры Кринке булевымн функциями 370 10.3. Предсгааяенне структуры Кринке реагирующих систем булевымн функпням н без предварнтельного явного построения струкОры Кряпке .........

372 1О 4. Предстаыенне булевыми функциями струкгуры Крнпке для программ ...,.....375 105. Символьный аягорнтм воде! айес1гшй дяв СТ).......,.......................................... 380 10.6. Операторы на мншкесшах н неподвижные точки ....... ! 07. Теорема Тарского о неподвижной точке... Решеткн. ..... 385 ..... 390 ..... 392 10.8. Символьный алгоритм вернфнкацнн шгя формулы Ерр..........

10.9. Определенне темпорвльнмх формул СП. через нешцшшкные точ!ш оператороа.... 10.10. Звкяюченне 10.11. Замечания .. 10.12. Задачи к главе 1О ... ...395 .......,........403 .................. 4 ! 0 ................ 4 1 1 .................. 4 ! ! Гаава11.Колвчествеввыйавалвзевстеш .........= ...,.......415 11.1. Вероятностный метод любе) сйесй!пй ......,.....,...,.....,.......,.......,.............,...4! 6 1! 2. Вероятностная латыш ветвяшепкя времени !Рта!ябййвю СП РСП.) н вернфнквння вероятностных попелей .................,............................................

427 11.3. Проверка свойств, ювнсящнх ат дискретного времени и вершццесгного выбора...,....,,.........,.....,...,..........,.............,,...........,432 11.4. Примеры свойсш, выражаемых и РСП.................,.„.......................,...,.„........ 437 11.5. Заюпоченне ........................................................,...........................,... 440 11.6. Замечания......................„..............,........,..................................,.... 441 11.7.

Звлачн к главе 11 ............, ....................,............,.........442 ис 5 6 1 8 8 0 0 5 Св напк литературы . Иностранные издавна . Литература на русском языке Материаяы из Интернета... 535 544 545 Предматвый указатель Глава 12. Системы реального времеви. -....... 445 12.1. Модель систем реального времени. Временн6$ автомат и мо нонешние ........446 12.2. Сети време ннмх автоматов: параляельная композишм .................................... 453 12.3.

Операционная семантика модели временнего автомата— система переходов.. .М51 12.4. Нереалистичные поведения аременнего автомвш............................................. 462 12.5. Проблема шмлнэа системы переходов временного впомша........................... 465 12.6. Временные регионы: одни таймер....

. 46$ !2.7 Граф регионов временного автомата ....................................................................472 12.8. Временные регионы дяя нескольких лшшльных часов .......................................476 12.9. Анализ временных автоматов: логика СП.................,........................................,482 12. 10. Временны тем поральнаа логика ветвяшепкя времени (ГппЫ СП ).............. 4$9 Иитерпретвпсм формул ТСП,. ..

491 Формальны семантика ТСТ1... ..............,................494 12Л1. Анализ временных автоматов: сведение проверки ТСП формул к проверке СП:формул .. .. 496 12Л2. Сложность пягоритмов воде! сйесйшй лля логики ТОТИ.......,.........................506 12Л 3. )йэугэм проблемы вернфнкапии временных автоматов ..................................... 507 Допускаемый яэмк. 507 Биснмуляция... .. 50$ Достижим ость ... .. 510 12.! 4. Временные зоны... ..5!1 Временные регионы и временные зонм ..............,.......,..„.......,.................... 5П Оперении нал зонами . .. 515 Пересечение зоны с осраничениями на показания чжюа ............................ 515 Приращение времени....

.515 Достижимость эа одни шаг. ... 516 Структуры данных дяя предсшвления временных зон ................................... 521 Матрипа разностей гранил (Ргйегепее Вшшд МаЫх, РВМ) ..................-.. ЯЗ разностная решавшая лнмрамма (Рйуегепсе Оеснйап Рмрмп, РРР) .... 524 12 15. Инструменты всрифн юшин систем реального времени.................................... 525 Ррраа! . 525 СОшзоз ... ...

526 12. ! 6. Заключение .. ... 521 12.17. Замечания ... ... 529 12.18. Зааачн к главе 12.. ... 530 Анализ корректности программных систем — тема, которая не теряет своей актуальности. Поэтому неудивительно, чго тысячи исследователей и ишкенеров во всем мире пытаотся юабрести новые методы и рвзрвботвть новые инструменты проверки программ. Спепмвлнсты по теоретической информатике леже создали отдельную ветвь этой дисциплины, которая назыажтся формвльные методы разработки и анализа прогрямы". Однако, несмотря на массированные атаки нв проблему, до послелнего времени не удавалось добиться ревльньш результатов, которые можно было внедрять в широкую практику.

Моде! сйескгпй оказался одним кз первых формальных методов, который вышел из лабораторий н универсгпетов в мнр промышленной разработки программных и аппаратных систем. Это одновременно радует и удишшег специалистов в области верификации программ — ведь для того. чтобы тон° мй математический инструмент стал простым и понятным для обычных программистов, нужно было решить не только многие научные и технические проблемы, но и преодолеть привычный консерватизм, традиционную прзкгику не рисковать и не полагаться в серьезных проектвх на слишком новые и еще неопробоввнные технологии. Такое "преодашние" невозможно без энтузиазма люлей увлеченных и авторитетных. Лишь они могут сломать предубеждение по отношению к новым технологиям. Юрий Глебович Карпов — один из них.

Он сочетает в себе высокую компетенцию и юношескую увлеченность изяществом теории, о которой он пышет. В результате читатель получил, пшквлуй, первую книгу на русском языке, которая рвскрыввст потенциал нового поколения инструментов рвзрвботкн программ, построенных нв основе использования формпеьных методов. .й. И. Тбппилшвив дкоделтк РАН, дирттюр Иисппипута сиснммного программировтяия РАИ, зоведуюшид кофедроггп сгктемиого программирования ло фокультеим вмчисяительиодмотемояиош п кибериетики МГУ и в МФТИ, идРЬ плхЛ "И, Р цо Это необычная книга. Особенность ей придтот три обстоятельства: ГЗ Актуальность и прикладная значимость ее тематики: сейчас уже смело можно сказать, что метод люде! сйесМпй проверки правильности функционирования компьютерных систем и устройств и их программного обеспечения вышел за пределы лабораторий н активно стал попользовать.

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

как Е. М. С!мЗге, О. ОгстЬегй, О. Ре!ед. Моде! сйесИпй // М1Т Реева, 1999. Русский перевод: 3. М. Кларк, О. Гранберг, Л. Пелен. Верификация моделей программ: Моде! СйесЫпй// М., 2002. !З На сегодня зта книга, пожалуй, наиболее полное изложение метода пкх1е! сйес!г!пй и мнргочнсленных его приложений. Р. П. Смелянский Заведующий лабораторией вычислительиыл кампчехсов факультета Вд/иК МГУ, доктор физико-маимматическга иаух профессор, академик РАЕН Предисловие 21 июня 2008 года на торжественном банкете Ассоциации по мечишннпльной технике (АСМ) в Сан-Франциоко, Капифорния, трем ученым быяп вручена высшая награда Ассоцижши — премия Тьюринга 2007 г.