DEVS

DEVS, abbreviating discrete event system specification, is a modular and hierarchical formalism for modeling and analyzing general systems that can be discrete event systems which might be described by state transition tables, and continuous state systems which might be described by differential equations, and hybrid continuous state and discrete event systems. DEVS is a timed event system.

## Contents

* 1 History
* 2 Formalism
* 2.1 Intuitive example
* 2.2 Atomic DEVS
* 2.3 Coupled DEVS
* 3 Analysis methods
* 3.1 Simulation for discrete event systems
* 3.2 Simulation for continuous state systems
* 3.3 Verification for discrete event systems
* 4 Timed event system
* 5 Variations of DEVS
* 5.1 Extensions (superclassing)
* 5.2 Restrictions (subclassing)
* 6 Behavior
* 6.1 Atomic DEVS
* 6.1.1 View 1: total states = states * elapsed times
* 6.1.2 View 2: total states = states * lifespans * elapsed times
* 6.1.3 Comparison of view1 and view2
* 6.1.3.1 Features of view1
* 6.1.3.2 Features of view2
* 6.2 Coupled DEVS
* 6.2.1 View1: Total states = states * elapsed times
* 6.2.2 View2: Total states = states * lifespan * elapsed times
* 6.2.3 Time passage
* 6.2.3.1 For view1
* 6.2.3.2 For view2
* 7 Simulation algorithms
* 7.1 Atomic DEVS
* 7.1.1 Common parts
* 7.1.2 View 1: total states = states * elapsed times
* 7.1.3 View 2: total states = states * lifespans * elapsed times
* 7.2 Coupled DEVS
* 8 FD-DEVS
* 8.1 History
* 8.2 Examples
* 8.2.1 Ping-pong game
* 8.2.2 Two-slot toaster
* 8.3 Atomic FD-DEVS
* 8.3.1 Formal definition
* 8.3.2 Behaviors of FD-DEVS models
* 8.4 Advantages
* 8.4.1 Applicability of time-zone abstraction
* 8.4.2 Reachability graph
* 8.4.3 Decidability of safety
* 8.4.4 Decidability of liveness
* 8.5 Disadvantages
* 8.5.1 Weak expressiveness for describing nondeterminism
* 8.6 Tool
* 8.6.1 For verification
* 8.6.2 For simulation via XML
* 9 SP-DEVS
* 9.1 History
* 9.2 Crosswalk controller example
* 9.3 Atomic SP-DEVS
* 9.3.1 Formal definition
* 9.3.2 Behaviors of a SP-DEVS model
* 9.4 Advantages
* 9.5 Disadvantages
* 9.6 Tools
* 10 See also
* 10.1 DEVS-related articles
* 10.2 Other formalisms
* 11 References

## History

DEVS is a formalism for modeling and analysis of discrete event systems (DESs). The DEVS formalism was invented by Bernard P. Zeigler, who is emeritus professor at the University of Arizona. DEVS was introduced to the public in Zeigler's first book, Theory of Modeling and Simulation in 1976,[1] while Zeigler was an associate professor at University of Michigan. DEVS can be seen as an extension of the Moore machine formalism,[2] which is a finite state automaton where the outputs are determined by the current state alone (and do not depend directly on the input). The extension was done by

1. associating a lifespan with each state,[1]
2. providing a hierarchical concept with an operation, called coupling,[3]

Since the lifespan of each state is a real number (more precisely, non-negative real) or infinity, it is distinguished from discrete time systems, sequential machines, and Moore machines, in which time is determined by a tick time multiplied by non-negative integers. Moreover, the lifespan can be a random variable; for example the lifespan of a given state can be distributed exponentially or uniformly. The state transition and output functions of DEVS can also be stochastic.

Zeigler proposed a hierarchical algorithm for DEVS model simulation in 1984[4] which was published in Simulation journal in 1987. Since then, many extended formalism from DEVS have been introduced with their own purposes: DESS/DEVS for combined continuous and discrete event systems, P-DEVS for parallel DESs, G-DEVS for piecewise continuous state trajectory modeling of DESs, RT-DEVS for realtime DESs, cell-DEVS for cellular DESs, fuzzy-DEVS for fuzzy DESs, dynamic structuring DEVS for DESs changing their coupling structures dynamically, and so on. In addition to its extensions, there are some subclasses such as SP-DEVS and FD-DEVS have been researched for achieving decidability of system properties.

Due to the modular and hierarchical modeling views, as well as its simulation-based analysis capability, the DEVS formalism and its variations have been used in many application of engineering (such as hardware design, hardware/software codesign, communications systems, manufacturing systems) and science (such as biology, and sociology)

## Formalism

Fig. 1. A DEVS model for ping-pong game

### Intuitive example

DEVS defines system behavior as well as system structure. System behavior in DEVS formalism is described using input and output events as well as states. For example, for the ping-pong player of Fig. 1, the input event is ?receive, and the output event is !send. Each player, A, B, has its states: Send and Wait. Send state takes 0.1 seconds to send back the ball that is the output event !send, while the Wait state lasts until the player receives the ball that is the input event ?receive.

The structure of ping-pong game is to connect two players: player A's output event !send is transmitted to player B's input event ?receive, and vice versa.

In the classic DEVS formalism, atomic DEVS captures the system behavior, while coupled DEVS describes the structure of system.

The following formal definition is for classic DEVS.[5] In this article, we will use the time base, 𝕋=[0,∞) that is the set of non-negative real numbers; the extended time base,𝕋∞=[0,∞] that is the set of non-negative real numbers plus infinity.

### Atomic DEVS

An atomic DEVS model is defined as a 7-tuple

M=<X,Y,S,s0,ta,δext,δint,λ>

where

>   * X is the set of input events;
>   * Y is the set of output events;
>   * S is the set of sequential states (or also called the set of partial states);
>   * s0∈S is the initial state;
>   * ta:S->𝕋∞ is the time advance function which is used to determine the lifespan of a state;
>   * δext:Q×X->S is the external transition function which defines how an input event changes a state of the system, where Q={(s,te)|s∈S,te∈(𝕋∩[0,ta(s)])} is the set of total states, and te is the elapsed time since the last event;[6]
>   * δint:S->S is the internal transition function which defines how a state of the system changes internally (when the elapsed time reaches to the lifetime of the state);
>   * λ:S->Yϕ is the output function where Yϕ=Y∪{ϕ} and ϕ∉Y is a silent event or an unobserved event. This function defines how a state of the system generates an output event (when the elapsed time reaches to the lifetime of the state);

The atomic DEVS model for ping-pong players

The atomic DEVS model for player A of Fig. 1 is given player=

<X,Y,S,s0,ta,δext,δint,λ>

such that

> X={?receive}Y={!send}S={(d,σ)|d∈{Wait,Send},σ∈𝕋∞}s0=(Send,0.1)ta(s)=σ for all s∈Sδext(((Wait,σ),te),?receive)=(Send,0.1)δint(Send,σ)=(Wait,∞)δint(Wait,σ)=(Send,0.1)λ(Send,σ)=!sendλ(Wait,σ)=ϕ

Both player A and player B are atomic DEVS models.

Simply speaking, there are two cases that an atomic DEVS model M can change its state s∈S: (1) when an external input x∈X comes into the system M; (2) when the elapsed time te reaches the lifespan of s which is defined by ta(s). At the same time of (2), M generates an output y∈Y which is defined by λ(s).

For formal behavior description of given an atomic DEVS model, refer to the section about behavior of atomic DEVS. Computer algorithms to implement the behavior of a given atomic DEVS model are available in the section about simulation algorithms for atomic DEVS.

### Coupled DEVS

The coupled DEVS defines which sub-components belong to it and how they are connected with each other. A coupled DEVS model is defined as an 8-tuple

N=<X,Y,D,{Mi},Cxx,Cyx,Cyy,Select>

where

