2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 89
Текст из файла (страница 89)
Например, зона 21 не изменится, если к ней добавить ограниченна хз >1, н/илн хз — х~ <5, илн хэ -х, < 3. Однако существует канонический вид таких матриц. однозначно определяющий зону. Канонической будет матрица при максимально узких границах. На рнс.12.27 видно, что дчя задания эрны 21 неравенства хэ -х, <3 и хз >1 действительно излишни: иа этом рисунке они представлены штриховыми линиями.
Добавление их, однако, делает задание таких зон однозначным. Нике приведен канонический внд матрицы, залающей зону 21: глава и яа 1, С Матрицы разносюй границ могут эффективно представлять множества соселннх временных регионов. Однако этой структурой данных оказалось невозможно эффективно описать множества регионов, которые не являются соседнимн.
Поскольку такие множества могут быть описаны логическими формулами, связывакицими все временные ограничения, их удобно представлюь с помощью бинарных решыощих диаграмм (ВОР). На этой основе разработаны эффективные алгоритмы символьной верификации систем реального времени. Разнсстная рвгйанэщая диаграмма (0Игегвпсв 0ес1аЬп 01аягаяэ, 000) Другой метод символьного представления множеств значений локальных часов во временном автомате основан на использовании так называемых роз- е 6 Рис.
1ИЭ. Рюиестнме режаюжяе дщгрэммы ляя пгмлствягмняя эеи я нк сбьелниений Ш1 ол лп пр эо Ц~ пг ле нг ал оп Сз вр ра ил ла Ц "п ко и! гг пс сгь ис пса ямн юд" юве ре- 12.16. Инструменты верификации систем реального времени Существует несколько программных еред для верификации систем реального времени. Кратко охарактеризуем две из них. Эти инструменты автоматизированной верификации временных автоматов свми выполняют построение параллельной композиции временных автоматов, построение графа регионов и/или графа зон, а также проверку выполнении свойств, вырюкенных формулами СТЬн ТСП 'для не очень больших систем.
0РРВВ! !)рраа( — зто программная среда для моделирования и варнфнкацнн методом "проверки молелей" систем реального времени, ршработанная объединенной командой двух университетов, Цррза)а 0п!!тешйу. Швеция, и Аа!йогй 1)пьегыгу, Дания, под руководством йг.'г'ь К!ш 1.вгшп и Р. Регегзшп. Система состоит из двух подсистем, графического интерфейса пользователя и подсистемы верификации. Графический редактор позволвет очень удобно оглюывкгь временные автоматы с целыми переменными (с ограниченным набором всенощных значений), попарно взанмолействуюшне мегодом ршщеву.
яостнмх реииаощих диаграмм (О!%кпсс 0есиоп 0вйгашв, 000в). Ревностная решвющш диагрпнма строится полностью аналогично Бинарным решающим диаграммам (В00), только роль двоичных переменных здесь играют неравенства вида х„-х сс, или х,-хгпсы. Пример разностной решающей диаграммы, задающей зону 21, представлен на рис.
12.23, п. 000, однако, позволяют предсгавить не только зоны, но и объединения зо, выравшемые произвольными логическими операциями над неравенствами. На.- пример, разисстная решыощая диаграмма, рнс. 12.2$, б, представлшт собой зону 22=(1ях, хЗ)л(2хха ч х! -хз <0). Цепью использования ревностных решающих диаграмм явлвется упрощение представления объединений временных зон н ускорение проверки прннадлшкности конкретного набора показаний часов такому обьедннению.
Разностные решшощне диаграммы обладают меньшей гибкостью, чем В00, дяя них вопросы упорядоченности, редукции, выполнения над ними логических операций решаются не так злегантгю, как для В00. Однако применение их в алгоритмах проверки некоторых свойств систем реального времени имеет определенные перспективы. глава гд Подсистема верификации строит граф регионов дия параллельной композиции временных автоматов. Система позволяет проварять, фактически, только свойства, выршкенные с помощью одноуровневых (не влоашнных) темпоральных формул логики СТТ.
вида Аор или Ерр, где р — это булеза комбинация атомарных прелнкатов и ограничений на значения локальных часов. Возможна темке проверка ограниченного во времени причинного следствия собьпий. Даже лри этом ограничении, однако, некио вырюить такие свойспш сне»ем, квк безопасность, ограниченная живость н достижнмость, например: О Ерр — достижимость (например, ЕР(х Ь у) — из начального состояния постижимо состояние, в котором пожжения часов х ие меньше, чем показания часов у); О АС»р — бежишсность (АС»(Лаз=»хд5)) — при функционировании автомата А всегда, если автомат попадает в локацию з, то показанна его часов х не меньше 5; О р-+ ! — лрнчинно.следственнаа связь угверашений р и 9, которая сокрашенно обозначает формулу АС(р ~ Арс) (это свойспю под именем ")еабьчо" было введено в ла б). Для проверки более слшкных свойств в среде ()рраа! трсбуегся строить контрольный автомат (оЬзегтег, илн ч»аюйбой).
Если свойство не выполняется, система выдает лиагностнческую траекторию. Система ()рраа! весьма удобна в исиользовании, она поставлястса свободно дла некоммерческих применений. Кгопое Инструмензэльный лаку» верификации сложнмх систем реального времени Кгопоз был разработан иссяедовательской группой Университета Гренобля и лаборатории УЕВ(МА0, Франция, в 2002 г. (первая версия — в !998 г.) В качестве модели испсльзуегся сеть взаимодейсгвукицнх временных автоматов, требования коррек»ности выраяшкпся формулами ТСТ(.. Для представления всех вычислений временного автомата Кгшхи использует граф зон. Для построенного графа зон Кгопов может выполнить проверку свойств, выраженных в полной версии логики ТСП., для чего применяются прямой и обратный алгоритмы проверки достюкнмосгн (Гшчнгб а»к( Ьасй»чш»( шасйаМ((гу) с использованием матриц разностей границ (ВВМ) для хранения зон.
Свойства, юпорые может проверять сисшма Кпюоз, могут быть доволь- коп жае Крс рап Сне риб '(2 В» чаа ми' усг по» слс Од си< ват ли ме1 ап! мо ер» че~ рп ме рк рн 12 но сложнымн. Например: "не более чем через 20 единиц времени е ыомапщ, когда приближающегося поезда нет, шлагбаум будет открыт", которое выра- жаезся в логике ТСТАВ так! вико по- юлюАО( «елг.=> ЕЦ пеагл орел)(! заптге)). ~ОВ. вия юй- на- Кроме того, еиотема позволяет проверять эквивалентвють двух систем, абст- рагированную от времени (бще-аЬзггасбпй п)п(та(енсе).
Систеиа Кгопоэ позиционируется как инструмент дяя продвинупях пользо- вателей, имеющих основательную подготовку в теоретических вопросах ве- рификации и поогроенна формальных моделей. ~ния 12.16. Заключение ! его я ео- енем конютея, збля и з98 г.) лыпет оаерггу пяютея сЬгаб внення яоволь- В настоящее время анализ свойств систем реального времени — это "горячая" область, в которой проводятея интенсивные исследования как в академических кругах„так и в индустрии. Поэтому многие термины здесь еще не устоялись, многие результаты являются только предаарнтельнымн.
Но даже зти предварительные результаты являются очень обнадежияжошими, они показывают большие аозможноети подхода воде! сйееЫпб для верификации еложных практических сиетем реального времени. Одним из главных вопросов в этой облаоти является следующий: можно ли системы реального времени описать формальной моделью, которая бы адекватно представляла поведение практических систем, разрабатываемых в различных областяху Существенным результатом здесь является модель временного автомата, которая была разработана сравнительно недавно ("Типам ащоюага аю юсеп! шобе(з...", [! 3)), Существует много других формализмов в этой области, однако именно временной автомат оказался одной из самых мощных н удобных моделей для представления поведения систем реального времени.
Этот формализм расширяет модель классического автомата введением локальных часов — вещественных переменных специального типа, значение которых возрастает синхронно со временем. Эти переменные игржот роль таймеров, с помощью каюрых можно измерять временные интервалы между событиями. С помощью такого механизма оказалось возможным выразить задержки между переходами системы, длзпельность выполнения операций и т. д. Модель временного автомата в настоящее время можно считать стандартной лпя представленна систем реального времени.
У временного автомата чнело состояний (в обычном понимании этого олова) — бесконечное число, каждый перекод в такам автомюе может быль представлен беоконечным числом переходов шгэбиением временной звдерагкн на проишольно большгю число ннтереапов. Поэтому система переколов, Глава 12 иредставлшощая вычисления временного автомата, не макет быль проанализирована без ее факторизации. Понятие временного региона как бесконечного ыножества наборов показаний локальных часов, эквивалентных с точки зрения проверяемых свойств, явяяется ключевым в анализе систем реального времени.
Это понятие позволяет свести бесконечное (континуум) число состояний временного автомата к конечному числу классов (символьных состояний). С помощью регионов удалось показать разрешимость многих проблем верификации временных автоматов: любые верифнкацисшные свойства поведения временного автомата имеют олин и тот же ответ дяя наборов значений локальных часов, находящихся в одном регионе. Недостатком графа регионов является астрономичешгое число регионов лэмсе для небольших временных автоматов: число регионов экспоненциально растет как от количества локальных часов, так и ог значений максимальных констант в ограииченивх на их значения. Поэтому непосредственное использование регионов для цракпгческой верификации невозможно.
Существует несколько подходов, позволяющих манипулировать множествами регионов, Одним из самых очевидных является использование бинарных решающих диаграмм (ВОЮ) для символьного представления множеств регионов. Такой подход был реализован, например, в системе СОБРАН.
Друпю решения в этом направлении используют понятие временной зоны. Для систем реального времени требуется анализ количественных характеристик поведения снсгем, чего не может дать обычная темпораяьная логика. Для выражения свойств систем реального времени было предложено несколько логик, одной нз них является довольно ясное расширение логики СП.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
