SP-DEVS

SP-DEVS는 "Schedule-Preserving Discrete Event System Specification(스케줄-보존 이산 이벤트 시스템 사양)"을 약칭하여 시뮬레이션 및 검증 방식으로 이산 이벤트 시스템을 모델링 및 분석하기 위한 형식주의입니다.SP-DEVS는 또한 Classic DEVS에서 계승된 모듈러형 및 계층형 모델링 기능도 제공합니다.

역사

SP-DEVS는 약 30년간 DEVS 형식주의의 미해결 문제였던 원래 네트워크의 유한 버텍스 도달 가능성 그래프를 확보함으로써 네트워크의 검증 분석을 지원하도록 설계되어 있습니다.이러한 네트워크 도달 가능성 그래프를 얻기 위해 SP-DEVS에는 다음 3가지 제약사항이 적용되어 있습니다.

이벤트 세트 및 상태 세트의 정밀도,
국가의 수명은 합리적인 수나 무한대로 계획될 수 있다.
외부 이벤트로부터 내부 일정을 유지합니다.

따라서 SP-DEVS는 DEVS와 FD-DEVS 양쪽의 서브 클래스입니다.이러한 3가지 제약에 의해 SP-DEVS 클래스는 상태 수가 유한한 경우에도 커플링 하에서 닫힙니다.이 속성은 SP-DEVS 커플링 모델을 사용하더라도 일부 정성적 속성과 정량적 속성에 대해 유한 버텍스 그래프 기반 검증을 가능하게 합니다.

횡단보도 컨트롤러의 예

시스템 요건 그림 1. 횡단보도 시스템 그림 2. 횡단보도 조명제어기 SP-DEVS 모델

횡단보도를 생각해 보세요.적색신호(응답보행금지신호)는 녹색신호(응답보행신호)와 반대방향으로 작용하기 때문에 간단하게는 녹색신호(G)와 보행신호(W)의 2가지 신호와 그림 1과 같이 누름버튼 1개만 고려한다.우리는 일련의 타이밍 제약으로 G와 W의 2개의 라이트를 제어하고 싶습니다.

두 개의 조명을 초기화하려면 G를 켜는 데 0.5초가 걸리고 0.5초 후에 W가 꺼집니다.그리고 30초마다 누군가 누름 버튼을 누르면 G가 꺼지고 W가 켜질 가능성이 있다.안전상의 이유로 G가 내린 지 2초 후에 W가 켜집니다.26초 후에 W가 내렸다가 2초 후에 G가 다시 켜집니다.이러한 동작은 반복됩니다.

컨트롤러 설계

위의 요건에 맞는 컨트롤러를 구축하기 위해 하나의 입력 이벤트 '푸시 버튼'(?p로 줄임말)과 4개의 출력 이벤트 '그린 온'(!g:1), '그린 오프'(!g:0), '워크 온'(!w:1) 및 '워크 오프'(!w:0)를 고려할 수 있습니다.컨트롤러의 상태 집합으로 booting-green(BG), booting-walk(BW), green-on(G), green-to-red(GR), red-on(R), walk-on(W), delay(D)를 고려한다.그림 2와 같이 상태 전이를 설계해 봅시다.처음에 컨트롤러는 수명이 0.5초인 BG부터 시작합니다.수명이 다한 후 이 순간 BW 상태로 이행하여 '그린온' 이벤트도 발생시킵니다.BW에 0.5초 머문 후 수명이 30초인 G 상태로 이행한다.컨트롤러는 출력 이벤트를 생성하지 않고 G를 G로 루프하여 G를 유지하거나 외부 입력 이벤트 ?p를 수신하면 GR 상태로 이동할 수 있습니다.단, GR에서의 실제 체류시간은 G에서의 루프에 대한 남은 시간입니다.GR에서 출력 이벤트 !g:0을 생성하고 R 상태를 2초간 유지한 후 출력 이벤트 !w:1을 포함한 W 상태로 이행합니다.26초 후 !w:0을 생성하는 D 상태로 이행하고 D에 2초간 머무른 후 출력 이벤트 g:1을 포함한 G로 돌아갑니다.

