2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 13
Текст из файла (страница 13)
Поэтому более точно его смысл передает такая формула (.Тзс глена г С(Я лпм ю Я иадеюсь): "Сейчас и всегда е будущем, если я буду жие, ябуду иадеятъсг~". Подобно этому, ушервщение "Пока сердце бьевюц я б)ду боротьсяР формвлнзуегсв тшг: О(Сердце бьется ~ Я борюсь). б) Несколько другой смысл имеет упюржденне "даы будем бсротьсв. лака ие иобеднн". Его можно формализотпь таю Мы баремсяПМы победив».
Эта формализация прелшшагаст уверенность говоршцего в будущей победе. Если такой уверенности нет, то утверашение слелуег формвлмювать (Мы боремся%Мы иабедипи)»СгМы боремся . В этой формуле нашла отражение мысль: мы асе рвано будем Бороться, деже если н не победим (причем не исключено, что борьба продолжится и после победы). В темпоральной логике иногда используется оператор ЗЦ, так называемый "слабый ()пб!" (по-английски "() п(езе"), имеющий именно эту семантику: р%ц и р Ед»И р . С ншюльзованнем слабого (Гтй утверждение "Мы б)дем бороинсж лака ие лобед»м" более точно фориализустся так: айи боремся ЪЦМы победили. Эта формула утверждает, что мы боремся сейчас, будем бороться н дальше. пока не победим, н лаже если побешг не будет, мы вое равно будем бороться.
в) Англоязычные докумеигы часто снабжаются припиской: "Нщ та!»ед ший з!Бпед" — "не действителен до тех пор, пока ие подписан". Одна из , аазмшкных формализаций этой фразм: Документ не действитевеч ЦЦДокумеит нодаисаи. Эта формула, однако, ничего не говорит о том. что случится с момента подпнсашш документа.
По умолчанию зта фрша шщразумевает, чго с момента подписания документ сра:у же становится действигельным (вступа-. ет в силу). Поэтому более точно смысл ягой фразы передаст следующая формула: (- Документ действителен) ЦУ (Д и од ис лСДоку сит д йсттви и) юка зся, :я и %, пь,ем пз т~а- ля Здесь используется сгибый Отб, поскольку нет гврвмгнй. будет ли доку мент действительно подписан. Если гарантировано, что документ в буду щем будет подписан (например. паспорт обязательно подписывается владельцем при получении н сразу сшновится валидиым), то эту фразу можно формально представить оператором Онгб: ( Документ действителен ) И (Документ лодлисанлСдокумент денснмтнетн).
г) Если обозначить р утверлошние "Я теояр, то Ср означает "Я твоя наеекнР. д) Утвермдеине чМы лридем к победе коммуггестического трудар формально запишется так: Р Коммунистический труд наба)гм! е) Строфе из песни В. Бехнова "Сегодня он иаэснт длгаз, а завтра Родину ирод аст", если ее понимать буквально, соответствует формула: Он «греет джазюХОн продает Родину. Но, и~видимому, поэт имел в аиду более общий смысл: С(Он играет джазмгХОн лродает Родину)— "если когда ниб)дь нарень начнет играть длсаз, то на сгедующьтг день он . найдет продавать Родину". Однако, возможно, поэт хотел этой фраюй передать еще более общую мысль: "если когда-нибудь парень нашит играть джаз, то нотам, рано иеи ноэдно, он облзатеяыю прсдпст Родину".
В этом случае он мог бы сказать точно и недвусмысленно (хотя и не совсем в рифму): С(Он играет джазсэХРОн продает Родину) . т) Пусть р озпачеет "Ялюблю Машу", а а — "ЯлюбпоДан(у". Тогда: Рр — чЯ когда-нибудь обязателыю нападаю ййииу"; Са — "Н люблю Дтиу и буду яюбивш ее всегда"; С(-р ч -ч)) — "Я однааоб, и никогда не буду любить и ййииу, иДгпиу одновременно"; а()р — "Н будущем я номобгю Маггу, а до той норы я буду любтнь Дт у"; РСР— "Когда-нибудь я наяюбею Машу наветю",' Суд — "Я буду бестшечгю виобпгтьаг еДаигу" ..
Гювев г з) Рекламный слоган "Раз Персил — всегда Пгрсгм" не совсем ясен простому человеку. Что значит — "Раг Персил ~ По-видимому, рекламодатели хотели сказать, что если некто когда-нибудь иопробуст Перепл, то с этого момент он уяю не сможет от Персила отказаться и будет им пользоваться всегда. Но тогла абсолютно точно смысл этого глогана выражает слелуюшал формула логики (,Т(л с(пр спр ). Подобиымн точными формулами н гкщо реклвмиромпь пшвры. Итак, темпоральные формулы могут конечным образом характеризовать свойства бесконечных процессов.
имеющих поведение по времени, резво)хь чнвающихся во времени в последовательности миров, или ситуаций, есяи снабдить миры (кажлую статическую сизуацию в дискретной последовательности таких ситуаций) конечным набором атомарных утверждений, принимшошнх одно из двух значений — истина нли ложь — в каждом нз миров. Атомарные угверхшения сами не включыот время, в юждом мире их истинностное значение статично, неизменно. Но в другом мире этн значения могут быть другнмн. 2.4. Реагирующие системы (геаст))уе еуе1егпе) в ение Я.В ( аи ив системы, твегйт в Реагирующие системы — это класс информационных систем, основной функцией которых является подаерхшнне взаимолействия с окружением, а не п)мобрвзованне информации.
Для этого класса систем — пршрамм, аппаратуры и т. п., которые в англоязычной литературе назывшотся геасбше тзюпм, мы будем использовать термин реагир)яшвие, потому что буквальный перевод слова геаслге — термин реаюниеиые — имеет прочную устоявшуюся семантику: он характеризует устройство, именхцее в хвосте сопла с вырывающимися клубами огня, Реагирующие системы отличны от обычных программ преобразования данных (их часто называют ивишсформавыонимми лрсграммани). Трансформационные программы принимают на вход исходные данные, производят вычисления и вмдают результат на выход, после чего работу завершают. Программы обращения матрицы, поиска экстремума функции, решения дифференциального уравнения численным мегодом — все зто трансформационные программы. Фактически прощании преобразования данных являются функциямн, осуществляющими отобршкение входных данных в выходные, и верификация такой програмы состоит в проверке правильвкти преоб- 1удь гкл ысл вать оракли ель- сииров.
гин- огут ршзоввиия возможных начальных шктошшй программы в закшочвтельиые ее состояния. Реагирующие системы, напротив, функционируют бесконечно, они кошро. пируют окружение, реагируя на внешние события — получение сообщения, щелчок кнопкой мыши, нахштие клавиши <Епыть и т. п. Останов таких систем обычно связан с поломкой илн коллизией (блокировкой) и валяется ошибкой. Как правило, реагирующие системы являются частлми ббльшнх систем, с которыми онн взаимодействуют. Операционные системы, протоколы коммуникации, планировщики, контроллеры, параллельные взаимодейст.- вующие программы, системы логического управления, драйверы — все зто примеры реагирующих систем. Верификация реагирующей системы ме может быть сведена к проверке отношения между входом и выходом после прихода системы в заключительное состояние: такие системы ииеют начальное состоямие, но не имеют заключительного состоаиия, они вообще не должны останавливаться.
Для задания требуемых свойств поведения реагирующих сисек наиболее удобным средством оказались формулы темпоральной логики. Сведем в таблицу сравнительные харакшристики трансформационных и реа.- гирующих систем (табл. 2,1). Таблниа 2Л. Сравнительные характеристики тршкформаннониьш н реагирующих еисми Примеры зной еии- ~гло|нать тер- гизу- Вычисшиня Поведение Семантика Функпия; Спспнфиквшм (шебошгшя к снекма), даи- рма- вы- Проения фый шля- шод- шоб- Транеформаигюиные нреграммиьм сисшмы Обработка данных, численные методы, вычисшнис функпн», распознавание обрезов и т.
д. Получение выходного значения зш фуикнин исхолиых значений Всегла юнечны с получением результата по нх завершении зыков программы ншеешя функвней ст ехали ых занима Обычно в анас логических пред- н шктушшвий, например (х д о) з(гу 6) г сслн до запуска программы 5 персмснивз х нс меньше О, то шкас завершения 5 гкрсменнаа у. булез юмть значение (х р из из рую янга «рограммиыз системы Прошхоша лрайвсры, системы логического упршлсиия, ОС н т.л. Обеспечение взвимодсяствма с окрумеиием по определенным правилам Всегла бсешгнсчны; шмогда нс завершаютсв ш~слгдоватслыккм сосгоаннй н реншнй системы на внешние события Обычно, в виде формуя тсмпо- Пшьиой логики, например: С(р ю Хре): для всех мктояиий пршрвммы сиравсдл н ю следую.
шсег сслн выпоаннай(Ь ушернле иие р, то пмом. в кмшм-то сш- луяннсм се мктоянин, ебязатевыю выповнитса Е Главе 2 Введенные выше последовательности миров ьюжно считать моделями функционирования технических реагирующих систем. Кюкаый мир может представлять состояние реагирующей системы, а переходы — изменения сосюяний, дискретные переходы снстмаы. Как внешнее воздействие, так н реакцию системы можно включить в ее состояние. Теперь макни формально определить вычисление реагирующей системы и ее поведение: + Опрвбвпании 2.$ (вычисление и поведение реаеир ей системы) Вычисление реагирующей системы — это бесконечная последователь- ность состояний, которые система проходит ао времени.
Поведение реагирующей системы — зто все возможные ее вычисления. Будем обозиачюь вычисления греческими буквами к, а и т.п., например: и ззг,гзгз.... Из одного состояния в другое система переходит в некоторые дискрвгиые ыомеигы времени ге, гп гз, ..., выполняя операшги. Начелыию состояние вычисления часто помечмпся стреякой (рнс. 2.7). Рвс 2.7. Бесконечная пеночка миров как вычисление дискретной системы о я Т ф Рне.3.8. Атонвриме преднкаты — базисиме свойсев системы. В заидма аоиояннн вычислеияя нстнним некоторые юъмарньм предикаты нз заданного конечного нх множестве В каждом состоянии маквт быть задан набор истинных в этом состоянии атомарнмх предикатов — тех баювых свойств, которые интересуют нас при аналию системы (рис. 2.8). Если атомарный преликат не выполняется в состоянии, то его в этом состоянии не будем указывать (т.
е. состояния помечаются теми атомарными преликатвми, которые в этом состоянии истинны), По значениям этих элементарных, неделимых утверждений можно строить как булавы формулы, харакшрмзуюпше конкретное состозние, так и темпорвльные формулы, хармперизуюшне целое вычисление, начннжощееся в этом состоянии. Имея в каждом сасгоянии вычисления известные иатинщктные значения атомарнмх предихатов, мы можем в кюкаом состоянии дискрепюй системы подсчитать истинность нли ложность любых логических и (в принципе) любых темпорвльных формул.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
