2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 80
Текст из файла (страница 80)
называютсв "диве/геелшными". Формально, вычисление о будет дивергентным, если йшб< (о,/)=ю. При анализе временных автоматов конавргентныс вычисления не рассматриваются, хотя а модели формально их построить можно. Анализ временных автоматов ограничивается только дивергентными вычислениями. Вычисления Зенон<к Прнмерамн другого типа коивергентных вычислений, которые формально могут существовать ао временном автомате, хотя они н противоречат интуиции, являются так называемые "еычвсзеввя Зенона". Такие вычисления представляют выполнение бесконечного числа переходов по действиям между локацнвмн автомата за конечное время. Например, у автомата 4< (рис. 12 8, а) может быть такое вычисление: (т;х=б)-1»(м< я=1)-о-»(<гх О)-1/7-»/Ш я=1/2)-Ь-+ (ш:х О)-1/4-+(яг,.т=1/4)-о-+(<Х я=О)-1/8-+(л;х 1/Я)-Ь-» (м;х=й)-1/16-+(<л;х !Лб)-а-+(<Хх=б)-1/32-+(пх=1/32)-Ь вЂ” » .
Это конвергепгное вычисление, здесь на бесконечном вычислении время тоже растет ограниченно (рис. 12.8, б/, но природа некорректности лругая. Подобные вычисления являются моделью хорошо известного парадокса Зенона: еытмленне бесконечного ксличесмеа дейсшеий е огралнчеллан внтереаш ерезмлн. В этом и шютоит нереалистичность таких вычислемий, хотя они возможны в соответствии со спецификацией временного автомата А< . В модели временного автомата мы предполагаем, чзо переходы, выполняемые вследствие наступления событий (действий), мгновенны. Если последовательность таких мпювенных действий образует цикл, то это и приводит к вычислениям Зенона. Хотя временной задервиой кшкдого из действий в цикле мы можем пренебречь, бесконечное число таких действий не мшкет быль рлаев гя цнн .
стоя> зс б запрс мени (л (л автоь быль терю 12.) Врб Одно ВЕРИГ ни мгновенным, ни Вьзполнзпься В огреннчсиный изпчрВВВ Вреыенн, посмимку скорость процессоров не явяяегся бесконечной. Налнчие выч«олений Зенона свндетсльствует о некорректности модели. Р)зс 1У.И а) Временной 'автомат Ач, 6) изменение во времени показаний сю локальных часов на вычнгленнн Зенона Звлержку. соответствующую реальному действию в снсюме, моделью которой Валяется мгновенный переход во временном автомате, можно учесть разнымп способами. Например, модель, у которой существует цикл с мгновенным действием а, можно легко намелить, введя дополнительно: ГЗ новую локацию "вылсялмпм дейсменя а ",' ГЗ новые локальные чаоы х„, учнтывающне длнгельность действия а П ннвврпанг(х, ь щах) влокацнн "еьилыненнедейслмие а": О мгновенные события лачаю, н окончание, выполнения действия и; П сброс часов х, на переходах, помеченных собьггнем начало,; 0 ограничение (О < пип пхе), которое установлено на переходе с мгновен, ным действнем околчалне нз локации "вьнмянслгм дейслмгм а ".
Возм дери Блок фнка инва! "длоз В зтс но ос терна цни. моин мата но гл ннва! ВВРЩ чнт т мы, ~ в нач сн- Возможны и другие вврианпя учета в модели задеряпш при выполнении лействня в реальной системе. Два различных варианта введения подобной задержки показаны на рнс. 12тк Блокировка времени в состоянии.
Примером этой некорректности спецификации временного автомата явлвется возможность попадания автомата в состояние, в котором текущие значения локальных часов не удовмтворяют инварианту соответствующей локации. Твкэя некоррекпккзь называется "бяокирсекой еремелй (11ше!оск). Если в автомате .4 1см. рнс, 12.1) в локации зс определить инвариант х < 1. то переход пг состояниа (зз1л = 1) в состояние (зс;к = 1) при действии Ь запрещен: такого состояния с локациай зс быть не может. Но оставаться в локации зз автомат также не может: это запрещено инвариантом локации зз. Отсутствие прогресса.
Еше одним примером некорректного поведения временного автомата является следующее вычисление автомата Ае на рнс. 12.8: (т;л=б)-02-+(т; я=02) — !.8-ь(лг, т=2)-104 ь (лг,я 12.4)-6.5-ь(т;к=18.9)... В этом вычислении время растет, но автомат не прогрессирует: он бесконечно остаетса в одной н той же локации, имея при этом в любой момент альтернативу — либо выполнить действие а, либо задержаться в текущей локации. Синтаксически определизь, по автомат должен выполнить переход, можно с помощью ннваривнтв, который ограничит время нахождения авто. мата в локации.
В локации м автомвта Ае этот инвариант равен ггке, именно поэтому здесь автомат может оставаться бесконечно долго. Отсутствие ннварижгш в локации не всегда является ошибкой. Например, отсутствие инваривнта в локации зс временного автомата А~ (см. рис, 12.1) ие противоречит требовайням к нему: этот автомат является моделью реагирующей сисшмы, он реагирует на внешние собьпия и может ожилать накатил кнопки в начальной локации зс сколь угодно долго.
Однако в локацнах з~ и зз этого автомата наличие инваришпов обязательно: внешнее окружение дшпюю быть проинформировано о типе щелчка кнопки мыши в огрпвиченнмй ин-. тервал времени. 12.6. Проблема анализа системы переходов временного автомата Одной ш главных проблем, препятствующих анелюу свойств поведения н верификации сисшм реального времени, является бесконечность числа со- Глава ГЯ сгояний системм переходов Т.
Поскольку соспмнием графа переходов временйбго автомата является пара (яокаягмг иокаюиия есгх локагьяых часов), у семантической модели аременндго автомата всегда будет не просто бесконечное число состояний, число его состояний имеет мощность континуум. Например, временной автомат лз с единственной локацией, единственнымн часамн и только одним переходом имеет систему переходов Т(Аз) с бесконечным множеспюм возмшкиых состояний и переходов (см. рис. 12.7). Возмшкна ли в принципе автоматическая верификация (например, анализ лостнжимости, алгоритмы проверки модели и т. п.) таких систем? Алгоритмы верификации разрабошны для систем перехолов с конечным числом шхтояиий, оии не мшуг быть механически перенесены на системы с бесконечным числом состояний. Один из методов упрощения системы переходов — объединить-состояния системы в группы (классы) эквивалентных состояний и рассмотреть вместо всего множеспш состояний пшько группы таких состояний, которые в некотором смысле подобны (рис. 12.9).
Группировать в классы эквивалентности можно по-разному. В нашем случае отношение эквивалентности на множестве состояний должно быть выбрано так, чтобы с точки зрения проверяемых свойств исходная система и редуцированная система меньшего размера были бы взаимозаменяемыми. неразличимымн. Пусть дана система переходов Т = (Я, ае, Е, и) н иекоторое отношение эквивалентности к, объединяющее в один кавос состояния системы Т, которые согласуются с переходамн Т (рнс. 12.9): г ч» 9 и Ггг(з, и, э ) в к) (3(ф О, 9 ) а Я): 3 ' ьт 9', т.
е. любые переходы из ссстоаний, эквиваланпгьш отноонтельно эквивалентности к, осушесшлшотся только в состояниа, которые также эквивалентны по эквивалентности и . Обозначим Т„новую систему переходов, которая называется троюиорсксвмлгой лерехадое Т ло модулю олаюшяиия эяегмпшиягяссяги и" н стро- Ь классы эквнвалепшости я являются состояниями Т„; Ь класс эквивалентности к, включмоший зе, являетоя начальным состоянием Т,; Ь аяфшит действий Т, совпадаег с алфавитом действий Т; Ь мншкество переходов Т„определяется для пар классов эквивалентности к. Часп рой а сном ма 12, Оосямиы (л,) буй иаи- орые мии- 1еит- ~охов х чаГи му таси- влиз итмы СТОЯ яным ~яиия ИСТО ТЕКО- кест.- ямых были Рис.
Яйся Спсмма иярмюлов Т и сисюмв пермюаоа Тя по модулю опюшения зяаммяеютюсти к Частным случаем такой эквивалентами является эквивалентность, а которой кямдое сооммиие системы переходов зкяиаалеитио только себе. бзипор. сисзема переходов по молулю такой экаиаалеипиюти совпадает с исходной Глаев 12 системой переходов. !!вс интересуют зквнввлентности, объединяющие в одни класс множества соогояний. Если даже число состояний системы переходов Т бесконечно, ио индекс (число кпассов) эквивалентности х будет конечным, то задача анализа бесконечной системы переходов после такой редукции может свестись к задаче аналнщ конечной системы переходов Т„.
Можно ли определить такое отношение эквивалеигности я на множестве состояний системы переходов Т(А) временндго автомата А, чтобы редуцированная сисгема переходов Т„(А), состояниями которой являютсв классы эквиавленпюсти х, могла бы заменить Т(А) при анализе, по крайней мере, некоторых интересных свойств? Такое отношение эквивалентности существует, оно определяегся на основе понятия временных регионов.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