아토믹 SP-DEVS

정식 정의

위의 횡단보도 신호등 컨트롤러는 원자 SP-DEVS 모델로 모델링할 수 있습니다.정식적으로는 원자 SP-DEVS는 7 태플입니다.

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

$S$ $S\times$ X $\rightarrow$ S는 $\delta _{x}:S\times X\rightarrow S$ 입력 이벤트가 시스템 상태를 어떻게 변화시키는지 정의하는 외부 전이 함수입니다.

$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$ 사일런트이벤트를 나타냅니다.출력 및 내부 전이 함수는 상태가 출력 이벤트를 생성하는 동시에 상태가 ^[1]내부에서 어떻게 변화하는지 정의합니다.

횡단보도 관제사의 형식적 표현

그림 2와 같은 위의 컨트롤러는 M $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}>$ y $>$ \ $display$ M = < $X$ , $Y$ , $S$ , s $_$ { $0$ , \ $tau$ , \ $display$ _ { $x$ , \ $display _$ { $y$ } { } $X$ x x x x x x $M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>$ x x x x x x x x 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$ \display $\tau$ $\tau$ = $\tau$ , $§$ { $displaystyle$ \ $display$ $\neq$ $\tau$ ( $\delta _{x}$ ) = 2; $§$ $x$ \ $displaystyle _{$ x $\delta _{x}$ ( $\delta _{x}$ ,?p) = s $if$ { $displaystyle$ \ $}$ G; $\delta _{y}$ $style$ \ $display$ $;$ ${\displaystyle$ \displaystyle $\phi$ } $\phi$ =( $GR$ ) $\delta _{y}$ y \ $displaystyle$ \ $displaystyle$ _ ${$ $y$ $}$ =(!g:0, R), $\delta _{y}$ $\delta _{y}$ y \ $displaystyle _{y$ R) =(!w:1, W) {displaystyle $_y}$ =( $W!$

SP-DEVS 모델의 동작

그림 3. SP-DEVS 모델의 이벤트 세그먼트와 그 상태 궤적

원자 SP-DEVS의 역동성을 포착하려면 시간과 관련된 두 가지 변수를 도입해야 합니다.하나는 수명이고 다른 하나는 마지막 리셋 이후의 경과 시간입니다.Let $t_{s}\in \mathbb {Q} _{[0,\infty ]}$ be the lifespan which is not continuously increasing but set by when a discrete event happens. $t_{e}\in [0,\infty ]$ $t_{e}\in [0,\infty ]$ $t_{e}\in [0,\infty ]$ [ $t_{e}\in [0,\infty ]$ , $]{$ $displaystyle$ t $_$ { $e$ } \ $in$ [ $0$ , \ $infty$ ]}는 $t_{e}\in [0,\infty ]$ 리셋이 없는 경우 시간이 지남에 따라 지속적으로 증가하는 경과시간을 나타냅니다.

그림 3은 그림 2와 같이 SP-DEVS 모델의 이벤트 세그먼트와 관련된 상태 궤적을 나타낸다.그림 3의 상단은 수평 축이 시간 축인 이벤트 궤적을 나타내며, 예를 들어!g:1은 0.5에 발생하며!w:0은 1.0 시간 단위로 발생하는 등 이벤트가 발생하는 것을 보여줍니다.그림 3의 하단은 $s\in S$ $(\display style$ s $\in$ S $)$ 가 $s\in S$ 수명 및 경과 시간과 $(s,t_{s},t_{e})$ 되어 있는 상기 이벤트 세그먼트와 관련된 상태 궤적을 ( $(s,t_{s},t_{e})$ s , $(s,t_{s},t_{e})$ , $(s,t_{s},t_{e})$ $)\display$ style ( $s$ , $t_{s$ , $t_{e}$ $(s,t_{s},t_{e})$ 의 형태로 나타냅니다. 예를 들어 (G, 30, 11)는 G의 상태를 나타냅니다.경과시간은 11시간 단위입니다.그림 3 하단의 라인 세그먼트는 SP-DEVS의 유일한 연속 변수인 경과 시간의 흐름을 보여준다.

SF-DEVS의 한 가지 흥미로운 특징은 외부 사건 ?p가 발생하는 그림 3의 시각 47에 그려진 SP-DEVS의 제한 (3)을 일정으로 보존하는 것일 수 있다.현시점에서는 상태가 G에서 GR로 변화해도 경과시간은 변화하지 않기 때문에 시각 47에서 회선 세그먼트가 끊어지지 $t_{e}$ t $t_{e}$ {\ $displaystyle t_{$ e $t_{e}$ }}는 t $t_{e}$ {\ $displaystyle t_{$ e $t_{e}$ }(이 예에서는 30)까지 증가할 수 있습니다.입력 사건으로부터의 스케줄의 보존과 음이 아닌 유리 번호까지의 시간 진행의 제한(위의 제한 (2) 참조)으로 인해 SP-DEVS 모델에서 모든 톱의 높이는 음이 아닌 유리 번호 또는 무한대일 수 있다(그림 3의 하단에 표시).

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

SP-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$ , $\$ taru _ { x , \ taru ${\mathcal {M}}=<X,Y,S',s_{0}',ta,\delta _{ext},\delta _{int},\lambda >$ { x , \ ${\mathcal {M}}=<X,Y,S',s_{0}',ta,\delta _{ext},\delta _{int},\lambda >$ _ { $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 >$

$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$ } 。 $}$
$상태$ $(s,t_{s})\in S'$ , $(s,t_{s})\in S'$ ) $(s,t_{s})\in S'$ $(s,t_{s})\in S'$ \ $displaystyle$ $($ s , $x\in X,\delta _{ext}(s,t_{s},t_{e},x)=(s',t_{s}-t_{e}){\text{ if }}\delta _{x}(s,x)=s'.$ $(s,t_{s})\in S'$ _ { $s$ ) \ $in$ S ' $x\in X,\delta _{ext}(s,t_{s},t_{e},x)=(s',t_{s}-t_{e}){\text{ if }}\delta _{x}(s,x)=s'.$ an an $x\in X,\delta _{ext}(s,t_{s},t_{e},x)=(s',t_{s}-t_{e}){\text{ if }}\delta _{x}(s,x)=s'.$ an x x x x x x x x x x x x x x x x x x $x\in X,\delta _{ext}(s,t_{s},t_{e},x)=(s',t_{s}-t_{e}){\text{ if }}\delta _{x}(s,x)=s'.$ x x x x x x x x x x x x x x x x x x x x X $,$ t $x\in X,\delta _{ext}(s,t_{s},t_{e},x)=(s',t_{s}-t_{e}){\text{ if }}\delta _{x}(s,x)=s'.$ $x\in X,\delta _{ext}(s,t_{s},t_{e},x)=(s',t_{s}-t_{e}){\text{ if }}\delta _{x}(s,x)=s'.$ $x\in X,\delta _{ext}(s,t_{s},t_{e},x)=(s',t_{s}-t_{e}){\text{ if }}\delta _{x}(s,x)=s'.$ ) $x\in X,\delta _{ext}(s,t_{s},t_{e},x)=(s',t_{s}-t_{e}){\text{ if }}\delta _{x}(s,x)=s'.$ ( $x\in X,\delta _{ext}(s,t_{s},t_{e},x)=(s',t_{s}-t_{e}){\text{ if }}\delta _{x}(s,x)=s'.$ s $x\in X,\delta _{ext}(s,t_{s},t_{e},x)=(s',t_{s}-t_{e}){\text{ if }}\delta _{x}(s,x)=s'.$ $, t$ $x\in X,\delta _{ext}(s,t_{s},t_{e},x)=(s',t_{s}-t_{e}){\text{ if }}\delta _{x}(s,x)=s'.$ , e $x\in X,\delta _{ext}(s,t_{s},t_{e},x)=(s',t_{s}-t_{e}){\text{ if }}\delta _{x}(s,x)=s'.$ e, e, $x\in X,\delta _{ext}(s,t_{s},t_{e},x)=(s',t_{s}-t_{e}){\text{ if }}\delta _{x}(s,x)=s'.$ , t $x\in X,\delta _{ext}(s,t_{s},t_{e},x)=(s',t_{s}-t_{e}){\text{ if }}\delta _{x}(s,x)=s'.$ e, t, t $x\in X,\delta _{ext}(s,t_{s},t_{e},x)=(s',t_{s}-t_{e}){\text{ if }}\delta _{x}(s,x)=s'.$ e)가 입력된 경우, t, t, t, e, e, t, t, e, e, e, e, e, e)는 x $,$ e $x\in X,\delta _{ext}(s,t_{s},t_{e},x)=(s',t_{s}-t_{e}){\text{ if }}\delta _{x}(s,x)=s'.$ $}$
상태 $(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 ($ $\delta _{int}(s,t_{s})=(s',\tau (s')$ , t $_$ { $s$ ) \ $in$ S ' $(s,t_{s})\in S'$ } , 、 $\delta _{int}(s,t_{s})=(s',\tau (s')$ $\delta _{int}(s,t_{s})=(s',\tau (s')$ $\delta _{y}(s)=(y,s').$ $\delta _{int}(s,t_{s})=(s',\tau (s')$ \ $displaystyle$ \ $displaystyle$ _ { $\delta _{y}(s)=(y,s').$ $\delta _{int}(s,t_{s})=(s',\tau (s')$ } ( $s$ , t $_$ { s $\delta _{int}(s,t_{s})=(s',\tau (s')$ ) $\delta _{int}(s,t_{s})=(s',\tau (s')$ $\delta _{y}(s)=(y,s').$ ( s , $\delta _{y}(s)=(y,s').$ _ { $t$ _ { s , { s $\delta _{int}(s,t_{s})=(s',\tau (s')$ $}$ ) $\delta _{y}(s)=(y,s').$ \ in S ' ) （ $\delta _{y}(s)=(y,s').$ ) $\delta _{y}(s)=(y,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').$ (,,,,, 。 $}$

이점

타임라인 추상화의 적용 가능성

한정된 수의 상태 및 이벤트와 함께 입력 이벤트에 의해 변경되지 않는 음이 아닌 합리적 값의 수명의 속성은 경과된 시간의 무한 다수의 값을 추상화함으로써 SP-DEVS 네트워크의 동작을 동등한 유한-vertex 도달 가능성 그래프로 추상화할 수 있음을 보증합니다.

SP-DEVS 네트워크의 각 컴포넌트에 대해 무한히 많은 경과시간을 추상화하기 위해 타임라인 추상화라고 불리는 시간 추상화 방법이 도입되었습니다 [Hwang05].일정의 순서와 상대적 차이가 보존되는 HCZF07].타임라인 추상화 기법을 사용함으로써 SP-DEVS 네트워크의 동작을 정점과 에지의 수가 유한한 도달 가능성 그래프로 추상화할 수 있다.

안전의 결정 가능성

질적 특성으로서 SP-DEVS 네트워크의 안전성은 (1) 특정 네트워크의 유한 버텍스 도달 가능성 그래프를 생성하고 (2) 일부 불량 상태에 도달할 수 있는지 여부를 체크함으로써 결정됩니다 [Hwang05].

라이브스의 결정성

질적 특성으로서 (1) 소정의 네트워크의 유한 버텍스 도달 가능성 그래프(RG)를 생성하고, (2) RG로부터 (2) 정점이 강하게 접속되어 있는 커널 지향 비사이클 그래프(KDAG)를 생성하고, (3) 정점이 KDAG 상태를 포함하는지 여부를 체크함으로써 SP-DEVS 네트워크의 유효성을 판정할 수 있다.한 쌍의 활성 상태[황05]

최소/최대 처리 시간 범위 결정 가능성

정량적 속성으로서 SP-DEVS 네트워크 내의 2개의 이벤트로부터의 최소 및 최대 처리 시간 경계는 (1) 유한 가상 도달 가능성 그래프를 생성하고 (2) 최소 처리 시간 경계의 최단 경로를 찾고 (2) 최대 처리 시간 경계의 최단 경로(사용 가능한 경우)를 구함으로써 계산할 수 있습니다.CZF07]

단점들

표현력 저하: OPNA 문제

SP-DEVS 모델의 총 상태 $(s,t_{s},t_{e})$ s , $(s,t_{s},t_{e})$ , $(s,t_{s},t_{e})$ e ) $(s,t_{s},t_{e})$ { $displaystyle ( s$ , $t_{s$ , $t_{e$ } ) $t_{s}=\infty$ s $=$ \ $displaystyle t_{s$ $t_{s}=\infty$ 이면 $t_{s}=\infty$ 상태( $s$ , t_{e})로 $(s,t_{s},t_{e})$ 합니다.그렇지 않으면 활성화 됩니다.

이미 알려진 SP-DEVS의 제한 중 하나는 "SP-DEVS 모델이 일단 패시브 상태가 되면 활성화(OPNA)로 돌아가지 않는다"는 현상입니다.이 현상은 [Hwang 05b]에서 처음 발견되었는데, 원래는 ODNR(일단 죽으면 다시 돌아오지 않는다)로 불렸다.이것이 발생하는 이유는 위의 제한(3)에 의해 입력 이벤트가 일정을 변경할 수 없기 때문에 패시브스테이트가 액티브스테이트로 복귀할 수 없습니다.

예를 들어 그림 3(b)에 그려진 토스터 모델은 "아이돌"(I)과 관련된 전체 상태가 수동적이기 때문에 SP-DEVS가 아니지만 토스트 시간이 20초 또는 40초인 활성 상태인 "토스트"(T)로 이동한다.실제로 그림 3(b)의 모델은 FD-DEVS입니다.

도구.

http://xsy-csharp.sourceforge.net/DEVSsharp/,에는 DEVS#이라고 불리는 오픈소스 라이브러리가 있습니다.이 라이브러리는 최소/최대 처리 시간 범위뿐만 아니라 안전성과 유효성을 찾기 위한 알고리즘도 지원합니다.

각주

^ $\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 $.$

레퍼런스

[Hwang05] M. H. 황 "지도자:스케줄에 근거한 실시간 시스템 검증」, 2005년 DEVS 심포지엄, 샌디에이고, 2005년 4월 2일부터 8일까지, ISBN978-1-56555-293-7(http://moonho.hwang.googlepages.com/publications)에서 입수 가능)
[ Hwang05b ]M. H. Hang, "재구성 가능한 자동화 시스템의 유한 상태 글로벌 동작 생성: DEVS 접근법", 2005년 IEEE-CASE, 캐나다 에드먼턴, 2005년 8월 1-2일 (http://moonho.hwang.googlepages.com/publications)에서 입수 가능)
[HCZF07] M.H. 황, S.K. 조, 버나드 자이글러, F.Lin, "스케줄 보존 DEVS 처리 시간 범위", AIMS 테크니컬 리포트, 2007, (http://www.acims.arizona.edu 및 http://moonho.hwang.googlepages.com/publications)에서 입수 가능)
[Sedgewick02], R. Sedgewick, 알고리즘 in C++, Part 5 그래프 알고리즘, 애디슨 웨슬리, 보스턴, 제3판
[ZKP00] : CS1 유지보수 : 여러 이름 : 작성자 목록 (링크)

[1] $\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 $.$

[1]

Search