>   * X is the set of input events;
>   * Y is the set of output events;
>   * D is the name set of sub-components;
>   * {Mi} is the set of sub-components where for each i∈D,Mi can be either an atomic DEVS model or a coupled DEVS model.
>   * Cxx⊆X×⋃i∈DXi is the set of external input couplings;
>   * Cyx⊆⋃i∈DYi×⋃i∈DXi is the set of internal couplings;
>   * Cyy:⋃i∈DYi->Yϕ is the external output coupling function;
>   * Select:2D->D is the tie-breaking function which defines how to select the event from the set of simultaneous events;

The coupled DEVS model for ping-pong game

The ping-pong game of Fig. 1 can be modeled as a coupled DEVS model N=<X,Y,D,{Mi},Cxx,Cyx,Cyy,Select> where X={};Y={};D={A,B}; MA and MB is described as above; Cxx={}; Cyx={(A.!send,B.?receive),(B.!send,A.?receive)}; and Cyy(A.!send)=ϕ,Cyy(B.!send)=ϕ.

Simply speaking, like the behavior of the atomic DEVS class, a coupled DEVS model N changes its components' states (1) when an external event x∈X comes into N; (2) when one of components Mi where i∈D executes its internal state transition and generates its output yi∈Yi. In both cases (1) and (2), a triggering event is transmitted to all influences which are defined by coupling sets Cxx,Cyx, and Cyy.

For formal definition of behavior of the coupled DEVS, you can refer to the section about behavior of coupled DEVS. Computer algorithms to implement the behavior of a given coupled DEVS mode are available at the section about simulation algorithms for coupled DEVS.

## Analysis methods

### Simulation for discrete event systems

The simulation algorithm of DEVS models considers two issues: time synchronization and message propagation. Time synchronization of DEVS is to control all models to have the identical current time. However, for an efficient execution, the algorithm makes the current time jump to the most urgent time when an event is scheduled to execute its internal state transition as well as its output generation. Message propagation is to transmit a triggering message which can be either an input or output event along the associated couplings which are defined in a coupled DEVS model. For more detailed information, the reader can refer to simulation algorithms for atomic DEVS and simulation algorithms for coupled DEVS.

### Simulation for continuous state systems

By introducing a quantization method which abstracts a continuous segment as a piecewise const segment, DEVS can simulate behaviors of continuous state systems which are described by networks of differential algebraic equations. This research has been initiated by Zeigler in 1990s.[7] Many properties have been clarified by Prof. Kofman in 2000s and Dr. Nutaro. In 2006, Prof. Cellier who is the author of Continuous System Modeling,[8] and Prof. Kofman wrote a text book, Continuous System Simulation,[9] in which chapters 11 and 12 cover how DEVS simulates continuous state systems. Dr. Nutaro's book,[10] covers the discrete event simulation of continuous state systems too.[11]

### Verification for discrete event systems

As an alternative analysis method against the sampling-based simulation method, an exhaustive generating behavior approach, generally called verification has been applied for analysis of DEVS models. It is proven that infinite states of a given DEVS model (especially a coupled DEVS model ) can be abstracted by behaviorally isomorphic finite structure, called a reachability graph when the given DEVS model is a sub-class of DEVS such as schedule-preserving DEVS (SP-DEVS), finite & deterministic DEVS (FD-DEVS),[12] and finite & real-time DEVS (FRT-DEVS).[13] As a result, based on the reachability graph, (1) dead-lock and live-lock freeness as qualitative properties are decidable with SP-DEVS,[14] FD-DEVS,[15] and FRT-DEVS;[13] and (2) min/max processing time bounds as a quantitative property are decidable with SP-DEVS so far by 2012.

## Timed event system

The general system has been described by Zeigler[16][17] with the standpoints to define (1) the time base, (2) the admissible input segments, (3) the system states, (4) the state trajectory with an admissible input segment, (5) the output for a given state. A timed event system defining the state trajectory associated with the current and event segments came from the class of general system to allows non-deterministic behaviors in it.[18] Since the behaviors of DEVS can be described by timed event system, DEVS and RTDEVS is a sub-class or an equivalent class of timed event system.

A timed event system is a structure

𝒢=<Z,Q,Q0,QA,Δ>

where

* Z is the set of events;
* Q is the set of states;
* Q0⊆Q is the set of initial states;
* QA⊆Q is the set of accepting states;
* Δ⊆Q×ΩZ,[tl,tu]×Q is the set of state trajectories in which (q,ω,q′)∈Δ indicates that a state q∈Q can change into q′∈Q along with an event segment ω∈ΩZ,[tl,tu]. If two state trajectories (q1,ω1,q2) and (q3,ω2,q4)∈Δ are called contiguous if q2=q3, and two event trajectories ω1 and ω2 are contiguous. Two contiguous state trajectories (q,ω1,p) and (p,ω2,q′)∈Δ implies (q,ω1ω2,q′)∈Δ.

Given a timed event system

𝒢=<Z,Q,Q0,QA,Δ>

, the set of its behaviors is called its language depending on the observation time length. Let

be the observation time length. If

0≤t<∞

-length observation language of

is denoted by

L(𝒢,t)

, and defined as

L(𝒢,t)={ω∈ΩZ,[0,t]:∃(q0,ω,q)∈Δ,q0∈Q0,q∈QA}.

We call an event segment

ω∈ΩZ,[0,t]

-length behavior of

, if

ω∈L(𝒢,t)

. By sending the observation time length

to infinity, we define infinite length observation language of

is denoted by

L(𝒢,∞)

, and defined as

L(𝒢,∞)={ω∈limt->∞ΩZ,[0,t]:∃{q:(q0,ω,q)∈Δ,q0∈Q0}⊆QA}.

We call an event segment

ω∈limt->∞ΩZ,[0,t]

an infinite-length behavior of

, if

ω∈L(𝒢,∞) ω∈L(𝒢,∞)

## Variations of DEVS

### Extensions (superclassing)

Numerous extensions of the classic DEVS formalism have been developed in the last decades. Among them formalisms which allow to have changing model structures while the simulation time evolves.

G-DEVS,[19][20] parallel DEVS, dynamic structuring DEVS, cell-DEVS,[21] dynDEVS, fuzzy-DEVS, GK-DEVS, ml-DEVS, symbolic DEVS, real-time DEVS, rho-DEVS

### Restrictions (subclassing)

There are some sub-classes known as schedule-preserving DEVS (SP-DEVS) and finite and deterministic DEVS (FD-DEVS) which were designated to support verification analysis. SP-DEVS and FD-DEVS whose expressiveness are E(SP-DEVS) ⊂ E(FD-DEVS)⊂ E(DEVS) where E(formalism) denotes the expressiveness of formalism.

## Behavior

### Atomic DEVS

The behavior of a given DEVS model is a set of sequences of timed events including null events, called event segments, which make the model move from one state to another within a set of legal states. To define it this way, the concept of a set of illegal state as well a set of legal states needs to be introduced.

In addition, since the behavior of a given DEVS model needs to define how the state transition change both when time is passed by and when an event occurs, it has been described by a much general formalism, called general system.[22] In this article, we use a sub-class of general system formalism, called timed event system instead.

Depending on how the total state and the external state transition function of a DEVS model are defined, there are two ways to define the behavior of a DEVS model using timed event system. Since the behavior of a coupled DEVS model is defined as an atomic DEVS model, the behavior of coupled DEVS class is also defined by timed event system.

#### View 1: total states = states * elapsed times

Suppose that a DEVS model, ℳ=<X,Y,S,s0,ta,δext,δint,λ> has

1. the external state transition δext:Q×X->S.
2. the total state set Q={(s,te)|s∈S,te∈(𝕋∩[0,ta(s)])} where te denotes elapsed time since last event and 𝕋=[0,∞) denotes the set of non-negative real numbers, and

Then the DEVS model,

is a timed event system

