SP-DEVS - Википедия - SP-DEVS

SP-DEVS Сокращение «Спецификация системы дискретных событий с сохранением расписания» - это формализм для моделирования и анализа систем дискретных событий как с помощью моделирования, так и с помощью методов проверки. SP-DEVS также предоставляет функции модульного и иерархического моделирования, унаследованные от Classic. DEVS.

История

SP-DEVS был разработан для поддержки верификационного анализа своих сетей, гарантируя получение конечного графа достижимости исходных сетей, что было открытой проблемой формализма DEVS примерно 30 лет. Чтобы получить такой граф достижимости своих сетей, на SP-DEVS были наложены три ограничения:

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

Таким образом, SP-DEVS является подклассом обоих DEVS и FD-DEVS. Эти три ограничения приводят к тому, что класс SP-DEVS закрывается при связывании, даже если число состояний конечно. Это свойство обеспечивает проверку некоторых качественных и количественных свойств на основе графа с конечными вершинами даже с моделями, связанными с SP-DEVS.

Пример контроллера пешеходного перехода

Системные Требования Рис. 1. Система пешеходного перехода Рис. 2. Модель SP-DEVS для контроллера освещения пешеходного перехода.

Рассмотрим систему пешеходного перехода. Так как красный свет (или световой сигнал запрета на прогулку) ведет себя противоположно зеленому свету (соответственно свету пешехода), для простоты мы рассматриваем только два огня: зеленый свет (G) и светильник для пешеходов (W ); и одну кнопку, как показано на рис. 1. Мы хотим управлять двумя индикаторами G и W с набором временных ограничений.

Для инициализации двух индикаторов требуется 0,5 секунды, чтобы включить G, а через 0,5 секунды W погаснет. Затем каждые 30 секунд существует вероятность того, что G погаснет, а W включится, если кто-то нажал кнопку. По соображениям безопасности W загорается через две секунды после выхода G. 26 секунд спустя W выходит, а через две секунды снова включается G. Такое поведение повторяется.

Дизайн контроллера

Чтобы создать контроллер, отвечающий вышеуказанным требованиям, мы можем рассмотреть одно входное событие «кнопка» (сокращенно? P) и четыре выходных события «зеленый свет» (! G: 1), «зеленый выключен» (! G: 0), «прогулка» (! W: 1) и «прогулка» (! W: 0), которые будут использоваться как сигналы команд для зеленого и пешеходного света. В качестве набора состояний контроллера мы рассматриваем «зеленый при загрузке» (BG), «переход при загрузке» (BW), «включение зеленого» (G), «зеленый-красный» (GR), красный цвет (R), прогулка (W), задержка (D). Давайте спроектируем переходы между состояниями, как показано на рис. 2. Первоначально контроллер запускается с BG, срок службы которого составляет 0,5 секунды. По истечении срока службы он переходит в состояние BW, в этот момент он также генерирует событие «зеленый свет». Через 0,5 секунды пребывания в BW он переходит в состояние G, время жизни которого составляет 30 секунд. Контроллер может оставаться в G, перебирая G в G без генерации какого-либо выходного события, или может перейти в состояние GR, когда он получает внешнее входное событие? P. Но фактическое время пребывания в GR - оставшееся время для цикла в G. Из GR он переходит в состояние R с генерацией выходного события! g: 0 и его состояние R последние две секунды, затем он переходит в состояние W с выходным событием! w: 1. 26 секунд спустя он переходит в состояние D с генерацией! W: 0 и после 2 секунд пребывания в D возвращается к G с выходным событием! G: 1.

Атомарный SP-DEVS

Формальное определение

Вышеупомянутый контроллер для пешеходных огней может быть смоделирован атомарной моделью SP-DEVS. Формально атомарный SP-DEVS представляет собой 7-кортеж

{ Displaystyle M = }

куда

${ displaystyle X}$ является конечный набор входных событий;
${ displaystyle Y}$ является конечный набор выходных событий;
${ displaystyle S}$ является конечный набор состояний;
${ displaystyle s_ {0} in S}$ является начальное состояние;
${ Displaystyle тау: S rightarrow mathbb {Q} _ {[0, infty]}}$ является расширенная функция времени который определяет продолжительность жизни состояния, в котором ${ Displaystyle mathbb {Q} _ {[0, infty]}}$ - это множество неотрицательных рациональных чисел плюс бесконечность.
${ displaystyle delta _ {x}: S times X rightarrow S}$ является функция внешнего перехода который определяет, как событие ввода изменяет состояние системы.
${ displaystyle delta _ {y}: S rightarrow Y ^ { phi} times S}$ является функция вывода и внутреннего перехода куда ${ Displaystyle Y ^ { phi} = Y чашка { phi }}$ и ${ displaystyle phi notin Y}$ обозначает тихое событие. Функция вывода и внутреннего перехода определяет, как состояние генерирует событие вывода, и в то же время как состояние изменяется внутри.^[1]

