유한 결정론적 이산 이벤트 시스템 사양

FD-DEVS(Finite & Deterministic Discretary Event System Specification)는 이산 이벤트 다이내믹 시스템을 시뮬레이션 및 검증 방식으로 모델링 및 분석하기 위한 형식주의입니다.FD-DEVS는 Classic DEVS에서 계승된 모듈러형 및 계층형 모델링 기능도 제공합니다.

역사

FD-DEVS는 원래 "스케줄 제어 가능한 DEVS"[Hwang05]로 명명되었으며 30년간 DEVS 형식주의의 미해결 문제였던 네트워크의 검증 분석을 지원하기 위해 설계되었습니다.또한 SP-DEVS의 이른바 "OPNA" 문제를 해결하기 위해 지정되었습니다.Classic DEVS의 관점에서 FD-DEVS에는 3가지 제약사항이 있습니다.

이벤트 세트 및 상태 세트의 정밀도,
국가의 수명은 합리적인 수나 무한대로 계획될 수 있다.
내부 일정을 보존하거나 입력 이벤트를 통해 업데이트할 수 있습니다.

세 번째 제한은 SP-DEVS로부터의 완화로도 볼 수 있습니다.SP-DEVS에서는 입력 이벤트에 의해 스케줄이 항상 유지됩니다.이 완화로 인해 OPNA의 문제는 없어졌지만 SP-DEVS 네트워크의 경과시간을 추상화하기 위해 사용할 수 있는 타임라인 추상화는 FD-DEVS 네트워크에서는 더 이상 유용하지 않다는 한 가지 제약이 있습니다[ Hwang05 ]하지만 또 다른 시간 추상화 방법[Dill89]은 교수에 의해 발명되었다.D. Dill은 FD-DEVS 네트워크의 유한 버텍스 도달 가능성 그래프를 얻기 위해 적용할 수 있습니다.

예

탁구 경기

그림 1: 탁구 게임용 FD-DEVS 결합도

2명의 플레이어가 있는 단일 ping-pong 매치를 검토합니다.각 플레이어는 FD-DEVS에 의해 모델화할 수 있으며, 플레이어 모델에는 입력 이벤트인 수신 이벤트와 출력 이벤트!send가 있으며, 두 가지 상태가 있습니다.전송 및 대기.플레이어가 "보내기"에 들어가면 "! 보내기"를 생성하고 전송 시간 0.1 시간 단위 이후 "대기"로 돌아갑니다.「Wait」에 머무르고 「?receive」가 되면, 재차 「Send」로 바뀝니다.즉, 플레이어 모델은 "?수신"되지 않는 한 "대기" 상태로 유지됩니다.

탁구를 완전히 일치시키기 위해 한 선수는 초기 상태가 "Send"인 공격자로 시작하고 다른 한 선수는 초기 상태가 "Wait"인 수비수로 시작합니다.그림 1에서 A선수가 초범이고 B선수가 초범이다.또, 게임을 계속하기 위해서는, 그림 1과 같이, 각 플레이어의 「?전송」이벤트를 다른 플레이어의 「?리시브」와 결합할 필요가 있습니다.

2 슬롯 토스터

그림 2: (a) 2 슬롯 토스터기 (b) 2 슬롯 토스터기용 FD-DEVS 결합도

그림 2(a)와 같이 두 개의 슬롯에 자체 시동 손잡이가 있는 토스터를 고려합니다.각 슬롯의 기능은 토스트 시간 이외에는 동일합니다.처음에는 노브를 누르지 않지만, 노브를 누르면 관련 슬롯이 건배 시간(왼쪽 슬롯은 20초, 오른쪽 슬롯은 40초) 동안 건배하기 시작합니다.건배 시간이 지나면, 각 슬롯과 그 노브가 팝업 됩니다.연결된 슬롯이 토스트 중일 때 노브를 누르려고 해도 아무 일도 일어나지 않습니다.

그림 2(b)와 같이 FD-DEVS로 모델링할 수 있다.2개의 슬롯은 원자성 FD-DEVS로 모델화되어 있습니다.입력 이벤트는 "?push"이고 출력 이벤트는 "!pop", 상태는 "Idle"(I) 및 "Toast"(T)이며 초기 상태는 "idle"(유휴)입니다."아이돌" 상태에서 "?push"(노브를 누르기 때문에)를 수신하면 상태가 "Toast"로 변경됩니다.즉, 「?push」이벤트를 수신하지 않는 한, 「Idle」에 영원히 머무릅니다.20초 후에 왼쪽(오른쪽) 슬롯은 「Idle」로 돌아옵니다.

