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

Э. Кларку, А. Эмерсону и Дж. Сифакнсу вручена премия Тьюринга Ассоциации АСМ за 2007 г. за их вклад в до. ведении метода тоде! сйесрбпй до производственной технологии, позволяющей ооуществлять верификацию моделей реальных программных и аппаратных систем. Во многих рабатах приводятся результаты использования этой технологии для верификации программно-аппаратных систем дяя критических применений (см., например, [69], [124] и лр.).

Теории и технике верификации, обьеднненной названием пюре( сйесалй, посвящена огромная лизературц от монографий и вводных обзоров до многочисленных университетских курсов, представленных презентацнямн в Интернете. Довольно полное нзлсмение материала этой области содермитсв в монографиях [34] н [19]. Укамем заесь также некоторью доступные вводные тексты: [106], [149], [117].

Иа русском взыке, кроме перевода основополагающей монографии [34], нет книг н почти нет статей, дающих общее введение в предмет. Исключением валяются слайды лекций Б. Конева, проч!ивиных им в ПОМИ АН РФ [!93], и лекции Ю. Лифшица [194]. В сборнике [168] несколько статей посвацено вопросам верификации программ в рамках разрабатываемого под руководством проф. А. А.

Шллыто "Автоматною подхода" к программированию, т. е. к программированию с явным выделением соспиннй. 1.9. Задачи к главе 1 1,1. Рассмотрнге параялельную программу с двумя процессами, юморые выпояняютса асинхронно: Р)з а,:Аю(: ((:лю2 г ээ! го1иэв ые пм ~3~ ,но го~ю. ого упгом му, гни эв ци. но- Ы. ~ые ра- жэгой че- Значение А вначале равно О. Рассмотрите все возмакные варианты значе- ний, которые могут иметь переменные В и С по завершении программы. 12.

Протестируйте программу разделения мноннсти для различных наборов значений в множествах 8 и Ь. Доюжите, что эта программа всегда работает правильно в случае одноэлементных множеств Я и/нлн Х . 1З. Протестируйте с помощью ручной прокрутки протокол %.СЛ.упсй при различных ситуациях в каналах передачи данных. глдвл 2 Темпоральные логики Для вернфнквцнн техннчвскнх систем свойства нх поведення должны быль выражены формально логнческнмн утвержденнямн, которые обеспечат простую, лаконнчную н недвусмысленную нх запись.

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

Достаточно мощные, выразнтельные н в то же время простые темпоральные логики былн пестровым как простые расшнрення обычной логики высказываннй. В этой главе вводятся две темпоральные логнкн: 1.'П. — темпоральная логика лннейюго временн, н СП. — темпоральная логика ветвящегося временн. Эгн логнкн очень просты, что отлнчает действнтельно полезные математические модели. Формулы этих логнк являются удобным языком для вырюкення свойств параллельных программных сноюм н, квк частный случай, встроенных систем. 2.1. Утверждении, истинность которых зависит от времени Прн всей шпроте нспользовання классической логнкн в науке, техннке н в обычной жнзнн очевидны ее ограннчення.

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

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

Если утверждения естественного языка явно илн неявно включают зависимость высказываний от времени или от порядка собмтий ао времени, то формализация нх в классической логике высказываний обычно неадекватна. Например, коммуштивность операции конъюнкции (перестайовочноеть ее аргументов А л В и В л А ) не выполняетса для следуюших высказываний: Дигону сяныо стртино, и он убие не эквивалентно предложению Джон убие, и ему снима странию. Джон умер, и его нсхарониеи не эквивалентно предложению Джона наборонили, и он умер. Джейн еыита заиузс и Роднеа Ребенка не эквявалентно предяшкению Дзьчьн родняа ребенка и еьнила запуск.

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

Высказывание "Светит сояняп", жякное сегодня, может стюь истинным завтра Утверждение "Я иыодеи" станет лшкным после того, как я поем. Многие утвержаения, в которых ввалятся причинно.следственные отношение, также отмены со временем: Если я видел ееуаныие, то я узнаю ее нри встрече. Раз Пероне — всегда Персид Мы не друзьц тжа ты не имииннмсд си- номь ~ымг ий и- р- а- и Утверждеиие естественного язмви: Вчера он сказал, что придет заенйнь значит он сказал что првдтп сггодни несомненно, истинно. Но в обычной логике вьюкюываиий формально дека- зать его истинность невозможно.

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

С2: Лифт нгтогда не проидгт мимо эталон, вызов от которого иостуты, но ещг не обслулсгн. Элементарные (атомариые) утверждения в этих высщпываииях могут быть истинны в один момент времени и дввиы в другой. Поэтому мы ие макам адекватно предсщвить утверждение С ! е помощью формулы логики выщаь зываиий: Послана иг Оцгнгботанл (есяи запрос Я послан. то ои обработан). Действительио, в классической лапше угверждеиил обычно поиимаются как истинные либо лшкиые независимо от времени, а утверждение С! явно различает разные моменты времени.

Оио утверждает, что если е некоторый момент времени г запрос Я послан, то в какой-то будуирпг момент времени гно г ои будет обработав. Попытаемся выразить зги свойства с помощью логики предикатов ! порядзи, вводя в употреблеиие такие выражеиия, как "событве р наппутто е момент г ". Утверлщеиие С! при зп>м будет выглядеть так: (Уг и ОЯПослан Я ю (Зг'> г)Обработанл (г') УтВЕРЯЩЕИИЕ С2 Е ЛОГИКЕ ПРЕДИКатаз ВЫГЛЯЛИт таК (ЗЛССЬ Лмфвгн(г)— угверждеиие: "Лифт е момент г нролодит мимо этажа р "): (Уг пб)(тг'дг$Вмзое„ил(ми:гхп 5 ! ) Обслужилгмтсл„(г!) ю (Зг2:гйг2йг')Лифт„(г2)) Талия формализация трудно чкгаеюя, и, как известно, доказазекьспщ в логике предикатов проводить довольно слшкио.

Этот путь формвлипшии завиоимых от времеви утверждений пока ие двл суииствеииых результатов для практики верификации технических систем.. Глевв 2 и и<в е,и 8 вмстмееиитя печь ивет се ятем и месив уменя йепнв (Осмммм) ОЕВЧЕО «Овеете времеви с '1 Ьвм еееа 4аМ' еси в и етст мемент я тммея Фане печь ивет Ов етсн (метнем) вснп пе О1тененв б Рне, 2.1.

Времмм глаголов англнйааио язьвм Ршг 1абеба)м и Рмзмп Ре'Геа мсдеаируююя соотношениями момешов настушимня ссбьпвй Помыгка построения формальной модели, наввно учитывающей время в высказываниях, была предпринята философом и логиком Гансом Райхенбахом (Наш Ке)ОЬепЬас(т) для изучения глагольных времен английского юыка. В теории Райхенбахв время глагола в предложении характеризуется соотношением моментов наступления событий, о которых говорится н которые подрезумеваются в предложении.

Используя соотношения во времени двух моментов: момента Я, в который сделано высказывание (арсе<)т г!ше), и момента Е наступления события, о котором говорится в высказывании (Етеш бте), можно сбрпкжать только три простых времени глагола — настоящее, прошедшее и будущее с соотношениями соответственно Е=Я, Е<Я и Е>Е. Для того чтобы покрьпь ббльшее число различных глагольных времен, Райхенбах ввел третий момент — момент й точки референции (Яефтелсе Вше), т. е.

момент, на который ссылается высказывание. В Рпюге РегГест, когда мы говорим, например, '7 н !!! !юге геен го)ж" (буквально "Н б)я)у имелм Длсояа увиденным"), зто высказывание отсылает нас не к тому моменту, когда в увидел Джона, но к моменту, по отношению к которому (м)бт ю(егепсе 1о) мое видение Джона уже произошло, т. е, соотношение между этими момейтами времениесть Я<Е<)1. , выоюм ыка. пои~те), про- >Я, Рай'же), с мы сола уви- кми Формальная модель Райхенбвха позволяет прояснить различия многих времен глаголов английского языка. Например, в предложении н! зал Уо)ш" соотношение между этими моментамм Я = Е < 3; а в предложении "! баге зеел уо)ш" это соотношение Е < Я = Б (рис.