Официальное представление контролера пешеходного перехода

Указанный выше контроллер, изображенный на рис.2, можно записать как ${ displaystyle M = }$ куда ${ displaystyle X}$ = {? p}; ${ displaystyle Y}$ = {! g: 0,! g: 1,! w: 0,! w: 1}; ${ displaystyle S}$ = {BG, BW, G, GR, R, W, D}; ${ displaystyle s_ {0}}$ = BG, ${ Displaystyle тау}$ (BG) = 0,5, ${ Displaystyle тау}$ (BW) = 0,5, ${ Displaystyle тау}$ (G) = 30, ${ Displaystyle тау}$ (GR) = 30, ${ Displaystyle тау}$ (R) = 2, ${ Displaystyle тау}$ (Вт) = 26, ${ Displaystyle тау}$ (D) = 2; ${ displaystyle delta _ {x}}$ (G,? P) = GR, ${ displaystyle delta _ {x}}$ (s,? p) = s, если s ${ displaystyle neq}$ ГРАММ; ${ displaystyle delta _ {y}}$ (BG) = (! G: 1, BW), ${ displaystyle delta _ {y}}$ (BW) = (! W: 0, G), ${ displaystyle delta _ {y}}$ (G) = ( ${ displaystyle phi}$ , ГРАММ), ${ displaystyle delta _ {y}}$ (GR) = (! G: 0, R), ${ displaystyle delta _ {y}}$ (R) = (! W: 1, W), ${ displaystyle delta _ {y}}$ (W) = (! W: 0, D), ${ displaystyle delta _ {y}}$ (D) = (! G: 1, G);

Поведение модели SP-DEVS

Рис. 3. Сегмент события и его траектория состояния модели SP-DEVS.

Чтобы запечатлеть динамику атомарного SP-DEVS, нам нужно ввести две переменные, связанные со временем. Один из них срок жизни, другой пройденное время с момента последней перезагрузки. Позволять ${ displaystyle t_ {s} in mathbb {Q} _ {[0, infty]}}$ быть продолжительностью жизни, которая не увеличивается непрерывно, а устанавливается, когда происходит дискретное событие. Позволять ${ Displaystyle т_ {е} в [0, infty]}$ обозначают истекшее время, которое непрерывно увеличивается со временем, если нет сброса.

Рис 3. показывает траекторию состояния, связанную с сегментом события модели SP-DEVS, показанной на рис. 2. Вверху на рис. показывает траекторию события, в которой горизонтальная ось является осью времени, поэтому она показывает, что событие происходит в определенное время, например,! g: 1 происходит в 0,5 и! w: 0 в 1,0 единицу времени и так далее. Внизу рисунка 3 показана траектория состояния, связанная с указанным выше сегментом события, в котором состояние ${ displaystyle s in S}$ связан с его продолжительностью жизни и прошедшим временем в виде ${ displaystyle (s, t_ {s}, t_ {e})}$ . Например, (G, 30, 11) означает, что состояние - G, его продолжительность жизни и прошедшее время - 11 единиц времени. Сегменты линии в нижней части рис. 3 показывают временной поток прошедшего времени, который является единственной непрерывной переменной в SP-DEVS.

Одной интересной особенностью SF-DEVS может быть сохранение расписания - ограничение (3) SP-DEVS, которое нарисовано в момент времени 47 на рис. 3., когда происходит внешнее событие? P. В этот момент, даже если состояние может измениться с G на GR, прошедшее время не изменится, поэтому сегмент линии не будет разорван в момент 47 и ${ displaystyle t_ {e}}$ может вырасти до ${ displaystyle t_ {e}}$ который в этом примере равен 30. Благодаря такому сохранению расписания от входных событий, а также ограничению временного перехода неотрицательным рациональным числом (см. Ограничение (2) выше), высота каждой пилы может быть неотрицательным рациональным числом или бесконечностью. (как показано в нижней части рис. 3.) в модели SP-DEVS.

SP-DEVS - это подкласс DEVS

Модель SP-DEVS, ${ Displaystyle M = }$ является DEVS ${ displaystyle { mathcal {M}} = }$ куда