아토믹 FD-DEVS

정식 정의

M=<X,Y,S,s_{0},\tau,\display_{x},\display_{y}>

어디에

$(\displaystyle$ X $)$ 는 $X$ 한정된 입력 이벤트 세트입니다.

$(\displaystyle$ Y $)$ 는 $Y$ 유한한 출력 이벤트 세트입니다.

$(\displaystyle$ S $)$ 는 $S$ 유한한 상태의 집합입니다.

$s_{0}\in S$ 0 $s_{0}\in S$ (\ $displaystyle s_{0}\in$ S $)$ 가 $s_{0}\in S$ 초기 상태입니다.

$]$ $S\rightarrow \mathbb {Q} _{[0,\infty$ $\mathbb {Q} _{[0,\infty ]}$ ]}는 $\tau :S\rightarrow \mathbb {Q} _{[0,\infty ]}$ $\mathbb {Q} _{[0,\infty ]}$ 상태의 수명을 정의하는 시간 진행 함수입니다.여기서 $\mathbb {Q} _{[0,\infty ]}$ [ 0 , $]$ \ $displaystyle \mathbb {$ Q} $_$ { { [ 0 , \ $infty$ ]}는 음이 아닌 유리수의 집합과 무한대입니다.

$1$ $S\times$ X $\rightarrow$ S $\times \{0,1\}$ 는 $\delta _{x}:S\times X\rightarrow S\times \{0,1\}$ 입력 이벤트가 시스템 상태 및 일정을 어떻게 변경하는지 정의하는 외부 전이 함수입니다. $상태$ $s의 내부$ 스케줄은 $\tau (s')$ $\delta _{x}(s)=(s',1)$ ( $\delta _{x}(s)=(s',1)$ ) $\delta _{x}(s)=(s',0)$ $\tau (s')$ ( s $、 1 )$ 의 $\tau (s')$ ( s $),$ ( s ), ( s ), ( s ), ( s ), ( s ), ( s ), ( s ), ( $\delta _{x}(s)=(s',0)$ $\delta _{x}(s)=(s',1)$ ), ( s ), ( $\delta _{x}(s)=(s',0)$ $),$ ( s $\delta _{x}(s)=(s',0)$ )에 $\tau (s')$ $\delta _{x}(s)=(s',0)$ 갱신됩니다.

$S$ $S\rightarrow$ Y $^{\phi}\times$ S $}$ 는 $\delta _{y}:S\rightarrow Y^{\phi }\times S$ 출력 및 내부 전이 함수입니다. $여기$ 서 Y $\phi \notin Y$ $Y^{\phi }=Y\cup \{\phi \}$ $y$ { $ϕ$ $Y^{\phi }=Y\cup \{\phi \}$ $= Y$ \ $cup$ \ { \ $phi \ }$ 는 $Y^{\phi }=Y\cup \{\phi \}$ $\phi \notin Y$ $\phi \notin Y$ 사일런트이벤트를 나타냅니다.출력 및 내부 전이 함수는 상태가 출력 이벤트를 생성하는 동시에 상태가 ^[2]내부에서 어떻게 변화하는지 정의합니다.

Ping-Pong 플레이어의 정식 표현

그림 1의 탁구 예에서 플레이어의 정식 표현은 다음과 같다.= -0, = {n1}: ={n2}}:{n2}을(를)로 보내십시오. 잘 됐군요. $\$ $display$ $\tau$ $\tau$ (전송) = 0.1, $=$ $\infty$ $\tau$ { $display$ style $\infty$ $\infty$ ; $\tau$ $\delta _{x}$ $\delta _{x}$ \ $display$ style $_$ { $x$ } (잠깐만요, ? $\delta _{y}$ ) $\delta _{x}$ = (전송, ? 수신) $display$ x x \ displaystyle $_$ { $\delta _{x}$ x} $\delta _{x}$ (전송 $,$ 1 ) = \ $displaystylearchyle$ ) $\delta _{y}$ $y$ $\delta _{y}$ \ $displaystyle _$ { $\delta _{y}$ y } $=$ ( ( \ $displaystyle$ \ phi $\phi$ , wait )

1 슬롯 토스터의 정식 표현

2 슬롯 토스터 그림 2(a)와 (b)의 슬롯의 공식 표현은 다음과 같습니다. $M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>$ $M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>$ < $M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>$ , $M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>$ , $M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>$ , $M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>$ 0 , $M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>$ 、 " , " $M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>$ , $M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>$ $>$ { { $display style$ M $= < X$ , $Y$ , S , $s$ _ { 0 } , \ $tau$ , \ display $style$ _{ x , \ $display$ $_$ { $x$ } , \ $display$ $_$ { $y$ > } 、 {displaysty } = $X$ $Y$ { $Y$ } } } 。오른쪽 슬롯의 경우 $(\displaystyle \infty$ $\infty$ $\tau$ $\infty$ ${\$ $displaystyle \infty$ $\delta _{y}$ $\infty$ 、 $\delta _{x}$ I 、 ? push ）、 $\delta _{x}$ \ $displaystyle$ _ { $x$ $\delta _{x}$ （ T 、 1 ）、 $x$ {\ {\ {\ {\ {\ {\ {\ {\ {\ {\ \ $\delta _{y}$ （ \ $displaystystyle$ ） $\delta _{y}$ 。 $\delta _{y}$ \ $displaystyle _$ { $\delta _{y}$ y } = ( $display$ \ $displaystyle$ \ phi $\phi$ , I )

횡단보도 신호등 제어기의 형식적 표현

전술한 바와 같이 FD-DEVS는 SP-DEVS의 완화입니다.즉, FD-DEVS는 SP-DEVS의 저녁 클래스입니다.본 위키피디아에서는 SP-DEVS에 사용되는 횡단보도 신호등 컨트롤러의 FD-DEVS 모델을 제공합니다. $M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>$ $X$ $M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>$ < $M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>$ , $M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>$ , $M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>$ , $M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>$ , $M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>$ " , " $M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>$ , " $>$ \ $display style$ M = < $X$ , $Y$ , $S$ , $s _$ { $0$ , \ $tau$ , \ $M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>$ $display style$ X $}$ = $X$ { } 。p}; $Y$ {\ $displaystyle$ Y $}$ $Y$ {!g:0, !g:1, !w:0, !w:1}; $S$ {\ $displaystyle$ S $}$ $s_{0}$ {BG, BW, G, G, GR, R, $s_{0}$ }; s ${$ $\tau$ $},$ $\tau$ \ $displaystyle$ (\ $b$ ${\$ { $displaystyle$ \ $\tau$ displaystyle $\tau$ = 2, $\tau$ $\tau$ { \ $displaystyle$ \ $\tau$ display $\tau$ $\tau$ = 26, $p$ { $displaystyle$ \ display $\delta _{x}$ $\tau$ ( D ) = 2 ; $\delta _{x}$ $\delta _{x}$ x \ $displaystyle _$ { $\delta _{x}$ x $\delta _{x}$ } ( G , p ) = ( G , ? p ) , $\delta _{x}$ ) 、 $\delta _{x}$ 、、、、、、、 $pppp$ \ displaystyp 、 \ $displaystylash$ { displaystyle \ displaystyle \ $d$ $\delta _{y}$ \ $displaystyle _$ { $\delta _{y}$ y $\delta _{y}$ } = ( ! w : 0 , G ) $、$ $\delta _{y}$ $y$ \ $\delta _{y}$ $displaystyle$ \ $phi$ $\phi$ } , G 、 $y$ $\delta _{y}$ $\phi$ $\$ displaystyle \ $\delta _{y}$ phi } , G $、$ $\delta _{y}$ y \ $displaystyle$ $_$ $\delta _{y}$ { g : 0 , R } = ( ! g : $\delta _{y}$ , R ) $δstylestylestyle$ ) $§$ $y {\displaystyle$ \displaystyle $_{$ y $\delta _{y}$ ( $\delta _{y}$ )=(!g:1, G);

FD-DEVS 모델의 동작

그림 3. 선수 A의 이벤트 세그먼트와 상태 궤적

FD-DEVS는 DEVS의 서브 클래스입니다.

FD-DEVS 모델 $M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>$ $M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>$ < $M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>$ , $M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>$ , $M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>$ , $M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>$ , " $M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>$ , " , " , " $M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>$ , " $>$ { $displaystyle$ M ${\mathcal {M}}=<X,Y,S',s_{0}',ta,\delta _{ext},\delta _{int},\lambda >$ < $M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>$ ${\mathcal {M}}=<X,Y,S',s_{0}',ta,\delta _{ext},\delta _{int},\lambda >$ , $Y$ , $s _$ { $0$ , \ $tau$ , \ $taru$ , \ $taru$ _ { x , \ $taru$ _ { $x }$ , \ ${\mathcal {M}}=<X,Y,S',s_{0}',ta,\delta _{ext},\delta _{int},\lambda >$ _ { y $M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>$ ${\mathcal {M}}=<X,Y,S',s_{0}',ta,\delta _{ext},\delta _{int},\lambda >$ $}$ ${\mathcal {M}}=<X,Y,S',s_{0}',ta,\delta _{ext},\delta _{int},\lambda >$ ) 、 ${\mathcal {M}}=<X,Y,S',s_{0}',ta,\delta _{ext},\delta _{int},\lambda >$ , ${\mathcal {M}}=<X,Y,S',s_{0}',ta,\delta _{ext},\delta _{int},\lambda >$ " , " " " " " " " " " " " " " " .

$M({$ displaystyle ${M})$ 의 ${\mathcal {M}}$ X $,$ $(Displaystyle$ X, Y $)$ 는 M $({displaystyle$ M $M$ 의 X, $Y$ 와 $X,Y$ 같다.
$\displaystyle S'=\{(s,t_{s}):s\in S,t_{s}\in \mathbb {T}^{\infty}\}$
$\displaystyle s_{0}'=(s_{0},\displays (s_{0})}}$
상태 $(s,t_{s})\in S'$ ( $(s,t_{s})\in S'$ , $(s,t_{s})\in S'$ $(s,t_{s})\in S'$ $(s,t_{s})\in S'$ \ $displaystyle ( s$ , $t$ _ { $s$ ) \ $in$ S $(s,t_{s})\in S'$ , $ta(s,t_{s})=t_{s}.$ a ( $ta(s,t_{s})=t_{s}.$ , $ta(s,t_{s})=t_{s}.$ ) $ta(s,t_{s})=t_{s}.$ $ta(s,t_{s})=t_{s}.$ s . $ta(s,t_{s})=t_{s}.$ \ $displaystyle$ ta ( $s$ , $t$ _ { s ) = $t$ _ { $s$ } 。 $}$
Given a state $(s,t_{s})\in S'$ and an input event $x\in X$ ,

$\displaystyle _{ext}(s,t_{s},t_{e},x)=syslog{case}(s',t_{s}-t_{e})&{\text{case}(s,x})=(s,0)\(s,\text(s)},{e}_cases}_cases}_cases}_cases}_cases}(s})&{e})_cases}_cases}_cases}_cases}'s}'s}'$

상태 $(s,t_{s})\in S'$ ( $(s,t_{s})\in S'$ , $(s,t_{s})\in S'$ s ) $(s,t_{s})\in S'$ $(s,t_{s})\in S'$ $′$ \ $displaystyle ($ $\delta _{int}(s,t_{s})=(s',\tau (s'))$ , $\delta _{int}(s,t_{s})=(s',\tau (s'))$ { $s$ ) \ $in$ S $'$ 、、 $\delta _{int}(s,t_{s})=(s',\tau (s'))$ s ; s ） = \ $displaystyle$ \ $int$ $s$ , $t$ _ { s } $\delta _{y}(s)=(y,s').$ ( $\delta _{y}(s)=(y,s').$ $\delta _{int}(s,t_{s})=(s',\tau (s'))$ , $\delta _{int}(s,t_{s})=(s',\tau (s'))$ _ { s , t $\delta _{int}(s,t_{s})=(s',\tau (s'))$ _ { s $\delta _{int}(s,t_{s})=(s',\tau (s'))$ } ) y $\delta _{int}(s,t_{s})=(s',\tau (s'))$ $\delta _{y}(s)=(y,s').$ ' $\delta _{y}(s)=(y,s').$ ) $\delta _{int}(s,t_{s})=(s',\tau (s'))$ ）。 $}$
상태 $(s,t_{s})\in S'$ ( $(s,t_{s})\in S'$ , $(s,t_{s})\in S'$ s ) $(s,t_{s})\in S'$ $(s,t_{s})\in S'$ $′$ \ $displaystyle ( s$ , $t$ $\lambda (s,t_{s})=y$ { $s$ ) \ $in$ S $(s,t_{s})\in S'$ $\lambda (s,t_{s})=y$ s , $\lambda (s,t_{s})=y$ ) $\lambda (s,t_{s})=y$ $\delta _{y}(s)=(y,s').$ $\delta _{y}(s)=(y,s').$ \ $displaystyle$ \ $displayda ($ $\delta _{y}(s)=(y,s').$ , $\delta _{y}(s)=(y,s').$ $\lambda (s,t_{s})=y$ _ { $s$ $\delta _{y}(s)=(y,s').$ } $=$ $\delta _{y}(s)=(y,s').$ } $。{ displaystyle$ \ { s $\delta _{y}(s)=(y,s').$ （ s , t _ t _ { s ; s ; s ; s ; s ; s ; s ; s ; s ) $\delta _{y}(s)=(y,s').$ ）） $\delta _{y}(s)=(y,s').$ (,,,,, 。 $}$

DEVS 동작의 상세한 것에 대하여는, 「Atomic DEVS 동작」을 참조해 주세요.

Ping-Pong 플레이어 A의 동작

그림 3은 그림 1에서 소개한 탁구 게임을 플레이하는 선수 A의 이벤트 세그먼트(위)와 관련 상태 궤적(아래)을 나타낸다.그림 3에서 플레이어 A의 상태는 (상태, 수명, 경과시간)=( $s,t_{s},t_{e}$ $s,t_{s},t_{e}$ s $s,t_{s},t_{e}$ $s,t_{s},t_{e}$ e $({$ s, $t_{s}, t_{$ e $s,t_{s},t_{e}$ 이며, 그림 3의 하단 선분은 경과시간 값을 나타낸다.플레이어 A의 초기 상태는 "Send"이고 라이프 타임이 0.1초이므로 (Send, 0.1, $t_{e}$ { $displaystyle t_{e$ 의 높이는 $(\$ 의 값인 0.1이 됩니다 $.$ (Wait, inf,^[3] 0)로 바뀐 후 $t_{e}$ 가 $t_{e}$ 리셋되면플레이어 A는 $t_{e}$ 가 $t_{e}$ $t_{e}$ 0이 $되는지$ 알 수 없습니다 $.$ 단, B선수는 0.1초 후에 A선수로 공을 반송하므로 A선수는 0.2시에 (송신, 0.10)으로 돌아갑니다.그 후, 0.1초 후에 플레이어 A의 상태가 되면(보내기, 0.1, 0.1), 플레이어 A는 다시 플레이어 B에게 공을 보내고(대기, inf, 0) 들어갑니다.따라서 "보내기"에서 "대기"로 이동하는 이 주기적 상태 전환은 영원히 지속됩니다.

그림 4. 토스터의 이벤트 세그먼트와 상태 궤적

토스터 동작

그림 4는 그림 2와 같이 왼쪽 슬롯의 이벤트 세그먼트(위)와 관련 상태 궤적(아래)을 나타내고 있으며, 그림 3과 같이 왼쪽 슬롯의 상태는 (상태, 수명, 경과시간)=( $s,$ $s,t_{s},t_{e}$ $,$ $t_{e$ 와 같이 그림 4와 같다.토스터의 초기 상태는 "I"이고 토스터의 수명은 무한이므로 (Wait, inf, $\$ 의 높이는 ?push 발생 시점에 따라 결정됩니다.그림 4는 40시에 푸시가 발생하고 토스터가 (T, 20, 0)로 바뀌는 경우를 나타낸다.그 후, 20초 후에 상태가 (T, 20, 20)가 되면, 토스터는 (Wait, inf, 0)로 돌아옵니다.또 언제 다시 "Tast"로 돌아갔는지 알 수 없습니다.그림 4는 90시에 푸시가 발생하여 토스터가 들어가는 경우입니다(T,20,0).시간 97에 다시 누르는 사람이 있어도 그 상태( $T,$ 20, 7)는 $\delta _{x}$ x x \ $displaystyle$ _ {x $($ T,?push)=(T, 1)이므로 전혀 변하지 않습니다.

이점

그림 5. 2 슬롯 토스터의 도달 가능성 그래프

시간대 추상화의 적용 가능성

유한한 수의 상태 및 이벤트와 함께 입력 이벤트에 의해 보존 또는 변경될 수 있는 음이 아닌 합리적인 값의 수명의 속성은 FD-DEVS 네트워크의 동작이 시간을 사용하여 무한히 많은 시간의 값을 추상화함으로써 동등한 유한-vertex 도달 가능성 그래프로 추상화될 수 있음을 보증합니다.교수님이 도입한 추상화 기법.D. Dill [Dill89]유한 버텍스 도달 가능성 그래프(RG)를 생성하는 알고리즘은 [HZ06a], [HZ07]에 도입되었습니다.

도달 가능성 그래프

그림 5는 그림 2와 같이 2 슬롯 토스터의 도달 가능성 그래프를 나타낸다.도달 가능성 그래프에서 각 정점은 t $t_{e1},t_{e2}$ , $t_{e1},t_{e2}$ e $($ 스타일 $t_{e1}, t_{e2$ }) 및 $t_{e1},t_{e2}$ $t_{e1}-t_{e2}$ e $t_{e1},t_{e2}$ 1 $t_{e1}-t_{e2}$ - $t_{e1}-t_{e2}$ $t_{e1}-t_{e2}$ $($ 스타일 $t_{e1}-t_{$ e2 $t_{e1}-t_{e2}$ 의 범위인 자체 이산 상태 및 시간대를 가진다. 예를 들어 그림 5의 노드(6)의 경우, 이산 상태 정보는 \ $in($ 표시 스타일 $)$ 이다. $0\leq t_{e1}\leq 40,0\leq t_{e2}\leq 40,-20\leq t_{e1}-t_{21}\leq 0$ 은 0 $0\leq t_{e1}\leq 40,0\leq t_{e2}\leq 40,-20\leq t_{e1}-t_{21}\leq 0$ $0\leq t_{e1}\leq 40,0\leq t_{e2}\leq 40,-20\leq t_{e1}-t_{21}\leq 0$ $0\leq t_{e1}\leq 40,0\leq t_{e2}\leq 40,-20\leq t_{e1}-t_{21}\leq 0$ 1 $0\leq t_{e1}\leq 40,0\leq t_{e2}\leq 40,-20\leq t_{e1}-t_{21}\leq 0$ $0\leq t_{e1}\leq 40,0\leq t_{e2}\leq 40,-20\leq t_{e1}-t_{21}\leq 0$ 、 $0\leq t_{e1}\leq 40,0\leq t_{e2}\leq 40,-20\leq t_{e1}-t_{21}\leq 0$ t $0\leq t_{e1}\leq 40,0\leq t_{e2}\leq 40,-20\leq t_{e1}-t_{21}\leq 0$ $0\leq t_{e1}\leq 40,0\leq t_{e2}\leq 40,-20\leq t_{e1}-t_{21}\leq 0$ $0\leq t_{e1}\leq 40,0\leq t_{e2}\leq 40,-20\leq t_{e1}-t_{21}\leq 0$ $0\leq t_{e1}\leq 40,0\leq t_{e2}\leq 40,-20\leq t_{e1}-t_{21}\leq 0$ 、 - $0\leq t_{e1}\leq 40,0\leq t_{e2}\leq 40,-20\leq t_{e1}-t_{21}\leq 0$ $0\leq t_{e1}\leq 40,0\leq t_{e2}\leq 40,-20\leq t_{e1}-t_{21}\leq 0$ e $0\leq t_{e1}\leq 40,0\leq t_{e2}\leq 40,-20\leq t_{e1}-t_{21}\leq 0$ - $0\leq t_{e1}\leq 40,0\leq t_{e2}\leq 40,-20\leq t_{e1}-t_{21}\leq 0$ 21 $0\leq t_{e1}\leq 40,0\leq t_{e2}\leq 40,-20\leq t_{e1}-t_{21}\leq 0$ 0 （ $displaystyle$ 0 \ $leq$ t _ { $e1}$ \ $leq$ 40 , $0$ \ $leq$ t _ 0 , 0 , 0 \ $leq$ t _ { $e2}$ \ $leq 40$ , $20$ \ $leq t _$ { $e1$ } 입니다 $0\leq t_{e1}\leq 40,0\leq t_{e2}\leq 40,-20\leq t_{e1}-t_{21}\leq 0$ 각 아치의 방향성을 나타냅니다.예를 들어 (6)에서 (5)로의 전이 호는 push1 이벤트에 의해 트리거된다.이 때, 아크의 세트 {1}는 (6)에서 (5)로의 이행시에 경과시간 1( $t_{e1}$ $t_{e1}$ ${$ 이 $t_{e1}$ 0 리셋 되는 것을 나타낸다.자세한 내용은 [HZ07]을 참조하십시오.

안전의 결정 가능성

질적 특성으로서 FD-DEVS 네트워크의 안전성은 (1) 특정 네트워크의 RG를 생성하고 (2) 일부 불량 상태가 도달 가능한지 여부를 체크함으로써 판단할 수 있다[HZ06b].

라이브스의 결정성

질적 특성으로서 (1) 소정의 네트워크의 RG를 생성하고 (2) RG에서 생성하며, (2) 정점이 강하게 접속된 커널 지향 비순환 그래프(KDAG)를 생성하고, (3) KDAG의 정점이 설정된 전이 사이클 상태를 포함하는지 여부를 체크함으로써 FD-DEVS 네트워크의 활성을 판정할 수 있다.HZ06b]

단점들

비결정론을 설명하기 위한 약한 표현력

FD-DEVS의 모든 특징 $\tau ,\delta _{x},\delta _{y}$ 인 $\tau ,\delta _{x},\delta _{y}$ $\tau ,\delta _{x},\delta _{y}$ $\tau ,\delta _{x},\delta _{y}$ , y $,$ \ $displaystyle \tau,$ \ $delta$ _{ $x},\delta$ _ ${y}$ 는 $\tau ,\delta _{x},\delta _{y}$ 비결정적 동작을 가진 시스템을 모델링하는 데 제약이 있다고 볼 수 있습니다.예를 들어 그림 1과 같은 탁구게임의 플레이어가 "Send" 상태에서 확률수명이 있는 경우 FD-DEVS는 비결정론을 효과적으로 포착하지 못한다.

도구.

검증용

안전성과 유효성을 찾기 위한 도달 가능성 그래프 기반 검증 알고리즘을 지원하는 2개의 오픈 소스 라이브러리 DEVS#(http://xsy-csharp.sourceforge.net/DEVSsharp/)과 XSY(https://code.google.com/p/x-s-y/)가 C#로 작성되어 있습니다.

XML을 통한 시뮬레이션의 경우

특히 FDDEVS를 사용한 DEVS의 표준화를 위해 Saurabh Mittal 박사는 동료들과 함께 FDDEVS의 XML 형식을 정의하는 작업을 수행해 왔습니다.http://www.duniptechnologies.com/research/xfddevs/에서 기사를 찾을 수 있습니다.이 표준 XML 형식은 UML 실행 [RCMZ09]에 사용되었습니다.

각주

^ $\delta _{x}$ $\rho :S\times X\rightarrow \{0,1\}$ $\delta _{x}$ \ $displaystyle$ \ $displaystyle$ _ $\delta _{x}$ { $\rho :S\times X\rightarrow \{0,1\}$ $\delta _{x}:S\times X\rightarrow S$ } $\rho :S\times X\rightarrow \{0,1\}$ : $\rho :S\times X\rightarrow \{0,1\}$ S × $\rho :S\times X\rightarrow \{0,1\}$ $\delta _{x}:S\times X\rightarrow S$ $\rho :S\times X\rightarrow \{0,1\}$ { $\rho :S\times X\rightarrow \{0,1\}$ , 1 $}$ { $\rho :S\times X\rightarrow \{0,1\}$ $displaystyle$ \ $rho$ : S \ $times$ X \ $\delta _{x}:S\times X\rightarrow S$ \ { $\delta _{x}:S\times X\rightarrow S$ 0 , $\rho :S\times X\rightarrow \{0,1\}$ 1 \ } $\delta _{x}:S\times X\rightarrow S$ : : : : : : : : $\delta _{x}:S\times X\rightarrow S$ s : : : : $s$ : : :2가지 기능으로 나눌 수 $\rho :S\times X\rightarrow \{0,1\}$ . $S\times$ X $\오른쪽 화살표$ S는 $\delta _{x}:S\times X\rightarrow S$ [Hwang05]와 같습니다.
^ $\delta _{y}$ \ $displaystyle$ \ $displayda _$ { y $\delta _{y}$ } $\lambda :S\rightarrow Y^{\phi }$ 、 $\lambda :S\rightarrow Y^{\phi }$ → $\lambda :S\rightarrow Y^{\phi }$ ϕ $\$ \ displayda : $\lambda :S\rightarrow Y^{\phi }$ 가지 기능으로 나눌 수 $\delta _{y}$ . $S\right 화살표$ Y $^{\phi$ }} 및 and $\lambda :S\rightarrow Y^{\phi }$ $\delta _{int}:S\rightarrow S$ t : $\delta _{int}:S\rightarrow S$ $\delta _{int}:S\rightarrow S$ \ $displaystyle$ \ $phi$ _ { $int :$ $[$ ZKP00]에서와 같이 S $\right$ 화살표 $\delta _{int}:S\rightarrow S$ S $.$
^ 그림 3의 inf는 $"\style\infty$ 를 의미합니다.

레퍼런스

[Dill89] D.L. Dill, "유한 상태 동시 시스템의 시간 설정 및 검증", 유한 상태 시스템의 컴퓨터 지원 검증 방법에 관한 워크숍 진행, 페이지 197-212, 프랑스 그르노블, 1989년
[ Hwang05 ]황M.H, "재구성 가능한 자동화 시스템의 유한 상태 글로벌 동작 생성: DEVS 접근법", 2005년 IEEE-CASE, 캐나다 에드먼턴, 2005년 8월 1일부터 2일까지 (http://moonho.hwang.googlepages.com/publications)에서 입수 가능)
[HZ06a] M. H. Hang 및 Bernard Zeigler, "유한하고 결정론적 DEVS를 사용한 모듈러 검증 프레임워크", 2006 DEVS 심포지엄 진행, pp57-65, 미국 앨라배마주 헌츠빌(http://www.acims.arizona.edu Archived 2012-07-26.26 Wayback Machine에서 입수 가능)
[HZ06b] M. H. Hang과 Bernard Zeigler, "A reachable Graph of Finite and Deterministic DEVS Networks", 2006 DEVS Sempium, pp48-56, 미국 앨라배마주 헌츠빌, http://www.acims.arizona.edu Archived 2012-07-26 Wayback Machine에서 입수 가능)
[HZ07] M.H. Hang과 Bernard Zeigler, "유한 결정론적 DEVS의 도달 가능성 그래프", 자동화 과학 및 엔지니어링에 관한 IEEE 트랜잭션, 제6권, 2009년 제3호, 페이지 454-467, http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?isnumber=5153598&arnumber=5071137&count=19&index=7
[RCMZ09] Josue L. Risco-Martin, Jesus M. de la Cruz, Saurabh Mittal 및 Bernard Zeigler, "eUDEVS: DEVS 모델링 및 시뮬레이션 이론을 사용한 실행 가능한 UML", "SIMUL, 트랜잭션"
[ZKP00]Bernard Zeigler, Tag Gon Kim, Herbert Praehofer (2000). Theory of Modeling and Simulation (second ed.). Academic Press, New York. ISBN 978-0-12-778455-7.{{cite book}}: CS1 maint: 여러 이름: 작성자 목록(링크)

[1] $\delta _{x}$ $\rho :S\times X\rightarrow \{0,1\}$ $\delta _{x}$ \ $displaystyle$ \ $displaystyle$ _ $\delta _{x}$ { $\rho :S\times X\rightarrow \{0,1\}$ $\delta _{x}:S\times X\rightarrow S$ } $\rho :S\times X\rightarrow \{0,1\}$ : $\rho :S\times X\rightarrow \{0,1\}$ S × $\rho :S\times X\rightarrow \{0,1\}$ $\delta _{x}:S\times X\rightarrow S$ $\rho :S\times X\rightarrow \{0,1\}$ { $\rho :S\times X\rightarrow \{0,1\}$ , 1 $}$ { $\rho :S\times X\rightarrow \{0,1\}$ $displaystyle$ \ $rho$ : S \ $times$ X \ $\delta _{x}:S\times X\rightarrow S$ \ { $\delta _{x}:S\times X\rightarrow S$ 0 , $\rho :S\times X\rightarrow \{0,1\}$ 1 \ } $\delta _{x}:S\times X\rightarrow S$ : : : : : : : : $\delta _{x}:S\times X\rightarrow S$ s : : : : $s$ : : :2가지 기능으로 나눌 수 $\rho :S\times X\rightarrow \{0,1\}$ . $S\times$ X $\오른쪽 화살표$ S는 $\delta _{x}:S\times X\rightarrow S$ [Hwang05]와 같습니다.

[2] $\delta _{y}$ \ $displaystyle$ \ $displayda _$ { y $\delta _{y}$ } $\lambda :S\rightarrow Y^{\phi }$ 、 $\lambda :S\rightarrow Y^{\phi }$ → $\lambda :S\rightarrow Y^{\phi }$ ϕ $\$ \ displayda : $\lambda :S\rightarrow Y^{\phi }$ 가지 기능으로 나눌 수 $\delta _{y}$ . $S\right 화살표$ Y $^{\phi$ }} 및 and $\lambda :S\rightarrow Y^{\phi }$ $\delta _{int}:S\rightarrow S$ t : $\delta _{int}:S\rightarrow S$ $\delta _{int}:S\rightarrow S$ \ $displaystyle$ \ $phi$ _ { $int :$ $[$ ZKP00]에서와 같이 S $\right$ 화살표 $\delta _{int}:S\rightarrow S$ S $.$

[3] 그림 3의 inf는 $"\style\infty$ 를 의미합니다.

[2]

[3]

Search