𝒢=<Z,Q,Q0,QA,Δ>

where

>   * The event set Z=X∪Yϕ.
>   * The state set Q=QA∪QN where QN={s¯∉S}.
>   * The set of initial states Q0={(s0,0)}.
>   * The set of accepting states QA=ℳ.Q.
>   * The set of state trajectories Δ⊆Q×ΩZ,[tl,tu]×Q is defined for two different cases: q∈QN and q∈QA. For a non-accepting state q∈QN, there is no change together with any even segment ω∈ΩZ,[tl,tu] so (q,ω,q)∈Δ.

> For a total state q=(s,te)∈QA at time t∈𝕋 and an event segment ω∈ΩZ,[tl,tu] as follows.

> If unit event segment

> ω

> is the null event segment, i.e.

> ω=ϵ[t,t+dt]

> (q,ω,(s,te+dt))∈Δ.

> If unit event segment

> ω

> is a timed event

> ω=(x,t)

> where the event is an input event

> x∈X

> ,

> (q,ω,(δext(q,x),0))∈Δ.

> If unit event segment

> ω

> is a timed event

> ω=(y,t)

> where the event is an output event or the unobservable event

> y∈Yϕ

> ,

> {(q,ω,(δint(s),0))∈Δifte=ta(s),y=λ(s)(q,ω,s¯)otherwise.

Computer algorithms to simulate this view of behavior are available at simulation algorithms for atomic DEVS section.

#### View 2: total states = states * lifespans * elapsed times

Suppose that a DEVS model, ℳ=<X,Y,S,s0,ta,δext,δint,λ> has

1. the total state set Q={(s,ts,te)|s∈S,ts∈𝕋∞,te∈(𝕋∩[0,ts])} where ts denotes lifespan of state s, te denotes elapsed time since last tsupdate, and 𝕋∞=[0,∞)∪{∞} denotes the set of non-negative real numbers plus infinity,
2. the external state transition is δext:Q×X->S×{0,1}.

Then the DEVS

Q=𝒟

is a timed event system

𝒢=<Z,Q,Q0,QA,Δ>

where

>   * The event set Z=X∪Yϕ.
>   * The state set Q=QA∪QN where QN={s¯∉S}.
>   * The set of initial statesQ0={(s0,ta(s0),0)}.
>   * The set of acceptance states QA=ℳ.Q.
>   * The set of state trajectories Δ⊆Q×ΩZ,[tl,tu]×Q is depending on two cases: q∈QN and q∈QA. For a non-accepting state q∈QN, there is no changes together with any segment ω∈ΩZ,[tl,tu] so (q,ω,q)∈Δ.

> For a total state q=(s,ts,te)∈QA at time t∈𝕋 and an event segment ω∈ΩZ,[tl,tu] as follows.

> If unit event segment

> ω

> is the null event segment, i.e.

> ω=ϵ[t,t+dt]

> (q,ω,(s,ts,te+dt))∈Δ.

> If unit event segment

> ω

> is a timed event

> ω=(x,t)

> where the event is an input event

> x∈X

> ,

> {(q,ω,(s′,ta(s′),0))∈Δifδext(s,ts,te,x)=(s′,1),(q,ω,(s′,ts,te))∈Δotherwise,i.e.δext(s,ts,te,x)=(s′,0).

> If unit event segment

> ω

> is a timed event

> ω=(y,t)

> where the event is an output event or the unobservable event

> y∈Yϕ

> ,

> {(q,ω,(s′,ta(s′),0))∈Δifte=ts,y=λ(s),δint(s)=s′,(q,ω,s¯)∈Δotherwise.

Computer algorithms to simulate this view of behavior are available at simulation algorithms for atomic DEVS section.

#### Comparison of view1 and view2

##### Features of view1

View1 has been introduced by Zeigler[23] in which given a total state

q=(s,te)∈Q

and

ta(s)=σ

where

is the remaining time.[23][22] In other words, the set of partial states is indeed

S={(d,σ)|d∈S′,σ∈𝕋∞}

where

is a state set. When a DEVS model receives an input event

x∈X

, view1 resets the elapsed time

by zero, if the DEVS model needs to ignore

in terms of the lifespan control, modelers have to update the remaining time

σ=σ−te

in the external state transition function

δext

that is the responsibility of the modelers.

Since the number of possible values of σ is the same as the number of possible input events coming to the DEVS model, that is unlimited. As a result, the number of states s=(d,σ)∈S is also unlimited that is the reason why view2 has been proposed.

If we don't care the finite-vertex reachability graph of a DEVS model, view1 has an advantage of simplicity for treating the elapsed time te=0 every time any input event arrives into the DEVS model. But disadvantage might be modelers of DEVS should know how to manage σ as above, which is not explicitly explained in δext itself but in Δ.

##### Features of view2

View2 has been introduced by Hwang and Zeigler[24][25] in which given a total state

q=(s,ts,te)∈Q

, the remaining time,

is computed as

σ=ts−te.

When a DEVS model receives an input event

x∈X

, view2 resets the elapsed time

by zero only if

δext(q,x)=(s′,1)

. If the DEVS model needs to ignore

in terms of the lifespan control, modelers can use

δext(q,x)=(s′,0)

Unlike view1, since the remaining time σ is not component of S in nature, if the number of states, i.e. |S| is finite, we can draw a finite-vertex (as well as edge) state-transition diagram.[24][25] As a result, we can abstract behavior of such a DEVS-class network, for example SP-DEVS and FD-DEVS, as a finite-vertex graph, called reachability graph.[24][25]

### Coupled DEVS

DEVS is closed under coupling.[3][26] In other words, given a coupled DEVS model N, its behavior is described as an atomic DEVS model M. For a given coupled DEVS N, once we have an equivalent atomic DEVS M, behavior of M can be referred to behavior of atomic DEVS which is based on timed event system.

Similar to behavior of atomic DEVS, behavior of the coupled DEVS class is described depending on definition of the total state set and its handling as follows.

#### View1: Total states = states * elapsed times

Given a coupled DEVS model N=<X,Y,D,{Mi},Cxx,Cyx,Cyy,Select>, its behavior is described as an atomic DEVS model M=<X,Y,S,s0,ta,δext,δint,λ>

where

* X and Y are the input event set and the output event set, respectively.
* S=×i∈DQi is the partial state set where Qi={(si,tei)|si∈Si,tei∈(𝕋∩[0,tai(si)])} is the total state set of component i∈D (Refer to view1 of behavior of DEVS), where 𝕋=[0,∞) is the set of non-negative real numbers.
* s0=×i∈Dq0i is the initial state set where q0i=(s0i,0) is the total initial state of component i∈D.
* ta:S->𝕋∞ is the time advance function, where 𝕋∞=[0,∞] is the set of non-negative real numbers plus infinity. Given s=(…,(si,tei),…),

ta(s)=min⁡{tai(si)−tei|i∈D}.

* δext:Q×X->S is the external state function. Given a total state q=(s,te) where s=(…,(si,tei),…),te∈(𝕋∩[0,ta(s)]), and input event x∈X, the next state is given by

δext(q,x)=s′=(…,(si′,te′i),…)

where

(si′,te′i)={(δext(si,tei,xi),0)if (x,xi)∈Cxx(si,tei)otherwise.

Given the partial state

s=(…,(si,tei),…)∈S

, let

IMM(s)={i∈D|tai(si)=ta(s)}

denote the set of imminent components. The firing component

i*∈D

which triggers the internal state transition and an output event is determined by

i*=Select(IMM(s)).

* δint:S->S is the internal state function. Given a partial state s=(…,(si,tei),…), the next state is given by

δint(s)=s′=(…,(si′,te′i),…)

where

(si′,te′i)={(δint(si),0)if i=i*(δext(si,tei,xi),0)if (λi*(si*),xi)∈Cyx(si,tei)otherwise.

* λ:S->Yϕ is the output function. Given a partial state s=(…,(si,tei),…),

λ(s)={ϕif λi*(si*)=ϕCyy(λi*(si*))otherwise.

#### View2: Total states = states * lifespan * elapsed times

Given a coupled DEVS model N=<X,Y,D,{Mi},Cxx,Cyx,Cyy,Select>, its behavior is described as an atomic DEVS model M=<X,Y,S,s0,ta,δext,δint,λ>

where

* X and Y are the input event set and the output event set, respectively.
* S=×i∈DQi is the partial state set where Qi={(si,tsi,tei)|si∈Si,tsi∈𝕋∞,tei∈(𝕋∩[0,tsi])} is the total state set of component i∈D (Refer to view2 of behavior of DEVS section).
* s0=×i∈Dq0i is the initial state set where q0i=(s0i,tai(s0i),0) is the total initial state of component i∈D.
* ta:S->𝕋∞ is the time advance function. Given s=(…,(si,tsi,tei),…),

ta(s)=min⁡{tsi−tei|i∈D}.

* δext:Q×X->S×{0,1} is the external state function. Given a total state q=(s,ts,te) where s=(…,(si,tsi,tei),…),ts∈𝕋∞,te∈(𝕋∩[0,ts]), and input event x∈X, the next state is given by

δext(q,x)=((…,(si′,ts′i,te′i),…),b)

where

(si′,ts′i,te′i)={(si′,tai(si′),0)if (x,xi)∈Cxx,δext(si,tsi,tei,xi)=(si′,1)(si′,tsi,tei)if (x,xi)∈Cxx,δext(si,tsi,tei,xi)=(si′,0)(si,tsi,tei)otherwise

and

b={1if ∃i∈D:(x,xi)∈Cxx,δext(si,tsi,tei,xi)=(si′,1)0otherwise.

Given the partial state

s=(…,(si,tsi,tei),…)∈S

, let

IMM(s)={i∈D|tsi−tei=ta(s)}

denote the set of imminent components. The firing component

i*∈D

which triggers the internal state transition and an output event is determined by

i*=Select(IMM(s)).

* δint:S->S is the internal state function. Given a partial state s=(…,(si,tsi,tei),…), the next state is given by

δint(s)=s′=(…,(si′,ts′i,te′i),…)

where

(si′,ts′i,te′i)={(si′,tai(si′),0)if i=i*,δint(si)=si′,(si′,tai(si′),0)if (λi*(si*),xi)∈Cyx,δext(si,tsi,tei,xi)=(s′,1)(si′,tsi,tei)if (λi*(si*),xi)∈Cyx,δext(si,tsi,tei,xi)=(s′,0)(si,tsi,tei)otherwise.

* λ:S->Yϕ is the output function. Given a partial state s=(…,(si,tsi,tei),…),

λ(s)={ϕif λi*(si*)=ϕCyy(λi*(si*))otherwise.

#### Time passage

Since in a coupled DEVS model with non-empty sub-components, i.e., |D|>0, the number of clocks which trace their elapsed times are multiple, so time passage of the model is noticeable.

##### For view1

Given a total state q=(s,te)∈Q where s=(…,(si,tei),…)

If unit event segment

is the null event segment, i.e.

ω=ϵ[t,t+dt]

, the state trajectory in terms of timed event system is

Δ(q,ω)=((…,(si,tei+dt),…),te+dt).

##### For view2

Given a total state q=(s,ts,te)∈Q where s=(…,(si,tsi,tei),…)

If unit event segment

is the null event segment, i.e.

ω=ϵ[t,t+dt]

, the state trajectory in terms of timed event system is

Δ(q,ω)=((…,(si,tsi,tei+dt),…),ts,te+dt).

## Simulation algorithms

### Atomic DEVS

Given an atomic DEVS model, simulation algorithms are methods to generate the model's legal behaviors which are trajectories not to reach to illegal states. (see Behavior of DEVS). Zeigler originally introduced the algorithms that handle time variables related to lifespan

ts∈[0,∞]

and elapsed time

te∈[0,∞)

by introducing two other time variables, last event time,

tl∈[0,∞)

, and next event time

tn∈[0,∞]

with the following relations:[3]

te=t−tl

and

ts=tn−tl

where

t∈[0,∞)

denotes the current time. And the remaining time,

tr=ts−te

is equivalently computed as

tr=tn−t

, apparently

tr∈[0,∞]

Since the behavior of a given atomic DEVS model can be defined in two different views depending on the total state and the external transition function (refer to behavior of DEVS section), the simulation algorithms are also introduced in two different views as below.

#### Common parts

Regardless of two different views of total states, algorithms for initialization and internal transition cases are commonly defined as below.

DEVS-simulator
variables:
parent // parent coordinator
tl // time of last event
tn // time of next event
A=(X,Y,S,ta,δext,δint,λ)// the associated Atomic DEVS model
when receive init-message(Time t)
tl<-t;
tn<-tl+ta(s);
when receive star-message(Time t)
if t≠tn then
error: bad synchronization;
y<-λ(s);
send y-message(y,t) to parent;
s<-δint(s)
tl<-t;
tn<-tl+ta(s);

#### View 1: total states = states * elapsed times

As addressed in behavior of atomic DEVS section, when DEVS receives an input event, right calling δext, the last event time,tl is set by the current time,t, thus the elapsed timete becomes zero because te=t−tl.

when receive x-message(x∈X, Time t)
if (tl≤t and t≤tn) == false then
error: bad synchronization;
s<-δext(s,t−tl,x)
tl<-t;
tn<-tl+ta(s);

#### View 2: total states = states * lifespans * elapsed times

Notice that as addressed in behavior of atomic DEVS section, depending on the value of b return by δext, last event time,tl, and next event time,tn,consequently, elapsed time, te, and lifespantn, are updated (if b=1) or preserved (if b=0).

when receive x-message(x∈X, Time t)
if (tl≤t and t≤tn) == false then
error: bad synchronization;
(s,b)<-δext(s,t−tl,x)
if b=1 then
tl<-t;
tn<-tl+ta(s);

### Coupled DEVS

Given a coupled DEVS model, simulation algorithms are methods to generate the model's legal behaviors, which are a set of trajectories not to reach illegal states. (see behavior of a coupled DEVS model.) Zeigler originally introduced the algorithms that handle time variables related to lifespan

ts∈[0,∞]

and elapsed time

te∈[0,∞)

by introducing two other time variables, last event time,

tl∈[0,∞)

, and next event time

tn∈[0,∞]

with the following relations:[3]

te=t−tl

and

ts=tn−tl

where

t∈[0,∞)

denotes the current time. And the remaining time,

tr=ts−te

is equivalently computed as

tr=tn−t,

apparently

tr∈[0,∞]

. Based on these relationships, the algorithms to simulate the behavior of a given coupled DEVS are written as follows.

algorithm DEVS-coordinator
Variables:
parent // parent coordinator
tl: // time of last event
tn: // time of next event
N=(X,Y,D,{Mi},Cxx,Cyx,Cyy,Select) // the associated coupled DEVS model
when receive init-message(Time t)
for each i∈D do
send init-message(t) to child i
tl<-max⁡{tli:i∈D};
tn<-min⁡{tni:i∈D};
when receive star-message(Time t)
if t≠tn then
error: bad synchronization;
i*<-Select({i∈D:tni=tn});
send star-message(t)to i*
tl<-max⁡{tli:i∈D};
tn<-min⁡{tni:i∈D};
when receive x-message(x∈X, Time t)
if (tl≤t and t≤tn) == false then
error: bad synchronization;
for each (x,xi)∈Cxx do
send x-message(xi,t) to child i
tl<-max⁡{tli:i∈D};
tn<-min⁡{tni:i∈D};
when receive y-message(yi∈Yi, Time t)
for each (yi,xi)∈Cyx do
send x-message(xi,t) to child i
if Cyy(yi)≠ϕ then
send y-message(Cyy(yi), t) to parent;
tl<-max⁡{tli:i∈D};
tn<-min⁡{tni:i∈D};

## FD-DEVS

FD-DEVS (finite & deterministic discrete event system specification) is a formalism for modeling and analyzing discrete event dynamic systems in both simulation and verification ways. FD-DEVS also provides modular and hierarchical modeling features which have been inherited from Classic DEVS.

### History

FD-DEVS was originally named as schedule-controllable DEVS[27] and designed to support verification analysis of its networks which had been an open problem of DEVS formalism for 30 years. In addition, it was also designated to resolve the so-called "OPNA" problem of SP-DEVS. From the viewpoint of classic DEVS, FD-DEVS has three restrictions

1. finiteness of event sets and state set,
2. the lifespan of a state can be scheduled by a rational number or infinity, and
3. the internal schedule can be either preserved or updated by an input event.

The third restriction can be also seen as a relaxation from SP-DEVS where the schedule is always preserved by any input events. Due to this relaxation there is no longer OPNA problem, but there is also one limitation that a time-line abstraction which can be used for abstracting elapsed times of SP-DEVS networks is no longer useful for FD-DEVS network.[27] But another time abstraction method[28] which was invented by Prof. D. Dill can be applicable to obtain a finite-vertex reachability graph for FD-DEVS networks.

### Examples

#### Ping-pong game

Fig. 1: FD-DEVS coupled diagram for ping-pong game

Consider a single ping-pong match in which there are two players. Each player can be modeled by FD-DEVS such that the player model has an input event ?receive and an output event !send, and it has two states: Send and Wait. Once the player gets into "Send", it will generates "!send" and go back to "Wait" after the sending time which is 0.1 time unit. When staying at "Wait" and if it gets "?receive", it changes into "Send" again. In other words, the player model stays at "Wait" forever unless it gets "?receive".

To make a complete ping-pong match, one player starts as an offender whose initial state is "Send" and the other starts as a defender whose initial state is "Wait". Thus in Fig. 1. player A is the initial offender and player B is the initial defender. In addition, to make the game continue, each player's "?send" event should be coupled to the other player's "?receive" as shown in Fig. 1.

#### Two-slot toaster

Fig. 2: (a) Two-slot toaster (b) FD-DEVS coupled diagram for two-slot toaster

Consider a toaster in which there are two slots that have their own start knobs as shown in Fig. 2(a). Each slot has the identical functionality except their toasting time. Initially, the knob is not pushed, but if one pushes the knob, the associated slot starts toasting for its toasting time: 20 seconds for the left slot, 40 seconds for the right slot. After the toasting time, each slot and its knobs pop up. Notice that even though one tries to push a knob when its associated slot is toasting, nothing happens.

One can model it with FD-DEVS as shown in Fig. 2(b). Two slots are modeled as atomic FD-DEVS whose input event is "?push" and output event is "!pop", states are "Idle" (I) and "Toast" (T) with the initial state is "idle". When it is "Idle" and receives "?push" (because one pushes the knob), its state changes to "Toast". In other words, it stays at "Idle" forever unless it receives "?push" event. 20 (res. 40) seconds later the left (res. right) slot returns to "Idle".

### Atomic FD-DEVS

#### Formal definition

M=<X,Y,S,s0,τ,δx,δy>

where

>   * X is a finite set of input events;
>   * Y is a finite set of output events;
>   * S is a finite set of states;
>   * s0∈S is the initial state;
>   * τ:S->ℚ[0,∞] is the time advance function which defines the lifespan of a state where ℚ[0,∞] is the set of non-negative rational numbers plus infinity.
>   * δx:S×X->S×{0,1} is the external transition function which defines how an input event changes the schedule as well as a state of the system. The internal schedule of a state s∈S is updated by τ(s′) if δx(s)=(s′,1), otherwise(i.e., δx(s)=(s′,0)), the schedule is preserved.[29]
>   * δy:S->Yϕ×S is the output and internal transition function where Yϕ=Y∪{ϕ} and ϕ∉Y denotes the silent event. The output and internal transition function defines how a state generates an output event, at the same time, how the state changes internally.[30]

Formal representation of ping-pong player

The formal representation of the player in the ping-pong example shown in Fig. 1 can be given as follows. M=<X,Y,S,s0,τ,δx,δy> where X={?receive}; Y={!send}; S={Send, Wait}; s0=Send for player A, Wait for player B; τ(Send)=0.1,τ(Wait)=∞; δx(Wait,?receive)=(Send,1), δx(Send,?receive)=(Send,0); δy(Send)=(!send, Wait), δy(Wait)=(ϕ, Wait).

Formal representation of one slot toaster

The formal representation of the slot of Two-slot Toaster Fig. 2(a) and (b) can be given as follows. M=<X,Y,S,s0,τ,δx,δy> where X={?push}; Y={!pop}; S={I, T}; s0=I; τ(T)=20 for the left slot, 40 for the right slot, τ(I)=∞; δx(I, ?push)=(T,1), δx(T,?push)=(T,0); δy(T)=(!pop, I), δy(I)=(ϕ, I).

Formal representation of crosswalk light controller

As mentioned above, FD-DEVS is an relaxation of SP-DEVS. That means, FD-DEVS is a supper class of SP-DEVS. We would give a model of FD-DEVS of a crosswalk light controller which is used for SP-DEVS in this Wikipedia. M=<X,Y,S,s0,τ,δx,δy> where X={?p}; Y={!g:0, !g:1, !w:0, !w:1}; S={BG, BW, G, GR, R, W, D}; s0=BG, τ(BG)=0.5,τ(BW)=0.5, τ(G)=30, τ(GR)=30,τ(R)=2, τ(W)=26, τ(D)=2; δx(G,?p)=(GR,0), δx(s,?p)=(s,0) if s ≠G; δy(BG)=(!g:1, BW), δy(BW)=(!w:0, G),δy(G)=(ϕ, G), δy(GR)=(!g:0, R), δy(R)=(!w:1, W), δy(W)=(!w:0, D), δy(D)=(!g:1, G);

#### Behaviors of FD-DEVS models

Fig. 3. An event segment and a state trajectory of player A

FD-DEVS is a sub-class of DEVS

A FD-DEVS model, M=<X,Y,S,s0,τ,δx,δy> is DEVS ℳ=<X,Y,S′,s0′,ta,δext,δint,λ> where

* X,Y of ℳ are the same as those of M.
* S′={(s,ts):s∈S,ts∈𝕋∞}
* s0′=(s0,τ(s0))
* Given a state (s,ts)∈S′, ta(s,ts)=ts.
* Given a state (s,ts)∈S′ and an input event x∈X,

δext(s,ts,te,x)={(s′,ts−te)if δx(s,x)=(s′,0)(s′,τ(s′))if δx(s,x)=(s′,1)

* Given a state (s,ts)∈S′, δint(s,ts)=(s′,τ(s′)) if δy(s)=(y,s′).
* Given a state (s,ts)∈S′, λ(s,ts)=y if δy(s)=(y,s′).

For details of DEVS behavior, the readers can refer to behavior of atomic DEVS section.

Behavior of ping-pong player A

Fig. 3. shows an event segment (top) and the associated state trajectory (bottom) of player A who plays the ping-pong game introduced in Fig. 1. In Fig. 3. the status of player A is described as (state, lifespan, elapsed time)=(s,ts,te) and the line segment of the bottom of Fig. 3. denotes the value of the elapsed time. Since the initial state of player A is "Send" and its lifetime is 0.1 seconds, the height of (Send, 0.1, te) is 0.1 which is the value of ts. After changing into (Wait, inf, 0) when te is reset by 0, player A doesn't know when te becomes 0 again. However, since player B sends back the ball to player A 0.1 second later, player A gets back to (Send, 0.1 0) at time 0.2. From that time, 0.1 seconds later when player A's status becomes (Send, 0.1, 0.1), player A sends back the ball to player B and gets into (Wait, inf, 0). Thus, this cyclic state transitions which move "Send" to "Wait" back and forth will go forever.

Fig. 4. An event segment and a state trajectory of a toaster

Behavior of a toaster

Fig. 4. shows an event segment (top) and the associated state trajectory (bottom) of the left slot of the two-slot toaster introduced in Fig. 2. Like Fig.3, the status of the left slot is described as (state, lifespan, elapsed time)=(s,ts,te) in Fig. 4. Since the initial state of the toaster is "I" and its lifetime is infinity, the height of (Wait, inf, te) can be determined by when ?push occurs. Fig. 4. illustrates the case ?push happens at time 40 and the toaster changes into (T, 20, 0). From that time, 20 seconds later when its status becomes (T, 20, 20), the toaster gets back to (Wait, inf, 0) where we don't know when it gets back to "Toast" again. Fig. 4. shows the case that ?push occurs at time 90 so the toaster get into (T,20,0). Notice that even though there someone push again at time 97, that status (T, 20, 7) doesn't change at all because δx(T,?push)=(T,1).

### Advantages

Fig. 5. Reachability Graph of Two-slot Toaster

#### Applicability of time-zone abstraction

The property of non-negative rational-valued lifespans which can be preserved or changed by input events along with finite numbers of states and events guarantees that the behavior of FD-DEVS networks can be abstracted as an equivalent finite-vertex reachability graph by abstracting the infinitely-many values of the elapsed times using the time abstracting technique introduced by Prof. D. Dill.[28] An algorithm generating a finite-vertex reachability graph (RG) has been introduced by Zeigler.[25][31]

#### Reachability graph

Fig. 5. shows the reachability graph of two-slot toaster which was shown in Fig. 2. In the reachability graph, each vertex has its own discrete state and time zone which are ranges of te1,te2 and te1−te2. For example, for node (6) of Fig. 5, discrete state information is ((E,∞),(T,40)), and time zone is 0≤te1≤40,0≤te2≤40,−20≤te1−t21≤0. Each directed arch shows how its source vertex changes into the destination vertex along with an associated event and a set of reset models. For example, the transition arc (6) to (5) is triggered by push1 event. At that time, the set {1} of the arc denotes that elapsed time of 1 (that is te1 is reset by 0 when transition (6) to (5) occurs.[25]

#### Decidability of safety

As a qualitative property, safety of a FD-DEVS network is decidable by (1) generating RG of the given network and (2) checking whether some bad states are reachable or not.[24]

#### Decidability of liveness

As a qualitative property, liveness of a FD-DEVS network is decidable by (1) generating RG of the given network, (2) from RG, generating kernel directed acyclic graph (KDAG) in which a vertex is strongly connected component, and (3) checking if a vertex of KDAG contains a state transition cycle which contains a set of liveness states.[24]

### Disadvantages

#### Weak expressiveness for describing nondeterminism

The features that all characteristic functions,τ,δx,δy of FD-DEVS are deterministic can be seen as somehow a limitation to model the system that has non-deterministic behaviors. For example, if a player of the ping-pong game shown in Fig. 1. has a stochastic lifespan at "Send" state, FD-DEVS doesn't capture the non-determinism effectively.

### Tool

#### For verification

There are two open source libraries DEVS# written in C#[32] and XSY written in Python[33] that support some reachability graph-based verification algorithms for finding safeness and liveness.

#### For simulation via XML

For standardization of DEVS, especially using FDDEVS, Dr. Saurabh Mittal together with co-workers has worked on defining of XML format of FDDEVS.[34] This standard XML format was used for UML execution.[35]

## SP-DEVS

SP-DEVS (schedule-preserving discrete event system specification) is a formalism for modeling and analyzing discrete event systems in both simulation and verification ways. SP-DEVS also provides modular and hierarchical modeling features which have been inherited from the classic DEVS.

### History

SP-DEVS has been designed to support verification analysis of its networks by guaranteeing to obtain a finite-vertex reachability graph of the original networks, which had been an open problem of DEVS formalism for roughly 30 years. To get such a reachability graph of its networks, SP-DEVS has been imposed the three restrictions:

1. finiteness of event sets and state set,
2. the lifespan of a state can be scheduled by a rational number or infinity, and
3. preserving the internal schedule from any external events.

Thus, SP-DEVS is a sub-class of both DEVS and FD-DEVS. These three restrictions lead that SP-DEVS class is closed under coupling even though the number of states are finite. This property enables a finite-vertex graph-based verification for some qualitative properties and quantitative property, even with SP-DEVS coupled models.

### Crosswalk controller example

System requirementsFig. 1. Crosswalk systemFig. 2. SP-DEVS model for crosswalk light controller

Consider a crosswalk system. Since a red light (resp. don't-walk light) behaves the opposite way of a green light (resp. walk light), for simplicity, we consider just two lights: a green light (G) and a walk light (W); and one push button as shown in Fig. 1. We want to control two lights of G and W with a set of timing constraints.

To initialize two lights, it takes 0.5 seconds to turn G on and 0.5 seconds later, W gets off. Then, every 30 seconds, there is a chance that G becomes off and W on if someone pushed the push button. For a safety reason, W becomes on two seconds after G got off. 26 seconds later, W gets off and then two seconds later G gets back on. These behaviors repeats.

Controller Design

To build a controller for above requirements, we can consider one input event 'push-button' (abbreviated by ?p) and four output events 'green-on' (!g:1), 'green-off' (!g:0), 'walk-on' (!w:1) and 'walk-off (!w:0) which will be used as commands signals for the green light and the walk light. As a set of states of the controller, we considers 'booting-green' (BG), 'booting-walk' (BW), 'green-on' (G), 'green-to-red' (GR), 'red-on' (R), 'walk-on' (W), 'delay' (D). Let's design the state transitions as shown in Fig. 2. Initially, the controller starts at BG whose lifespan is 0.5 seconds. After the lifespan, it moves to BW state at this moment, it generates the 'green-on' event, too. After 0.5 seconds staying at BW, it moves to G state whose lifespan is 30 seconds. The controller can keep staying at G by looping G to G without generating any output event or can move to GR state when it receives the external input event ?p. But, the actual staying time at GR is the remaining time for looping at G. From GR, it moves to R state with generating an output event !g:0 and its R state last two seconds then it will move to W state with output event !w:1. 26 seconds later, it moves to D state with generating !w:0 and after staying 2 seconds at D, it moves back to G with output event !g:1.

### Atomic SP-DEVS

#### Formal definition

The above controller for crosswalk lights can be modeled by an atomic SP-DEVS model. Formally, an atomic SP-DEVS is a 7-tuple M=<X,Y,S,s0,τ,δx,δy>

where

* X is a finite set of input events;
* Y is a finite set of output events;
* S is a finite set of states;
* s0∈S is the initial state;
* τ:S->ℚ[0,∞] is the time advanced function which defines the lifespan of a state where ℚ[0,∞] is the set of non-negative rational numbers plus infinity.
* δx:S×X->S is the external transition function which defines how an input event changes a state of the system.
* δy:S->Yϕ×S is the output and internal transition function where Yϕ=Y∪{ϕ} and ϕ∉Y denotes the silent event. The output and internal transition function defines how a state generates an output event, at the same time, how the state changes internally.[36]

Formal representation of crosswalk controller

The above controller shown in Fig. 2 can be written as M=<X,Y,S,s0,τ,δx,δy> where X={?p}; Y={!g:0, !g:1, !w:0, !w:1}; S={BG, BW, G, GR, R, W, D}; s0=BG, τ(BG)=0.5,τ(BW)=0.5, τ(G)=30, τ(GR)=30,τ(R)=2, τ(W)=26, τ(D)=2; δx(G,?p)=GR, δx(s,?p)=s if s ≠G; δy(BG)=(!g:1, BW), δy(BW)=(!w:0, G),δy(G)=(ϕ, G), δy(GR)=(!g:0, R), δy(R)=(!w:1, W), δy(W)=(!w:0, D), δy(D)=(!g:1, G);

#### Behaviors of a SP-DEVS model

Fig. 3. Event segment and its state trajectory of SP-DEVS model

To captured the dynamics of an atomic SP-DEVS, we need to introduce two variables associated to time. One is the lifespan, the other is the elapsed time since the last resetting. Let ts∈ℚ[0,∞] be the lifespan which is not continuously increasing but set by when a discrete event happens. Let te∈[0,∞] denote the elapsed time which is continuously increasing over time if there is no resetting.

Fig.3. shows a state trajectory associated with an event segment of the SP-DEVS model shown in Fig. 2. The top of Fig.3. shows an event trajectory in which the horizontal axis is a time axis so it shows an event occurs at a certain time, for example, !g:1 occurs at 0.5 and !w:0 at 1.0 time unit, and so on. The bottom of Fig. 3 shows the state trajectory associated with the above event segment in which the state s∈S is associated with its lifespan and its elapsed time in the form of (s,ts,te). For example, (G, 30, 11) denotes that the state is G, its lifespan is and the elapsed time is 11 time units. The line segments of the bottom of Fig. 3 shows the time flow of the elapsed time which is the only one continuous variable in SP-DEVS.

One interesting feature of SF-DEVS might be the preservation of schedule the restriction (3) of SP-DEVS which is drawn at time 47 in Fig. 3. when the external event ?p happens. At this moment, even though the state can change from G to GR, the elapsed time does not change so the line segment is not broken at time 47 and te can grow up to te which is 30 in this example. Due to this preservation of the schedule from input events as well as the restriction of the time advance to the non-negative rational number (see restriction (2) above), the height of every saw can be a non-negative rational number or infinity (as shown in the bottom of Fig. 3.) in a SP-DEVS model.

SP-DEVS is a sub-class of DEVS

A SP-DEVS model, M=<X,Y,S,s0,τ,δx,δy> is DEVS ℳ=<X,Y,S′,s0′,ta,δext,δint,λ> where

* X,Y of ℳ are the same as those of M.
* S′={(s,ts):s∈S,ts∈𝕋∞}
* s0′=(s0,τ(s0))
* Given a state (s,ts)∈S′, ta(s,ts)=ts.
* Given a state (s,ts)∈S′ and an input event x∈X,δext(s,ts,te,x)=(s′,ts−te) if δx(s,x)=s′.
* Given a state (s,ts)∈S′, δint(s,ts)=(s′,τ(s′) if δy(s)=(y,s′).
* Given a state (s,ts)∈S′, λ(s,ts)=y if δy(s)=(y,s′).

### Advantages

* Applicability of time-line abstraction

The property of non-negative rational-valued lifespans which are not changed by input events along with finite numbers of states and events guarantees that the behavior of SP-DEVS networks can be abstracted as an equivalent finite-vertex reachability graph by abstracting the infinitely-many values of the elapsed times.

To abstract the infinitely-many cases of elapsed times for each components of SP-DEVS networks, a time-abstraction method, called the time-line abstraction has been introduced in which the orders and relative difference of schedules are preserved.[37][38] By using the time-line abstraction technique, the behavior of any SP-DEVS network can be abstracted as a reachability graph whose numbers of vertices and edges are finite.

* Decidability of safety

As a qualitative property, safety of a SP-DEVS network is decidable by (1) generating the finite-vertex reachability graph of the given network and (2) checking whether some bad states are reachable or not.[37]

* Decidability of liveness

As a qualitative property, liveness of a SP-DEVS network is decidable by (1) generating the finite-vertex reachability graph (RG) of the given network, (2) from RG, generating kernel directed acyclic graph (KDAG) in which a vertex is strongly connected component, and (3) checking if a vertex of KDAG contains a state transition cycle which contains a set of liveness states.[37]

* Decidability of min/max processing time bounds

As a quantitative property, minimum and maximum processing time bounds from two events in SP-DEVS networks can be computed by (1) generating the finite-vertex reachability graph and (2.a) by finding the shortest paths for the minimum processing time bound and (2.b) by finding the longest paths (if available) for the maximum processing time bound.[38]

### Disadvantages

* Less expressiveness: OPNA problem

Let a total state (s,ts,te) of a SP-DEVS model be passive if ts=∞; otherwise, it be active.

One of known SP-DEVS's limitation is a phenomenon that "once an SP-DEVS model becomes passive, it never returns to become active (OPNA)". This phenomenon was found first by Hwang,[39] although it was originally called ODNR ("once it dies, it never returns"). The reason why this one happens is because of the restriction (3) above in which no input event can change the schedule so the passive state can not be awaken into the active state.

For example, the toaster models drawn in Fig. 3(b) are not SP-DEVS because the total state associated with "idle" (I), is passive but it moves to an active state, "toast" (T) whose toasting time is 20 seconds or 40 seconds. Actually, the model shown in Fig. 3(b) is FD-DEVS.

### Tools

There is an open source library, called DEVS#[32] that supports some algorithms for finding safeness and liveness as well as min/max processing time bounds.

## See also

### DEVS-related articles

* Event segment
* Timed event system
* PowerDEVS

### Other formalisms

* Automata theory: a formal method for state transition systems
* Finite-state machine: a state transition machine with finite sets of events and states
* Petri nets: a graphical representation of state and transition relations
* Markov chain: a stochastic process in which the future will be determined by the current state
* Specification and Description Language: SDL, a formal complete and unambiguous language to graphically represent simulation models.

## References

1. ↑ 1.0 1.1 Zeigler, Bernard (1976). Theory of Modeling and Simulation (1st ed.). New York: Wiley Interscience. ISBN 0-12-778455-1. http://acims.asu.edu/publications/books-proceedings-and-manuscripts/theory-of-modeling-and-simulation-2nd-edition-academic-press.
2. ↑ Zeigler, Bernard (1968). On the Feedback Complexity of Automata (Ph.D.). University of Michigan.automata were the mathematical models of Dr. Zeigler's Ph.D. thesis
3. ↑ 3.0 3.1 3.2 3.3 Zeigler, Bernard (1984). Multifacetted Modeling and Discrete Event Simulation. London; Orlando: Academic Press. ISBN 978-0-12-778450-2.
4. ↑ Zeigler, Bernard (1987). "Hierarchical, modular discrete-event modelling in an object-oriented environment". Simulation 49 (5): 219–230. doi:10.1177/003754978704900506.
5. ↑ Zeigler, Bernard; Kim, Tag Gon; Praehofer, Herbert (2000). Theory of Modeling and Simulation (2nd ed.). New York: Academic Press. ISBN 978-0-12-778455-7.
6. ↑ We can also define the external transition function as δext:Q×X->S×{0,1} where Q=S×𝕋∞×𝕋 such that for a total state (s,ts,te)∈Q, s∈S is a partial state, ts∈𝕋∞ is the lifespan of s, and te∈(𝕋∩[0,ts]) is the elapsed time since last update of ts. For more how to understand this function, refer to the article, Behavior of DEVS.
7. ↑ Cite error: Invalid `<ref>` tag; no text was provided for refs named `Zeigler904`
8. ↑ Cellier, Francois E. (1991). Continuous System Modeling (1st ed.). Springer. ISBN 978-0-387-97502-3.
9. ↑ Cellier, Francois E.; Kofman, Ernesto (2006). Continuous System Simulation (1st ed.). Springer. ISBN 978-0-387-26102-7.
10. ↑ Nutaro, James (2010). Building Software for Simulation: Theory, Algorithms, and Applications in C++ (1st ed.). Wiley. ISBN 978-0-470-41469-9.
11. ↑ the use of quantized values in order to simulate continuous systems by means of a discrete event method was empirically tried out a few years sooner - in the early 1990s - by a French engineer. He was then working for a company spun off from University of Valenciennes, and now part of the Schneider Electric. This quantization is a feature of a simulation software of which this engineer is the conceptor and main developer, that is used for PLC programs checking and operator training.
12. ↑ Hwang, M.H.; Zeigler, B.P. (2009). "Reachability Graph of Finite and Deterministic DEVS Networks". IEEE Transactions on Automation Science and Engineering 6 (3): 454–467. doi:10.1109/TASE.2009.2024064.
13. ↑ 13.0 13.1 Hwang, M.H.. "Qualitative verification of finite and real-time DEVS networks". Proceedings of 2012 Symposium on Theory of Modeling and Simulation - DEVS Integrative M&S Symposium.
14. ↑ Hwang, M.H. (April 2–8, 2005). "Tutorial: Verification of Real-time System Based on Schedule-Preserved DEVS". Proceedings of 2005 DEVS Symposium. San Diego. ISBN 1-56555-293-8.
15. ↑ Hwang, M.H.; Zeigler, B.P.. "A Modular Verification Framework using Finite and Deterministic DEVS". Proceedings of 2006 DEVS Symposium. Huntsville, Alabama, USA. pp. 57–65.
16. ↑ Zeigler, Bernard (1976). Theory of Modeling and Simulation (first ed.). New York: Wiley Interscience.
17. ↑ Zeigler, Bernard; Kim, Tag Gon; Praehofer, Herbert (2000). Theory of Modeling and Simulation (second ed.). New York: Academic Press. ISBN 978-0-12-778455-7.
18. ↑ Hwang, Moon H. (2012). "Qualitative Verification of Finite and Real-Time DEVS Networks". Proceedings of 2012 TMS/DEVS. Orlando, FL, USA. pp. 43:1–43:8. ISBN 978-1-61839-786-7.
19. ↑ Giambiasi, N.; Escude, B.; Ghosh, S. (2001). "Generalized Discrete Event Simulation of Dynamic Systems". SCS Transactions: Recent Advances in DEVS Methodology-part II 18 (4): 216–229.
20. ↑ Zacharewicz, Gregory; Frydman, Claudia; Giambiasi, Norbert (2008). "G-DEVS/HLA Environment for Distributed Simulations of Workflows". Simulation 84 (5): 197–213. doi:10.1177/0037549708092833. https://hal.archives-ouvertes.fr/hal-00204203/file/Revue_Simulation_GZ_CF_NG_Reviewed_Final_SAGE_Biblio(1).pdf.
21. ↑ Wainer, Gabriel A. (2009). Discrete-Event Modeling and Simulation: A Practitioner's Approach (1st ed.). CRC Press. ISBN 978-1-4200-5336-4.
22. ↑ 22.0 22.1 Zeigler, Bernard; Kim, Tag Gon; Praehofer, Herbert (2000). Theory of Modeling and Simulation (second ed.). New York: Academic Press. ISBN 978-0-12-778455-7.
23. ↑ 23.0 23.1 Zeigler, Bernard (1984). Multifacetted Modeling and Discrete Event Simulation. London; Orlando: Academic Press. ISBN 978-0-12-778450-2.
24. ↑ 24.0 24.1 24.2 24.3 24.4 Hwang, M. H.; Zeigler, Bernard (2006). "A Reachable Graph of Finite and Deterministic DEVS Networks". Proceedings of 2006 DEVS Symposium. Huntsville, Alabama, USA. pp. 48–56. http://www.acims.arizona.edu/.
25. ↑ 25.0 25.1 25.2 25.3 25.4 Hwang, M. H.; Zeigler, Bernard (2009). "Reachability Graph of Finite & Deterministic DEVS". IEEE Transactions on Automation Science and Engineering 6 (3): 454–467. doi:10.1109/TASE.2009.2024064. https://ieeexplore.ieee.org/document/5071137.
26. ↑ Zeigler, Bernard; Kim, Tag Gon; Praehofer, Herbert (2000). Theory of Modeling and Simulation (second ed.). New York: Academic Press. ISBN 978-0-12-778455-7.
27. ↑ 27.0 27.1 Hwang, M. H. (August 2005). "Generating Finite-State Global Behavior of Reconfigurable Automation Systems: DEVS Approach". Proceedings of 2005 IEEE-CASE. Edmonton, Canada. http://moonho.hwang.googlepages.com/publications.
28. ↑ 28.0 28.1 Dill, D. L. (1989). "Timing Assumptions and Verification of Finite-State Concurrent Systems". Proceedings of the Workshop on Computer Aided Verification Methods for Finite State Systems. Grenoble, France. pp. 197–212.
29. ↑ Hwang, M. H. (August 2005). "Generating Finite-State Global Behavior of Reconfigurable Automation Systems: DEVS Approach". Proceedings of 2005 IEEE-CASE. Edmonton, Canada. http://moonho.hwang.googlepages.com/publications. (note: δx can be divided into two functions: ρ:S×X->{0,1} and δx:S×X->S)
30. ↑ Zeigler, Bernard; Kim, Tag Gon; Praehofer, Herbert (2000). Theory of Modeling and Simulation (second ed.). New York: Academic Press. ISBN 978-0-12-778455-7. (note: δy can be divided into two functions: λ:S->Yϕ and δint:S->S)
31. ↑ Hwang, M. H.; Zeigler, Bernard (2006). "A Modular Verification Framework using Finite and Deterministic DEVS". Proceedings of 2006 DEVS Symposium. Huntsville, Alabama, USA. pp. 57–65. http://www.acims.arizona.edu/.
32. ↑ 32.0 32.1 "DEVSsharp". https://xsy-csharp.sourceforge.net/DEVSsharp/.
33. ↑ "XSY". https://code.google.com/p/x-s-y/.
34. ↑ Mittal, Saurabh. "xFDDEVS". http://www.duniptechnologies.com/research/xfddevs/.
35. ↑ Risco-Martín, José L.; de la Cruz, Jesús M.; Mittal, Saurabh; Zeigler, Bernard (2009). "eUDEVS: Executable UML with DEVS Theory of Modeling and Simulation". SIMULATION, Transaction of the Society for Modeling and Simulation International 85 (11–12): 750–777. doi:10.1177/0037549709104727. http://sim.sagepub.com/content/85/11-12/750.short.
36. ↑ Zeigler, Bernard; Kim, Tag Gon; Praehofer, Herbert (2000). Theory of Modeling and Simulation (second ed.). New York: Academic Press. ISBN 978-0-12-778455-7. (note: δy can be divided into two functions: λ:S->Yϕ and δint:S->S)
37. ↑ 37.0 37.1 37.2 Hwang, M. H. (April 2–8, 2005). "Tutorial: Verification of Real-time System Based on Schedule-Preserved DEVS". Proceedings of 2005 DEVS Symposium. San Diego. ISBN 978-1-56555-293-7. http://moonho.hwang.googlepages.com/publications.
38. ↑ 38.0 38.1 Hwang, M. H.; Cho, S. K.; Zeigler, Bernard; Lin, F. (2007). ﻿Processing Time Bounds of Schedule-Preserving DEVS﻿ (Report). http://www.acims.arizona.edu/. Retrieved 2008-03-18.
39. ↑ Hwang, M. H. (August 1–2, 2005). "Generating Finite-State Global Behavior of Reconfigurable Automation Systems: DEVS Approach". Proceedings of 2005 IEEE-CASE. Edmonton, Canada. http://moonho.hwang.googlepages.com/publications.

0.00

(0 votes)

Original source: https://en.wikipedia.org/wiki/DEVS. Read more

|

Retrieved from "https://handwiki.org/wiki/index.php?title=DEVS&oldid=3988928"