${ displaystyle X, Y}$ из ${ Displaystyle { mathcal {M}}}$ такие же, как у ${ displaystyle M}$ .
${ Displaystyle S '= {(s, t_ {s}): s in S, t_ {s} in mathbb {T} ^ { infty} }}$
${ Displaystyle s_ {0} '= (s_ {0}, tau (s_ {0}))}$
Учитывая состояние ${ displaystyle (s, t_ {s}) in S '}$ , ${ displaystyle ta (s, t_ {s}) = t_ {s}.}$
Учитывая состояние ${ displaystyle (s, t_ {s}) in S '}$ и событие ввода ${ displaystyle x in X, delta _ {ext} (s, t_ {s}, t_ {e}, x) = (s ', t_ {s} -t_ {e}) { text {if} } delta _ {x} (s, x) = s '.}$
Учитывая состояние ${ displaystyle (s, t_ {s}) in S '}$ , ${ displaystyle delta _ {int} (s, t_ {s}) = (s ', tau (s')}$ если ${ displaystyle delta _ {y} (s) = (y, s ').}$
Учитывая состояние ${ displaystyle (s, t_ {s}) in S '}$ , ${ displaystyle lambda (s, t_ {s}) = y}$ если ${ displaystyle delta _ {y} (s) = (y, s ').}$

Преимущества

Применимость абстракции временной шкалы

Свойство неотрицательной рациональной продолжительности жизни, которая не изменяется входными событиями вместе с конечным числом состояний и событий, гарантирует, что поведение сетей SP-DEVS может быть абстрагировано как эквивалентный граф достижимости с конечными вершинами, абстрагируя бесконечно- много значений прошедшего времени.

Чтобы абстрагироваться от бесконечного числа случаев истекшего времени для каждого компонента сетей SP-DEVS, используется метод абстракции времени, называемый абстракция шкалы времени был введен [Hwang05],[HCZF07] в котором сохранены порядок и относительная разница расписаний. Используя технику абстракции шкалы времени, поведение любой сети SP-DEVS можно абстрагировать как граф достижимости, число вершин и ребер которого конечно.

Разрешимость безопасности

В качестве качественного свойства безопасность сети SP-DEVS может быть решена путем (1) создания графа достижимости конечных вершин данной сети и (2) проверки достижимости некоторых плохих состояний. [Hwang05].

Разрешимость жизни

В качестве качественного свойства живучесть сети SP-DEVS разрешима: (1) генерируя граф достижимости с конечными вершинами (RG) данной сети, (2) из RG, генерируя ядро ориентированный ациклический граф (KDAG), в котором вершина компонент сильной связности и (3) проверка того, содержит ли вершина KDAG цикл перехода состояний, который содержит набор состояний жизнеспособности[Hwang05].

Разрешимость минимального / максимального времени обработки

В качестве количественного свойства минимальные и максимальные границы времени обработки из двух событий в сетях SP-DEVS могут быть вычислены путем (1) создания графа достижимости с конечными вершинами и (2.a) путем нахождения кратчайших путей для минимального времени обработки. и (2.b) путем нахождения самых длинных путей (если они доступны) за максимальное время обработки. [HCZF07].

Недостатки

Меньшая выразительность: проблема OPNA

Пусть общее состояние ${ displaystyle (s, t_ {s}, t_ {e})}$ модели SP-DEVS быть пассивный если ${ displaystyle t_ {s} = infty}$ ; в противном случае это будет активный.

Одним из известных ограничений SP-DEVS является феномен, заключающийся в том, что «как только модель SP-DEVS становится пассивной, она больше никогда не становится активной (OPNA)». Это явление было впервые обнаружено [Hwang 05b] хотя изначально он назывался ODNR («если он умирает, он никогда не возвращается»). Причина, по которой это происходит, заключается в ограничении (3) выше, в котором никакое событие ввода не может изменить расписание, поэтому пассивное состояние не может быть пробуждено в активное состояние.

Например, модели тостеров, изображенные на рис. 3 (b), не являются SP-DEVS, потому что общее состояние, связанное с «бездействием» (I), является пассивным, но оно переходит в активное состояние «тост» (T), чье значение время составляет 20 секунд или 40 секунд. Фактически модель, показанная на рис. 3 (б), является FD-DEVS.

Инструмент

Существует библиотека с открытым исходным кодом под названием DEVS # по адресу http://xsy-csharp.sourceforge.net/DEVSsharp/, который поддерживает некоторые алгоритмы определения безопасности и живучести, а также ограничения времени обработки Min / Max.

Сноски

^ ${ displaystyle delta _ {y}}$ можно разделить на две функции: ${ displaystyle lambda: S rightarrow Y ^ { phi}}$ и ${ displaystyle delta _ {int}: S rightarrow S}$ как в [ZKP00].