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.

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, while Zeigler was an associate professor at University of Michigan. DEVS can be seen as an extension of the Moore machine formalism,automata were the mathematical models of Dr. Zeigler's Ph.D. thesis 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

# associating a lifespan with each state,
# providing a hierarchical concept with an operation, called ''coupling'',

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 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

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'' output event ''!send'' is transmitted to Player ''B'' 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. In this article, we will use the time base, \mathbb= ,\infty) that is the set of non-negative real numbers; the extended time base,$\mathbb^\infty=[0,\infty/math> that is the set of non-negative real numbers plus infinity.$

Atomic DEVS

An atomic DEVS model is defined as a 7-tuple 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'');
* $s_0\in S$ is ''the initial state'';
* $ta:S \rightarrow \mathbb^\infty$ is ''the time advance function'' which is used to determine the lifespan of a state;
* $\delta_:Q \times X \rightarrow S$ is ''the external transition function'' which defines how an input event changes a state of the system, where $Q=\$ is the ''set of total states'', and $t_e$ is the ''elapsed time'' since ''the last event'';We can also define the external transition function as $\delta_:Q \times X \rightarrow S \times \$ where $Q = S \times \mathbb^\infty \times \mathbb$ such that for a total state $(s, t_s, t_e) \in Q$, $s \in S$ is a partial state, $t_s \in \mathbb^\infty$ is the lifespan of $s$, and t_e \in (\mathbb \cap ,t_s is the elapsed time since ''last update'' of $t_s$. For more how to understand this function, refer to the article, Behavior of DEVS.
* $\delta_:S \rightarrow 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);
* $\lambda:S \rightarrow Y^\phi$ is ''the output function'' where $Y^\phi=Y \cup \$ and $\phi \not\in 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= such that

$\begin X &= \\\ Y &= \\\ S &= \\\ s_0 &= (\textit, 0.1)\\ ta(s) &=\sigma \text s \in S\\ \delta_(((\textit,\sigma),t_e),?\textit)&=(\textit,0.1)\\ \delta_(\textit,\sigma)&=(\textit,\infty)\\ \delta_(\textit,\sigma)&=(\textit,0.1)\\ \lambda(\textit,\sigma)&=!\textit\\ \lambda(\textit,\sigma)&=\phi \end$

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 \in S$: (1) when an external input $x \in X$ comes into the system $M$; (2) when the elapsed time $t_e$ reaches the lifespan of $s$ which is defined by $ta(s)$. At the same time of (2), $M$ generates an output $y \in Y$ which is defined by $\lambda(s)$.

For formal behavior description of given an Atomic DEVS model, refer to the section Behavior of atomic DEVS. Computer algorithms to implement the behavior of a given Atomic DEVS model are available in the section 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-tuplewhere

* $X$ is ''the set of input events'';
* $Y$ is ''the set of output events'';
* $D$ is ''the name set of sub-components'';
* $\$ is ''the set of sub-components'' where for each $i \in D, M_i$ can be either an atomic DEVS model or a coupled DEVS model.
* $C_\subseteq X \times \bigcup_ X_i$ is ''the set of external input couplings'';
* $C_\subseteq \bigcup_ Y_i \times \bigcup_ X_i$ is ''the set of internal couplings'';
* $C_: \bigcup_ Y_i \rightarrow Y^\phi$ is ''the external output coupling function'';
* $Select:2^D \rightarrow 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= where $X=\$;$Y=\$;$D=\$; $M_A \text M_B$ is described as above; $C_=\$; $C_=\$; and $C_(A.!send)=\phi, C_(B.!send)=\phi$.

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 \in X$ comes into $N$; (2) when one of components $M_i$ where $i \in D$ executes its internal state transition and generates its output $y_i \in Y_i$. In both cases (1) and (2), a triggering event is transmitted to all influences which are defined by coupling sets $C_, C_,$ and $C_$.

For formal definition of behavior of the coupled DEVS, you can refer to the section Behavior of Coupled DEVS. Computer algorithms to implement the behavior of a given coupled DEVS mode are available at the section 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. 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'', and Prof. Kofman wrote a text book, ''Continuous System Simulation'', in which Chapters 11 and 12 cover how DEVS simulates continuous state systems. Dr. Nutaro's book, covers the discrete event simulation of continuous state systems too.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.

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), and Finite & Real-time DEVS (FRT-DEVS). As a result, based on the reachability graph, (1) dead-lock and live-lock freeness as qualitative properties are decidable with SP-DEVS, FD-DEVS, and FRT-DEVS; and (2) min/max processing time bounds as a quantitative property are decidable with SP-DEVS so far by 2012.

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, Parallel DEVS, Dynamic Structuring DEVS, Cell-DEVS, 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) $\subset$ ''E''( FD-DEVS)$\subset$ ''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. 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, \mathcal= has

# the external state transition $\delta_:Q \times X \rightarrow S$.
# the total state set $Q=\$ where $t_e$ denotes elapsed time since last event and \mathbb= Timed Event System \mathcal= where

* The event set $Z=X \cup Y^\phi$.
* The state set $Q=Q_A \cup Q_N$ where $Q_N=\$.
* The set of initial states $\,Q_0 = \$.
* The set of accepting states $Q_A = \mathcal.Q.$
* The set of state trajectories $\Delta \subseteq Q \times \Omega_ \times Q$ is defined for two different cases: $q \in Q_N$ and $q \in Q_A$. For a non-accepting state $q \in Q_N$, there is no change together with any even segment $\omega \in \Omega_$ so $(q,\omega,q) \in \Delta.$

For a total state $q=(s,t_e) \in Q_A$ at time $t \in \mathbb$ and an event segment $\omega \in \Omega_$ as follows.

If unit event segment $\omega$ is the null event segment, i.e. $\omega=\epsilon_$

$\, (q, \omega, (s, t_e+dt)) \in \Delta.$

If unit event segment $\omega$ is a timed event $\omega=(x, t)$ where the event is an input event $x \in X$,

$(q, \omega, (\delta_(q,x), 0)) \in \Delta.$

If unit event segment $\omega$ is a timed event $\omega=(y, t)$ where the event is an output event or the unobservable event $y \in Y^\phi$,

$\begin (q, \omega,(\delta_(s), 0)) \in \Delta& \textrm ~ t_e = ta(s), y = \lambda(s)\\ (q, \omega, \bar) & \textrm. \end$

Computer algorithms to simulate this view of behavior are available at Simulation Algorithms for Atomic DEVS.

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

Suppose that a DEVS model, \mathcal= has

# the total state set $Q=\$ where $t_s$ denotes lifespan of state $s$, $t_e$ denotes elapsed time since last $t_s$update, and $\mathbb^\infty=[0,\infty) \cup \$ denotes the set of non-negative real numbers plus infinity,
# the external state transition is $\delta_:Q \times X \rightarrow S \times \$.

Then the DEVS $Q=\mathcal$ is a timed event system \mathcal= where

* The event set $Z=X \cup Y^\phi$.
* The state set $Q=Q_A \cup Q_N$ where $Q_N=\$.
* The set of initial states$\,Q_0 = \$.
* The set of acceptance states $Q_A = \mathcal.Q$.
* The set of state trajectories $\Delta \subseteq Q \times \Omega_ \times Q$ is depending on two cases: $q \in Q_N$ and $q \in Q_A$. For a non-accepting state $q \in Q_N$, there is no changes together with any segment $\omega \in \Omega_$ so $(q,\omega,q) \in \Delta.$

For a total state $q=(s,t_s, t_e) \in Q_A$ at time $t \in \mathbb$ and an event segment $\omega \in \Omega_$ as follows.

If unit event segment $\omega$ is the null event segment, i.e. $\omega=\epsilon_$

$(q, \omega, (s, t_s, t_e+dt)) \in \Delta.$

If unit event segment $\omega$ is a timed event $\omega=(x, t)$ where the event is an input event $x \in X$,

$\begin (q, \omega, (s', ta(s'), 0))\in \Delta& \textrm ~\delta_(s,t_s,t_e,x)=(s',1),\\ (q, \omega, (s', t_s, t_e))\in \Delta& \textrm ~\delta_(s,t_s,t_e,x)=(s',0). \end$

If unit event segment $\omega$ is a Event Segment#Timed event">timed event $\omega=(y, t)$ where the event is an output event or the unobservable event $y \in Y^\phi$,

$\begin (q, \omega, (s', ta(s'),0)) \in \Delta& \textrm ~t_e = t_s, y = \lambda(s), \delta_(s)=s',\\ (q, \omega, \bar )\in \Delta& \textrm. \end$

Computer algorithms to simulate this view of behavior are available at Simulation Algorithms for Atomic DEVS.

Comparison of View1 and View2

= Features of View1

=
View1 has been introduced by Zeigler in which given a total state $q=(s,t_e) \in Q$ and

$\, ta(s)=\sigma$

where $\sigma$ is the remaining time. In other words, the set of partial states is indeed $S=\$ where $S'$ is a state set.

When a DEVS model receives an input event $x \in X$, View1 resets the elapsed time $t_e$ by zero, if the DEVS model needs to ignore $x$ in terms of the lifespan control, modelers have to update the remaining time

$\, \sigma = \sigma - t_e$

in the external state transition function $\delta_$ that is the responsibility of the modelers.

Since the number of possible values of $\sigma$ 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, \sigma) \in 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 $t_e=0$ every time any input event arrives into the DEVS model. But disadvantage might be modelers of DEVS should know how to manage $\sigma$ as above, which is not explicitly explained in $\delta_$ itself but in $\Delta$.

= Features of View2

=
View2 has been introduced by Hwang and Zeigler in which given a total state $q=(s, t_s, t_e) \in Q$, the remaining time, $\sigma$ is computed as

$\, \sigma = t_s - t_e.$

When a DEVS model receives an input event $x \in X$, View2 resets the elapsed time $t_e$ by zero only if $\delta_(q,x)=(s',1)$. If the DEVS model needs to ignore $x$ in terms of the lifespan control, modelers can use $\delta_(q,x)=(s',0)$.

Unlike View1, since the remaining time $\sigma$ 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. 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.

Coupled DEVS

''DEVS is closed under coupling.'' 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 = , its behavior is described as an atomic DEVS model M =

where

* $X$ and $Y$ are the input event set and the output event set, respectively.
* $S=\underset\times Q_i$ is the partial state set where $Q_i=\$ is the total state set of component $i \in D$ (Refer to View1 of Behavior of DEVS), where $\mathbb=[0,\infty)$ is the set of non-negative real numbers.
* $s_0=\underset\times q_$ is the initial state set where $q_=(s_,0)$ is the total initial state of component $i \in D$.
* $ta:S \rightarrow \mathbb^\infty$ is the time advance function, where \mathbb^\infty= ,\infty/math> is the set of non-negative real numbers plus infinity. Given $s=(\ldots, (s_,t_),\ldots)$,

$ta(s)= \min\.$

* $\delta_:Q \times X \rightarrow S$ is the external state function. Given a total state $q=(s,t_e)$ where s=(\ldots, (s_, t_),\ldots), t_e \in (\mathbb\cap ,ta(s)), and input event $x \in X$, the next state is given by

$\delta_(q, x)=s'=(\ldots,(s_i', t_'), \ldots)$

where

$(s_i', t_')= \begin (\delta_(s_i, t_, x_i),0) & \text (x, x_i) \in C_\\ (s_i, t_) & \text. \end$

Given the partial state $s=(\ldots,(s_i, t_),\ldots) \in S$, let $IMM(s)=\$ denote ''the set of imminent components''. The ''firing component'' $i^* \in D$ which triggers the internal state transition and an output event is determined by

$i^* = Select(IMM(s)).$

* $\delta_:S \rightarrow S$ is the internal state function. Given a partial state $s=(\ldots, (s_, t_),\ldots)$, the next state is given by

$\delta_(s)=s'=(\ldots,(s_i', t_'), \ldots)$

where

$(s_i', t_')= \begin (\delta_(s_i),0) & \text i = i^*\\ (\delta_(s_i, t_, x_i),0) & \text (\lambda_(s_), x_i) \in C_\\ (s_i, t_) & \text. \end$

* $\lambda:S \rightarrow Y^\phi$ is the output function. Given a partial state $s=(\ldots, (s_, t_),\ldots)$,

$\lambda(s)= \begin \phi &\text \lambda_(s_)=\phi \\ C_(\lambda_(s_)) &\text. \end$

View2: Total states = states * lifespan * elapsed times

Given a coupled DEVS model N = , its behavior is described as an atomic DEVS model M =

where

* $X$ and $Y$ are the input event set and the output event set, respectively.
* $S=\underset\times Q_i$ is the partial state set where $Q_i=\$ is the total state set of component $i \in D$ (Refer to View2 of Behavior of DEVS).
* $s_0=\underset\times q_$ is the initial state set where $q_=(s_,ta_i(s_),0)$ is the total initial state of component $i \in D$.
* $ta:S \rightarrow \mathbb^\infty$ is the time advance function. Given $s=(\ldots, (s_,t_,t_),\ldots)$,

$ta(s)= \min\.$

* $\delta_:Q \times X \rightarrow S \times \$ is the external state function. Given a total state $q=(s,t_s,t_e)$ where s=(\ldots, (s_, t_,t_),\ldots), t_s \in \mathbb^\infty, t_e \in (\mathbb\cap ,t_s), and input event $x \in X$, the next state is given by

$\delta_(q, x)=((\ldots,(s_i', t_', t_'), \ldots),b)$

where

$(s_i', t_', t_')= \begin (s_i', ta_i(s_i'), 0) & \text (x, x_i) \in C_,\delta_(s_i, t_, t_, x_i)=(s_i',1)\\ (s_i', t_, t_ ) & \text (x, x_i) \in C_,\delta_(s_i, t_, t_, x_i)=(s_i',0)\\ (s_i, t_, t_) & \text \end$

and

$b= \begin 1 & \text \exists i \in D: (x, x_i) \in C_,\delta_(s_i, t_, t_, x_i)=(s_i',1)\\ 0 & \text. \end$

Given the partial state $s=(\ldots,(s_i, t_, t_),\ldots) \in S$, let $IMM(s)=\$ denote ''the set of imminent components''. The ''firing component'' $i^* \in D$ which triggers the internal state transition and an output event is determined by

$i^* = Select(IMM(s)).$

* $\delta_:S \rightarrow S$ is the internal state function. Given a partial state $s=(\ldots, (s_,t_, t_),\ldots)$, the next state is given by

$\delta_(s)=s'=(\ldots,(s_i', t_', t_'), \ldots)$

where

$(s_i', t_', t_')= \begin (s_i', ta_i(s_i'),0) & \text i = i^*,\delta_(s_i)=s_i',\\ (s_i', ta_i(s_i'),0) & \text (\lambda_(s_), x_i) \in C_,\delta_(s_i, t_, t_, x_i)=(s', 1)\\ (s_i', t_, t_) & \text (\lambda_(s_), x_i) \in C_,\delta_(s_i, t_, t_, x_i)=(s', 0)\\ (s_i, t_, t_) & \text. \end$

* $\lambda:S \rightarrow Y^\phi$ is the output function. Given a partial state $s=(\ldots, (s_, t_, t_),\ldots)$,

$\lambda(s)= \begin \phi &\text \lambda_(s_)=\phi \\ C_(\lambda_(s_)) &\text. \end$

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,t_e) \in Q$ where $s = (\ldots,(s_i, t_),\ldots)$

If unit event segment $\omega$ is the null event segment, i.e. $\omega=\epsilon_$, the state trajectory in terms of Timed Event System is

$\Delta(q, \omega)=((\ldots,(s_i, t_+dt),\ldots), t_e+dt).$

= For View2

=
Given a total state $q=(s,t_s,t_e) \in Q$ where $s = (\ldots,(s_i, t_, t_),\ldots)$

If unit event segment $\omega$ is the null event segment, i.e. $\omega=\epsilon_$, the state trajectory in terms of Timed Event System is

$\Delta(q, \omega)=((\ldots,(s_i,t_, t_+dt),\ldots), t_, t_e+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'' t_s \in ,\infty/math> and ''elapsed time'' t_e\in ,\infty/math> with the following relations:

$\, t_e = t - t_l$

and

$\, t_s = t_n - t_l$

where $t\in [0,\infty)$ denotes the ''current time''. And the ''remaining time'',

$\,t_r=t_s-t_e$

is equivalently computed as

$\, t_r = t_n - t$

, apparently t_r \in ,\infty/math>.

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), 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
$t_l$ // time of last event
$t_n$ // time of next event
$A=(X,Y,S,ta, \delta_, \delta_, \lambda)$// the associated DEVS#Atomic DEVS">Atomic DEVS model
when receive init-message(Time $t$)
$t_l \leftarrow t;$
$t_n \leftarrow t_l + ta(s);$
when receive star-message(Time $t$)
if $t \ne t_n$ then
error: bad synchronization;
$y \leftarrow \lambda(s);$
send y-message($y,t$) to parent;
$s \leftarrow \delta_(s)$
$t_l \leftarrow t;$
$t_n \leftarrow t_l + ta(s);$

View 1: total states = states * elapsed times

As addressed in Behavior of Atomic DEVS, when DEVS receives an input event, right calling $\delta_$, the last event time,$t_l$ is set by the current time,$t$, thus the elapsed time$t_e$ becomes zero because $t_e = t - t_l$.
when receive x-message($x \in X$, Time $t$)
if $( t_l \le t$ and $t \le t_n )$

false then
error: bad synchronization;
$s \leftarrow \delta_(s,t-t_l, x)$
$t_l \leftarrow t;$
$t_n \leftarrow t_l + ta(s);$

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

Notice that as addressed in Behavior of Atomic DEVS, depending on the value of $b$ return by $\delta_$, last event time,$t_l$, and next event time,$t_n$,consequently, elapsed time, $t_e$, and lifespan$t_n$, are updated (if $b=1$) or preserved (if $b=0$).
when receive x-message($x \in X$, Time $t$)
if $( t_l \le t$ and $t \le t_n )$

false then
error: bad synchronization;
$(s,b) \leftarrow \delta_(s, t-t_l, x)$
if $b = 1$ then
$t_l \leftarrow t;$
$t_n \leftarrow t_l + 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'' t_s \in ,\infty/math> and ''elapsed time'' t_e\in ,\infty/math> with the following relations:

$\, t_e = t - t_l$

and

$\, t_s = t_n - t_l$

where $t\in [0,\infty)$ denotes the ''current time''. And the ''remaining time'',

$\,t_r=t_s-t_e$

is equivalently computed as

$\, t_r = t_n - t,$

apparently t_r \in ,\infty/math>. 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
$t_l$: // time of last event
$t_n$: // time of next event
$N=(X, Y, D, \, C_, C_, C_,Select)$ // the associated DEVS#Coupled DEVS">Coupled DEVS model
when receive init-message(Time ''t'')
for each $i \in D$ do
send init-message(''t'') to child $i$
$t_l \leftarrow \max\$;
$t_n \leftarrow \min\$;
when receive star-message(Time ''t'')
if $t \ne t_n$ then
error: bad synchronization;
$i^* \leftarrow Select(\);$
send star-message(''t'')to $i^*$
$t_l \leftarrow \max\$;
$t_n \leftarrow \min\$;
when receive x-message($x \in X$, Time ''t'')
if $( t_l \le t$ and $t \le t_n )$

false then
error: bad synchronization;
for each $(x,x_i) \in C_$ do
send x-message($x_i$,''t'') to child $i$
$t_l \leftarrow \max\$;
$t_n \leftarrow \min\$;
when receive y-message($y_i \in Y_i$, Time ''t'')
for each $(y_i,x_i) \in C_$ do
send x-message($x_i$,''t'') to child $i$
if $C_(y_i)\ne \phi$ then
send y-message($C_(y_i)$, ''t'') to parent;
$t_l \leftarrow \max\$;
$t_n \leftarrow \min\$;

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" 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

# finiteness of event sets and state set,
# the lifespan of a state can be scheduled by a rational number or infinity, and
# 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. But another time abstraction method 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

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

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 =

where

* $X$ is ''a finite set of input events'';
* $Y$ is ''a finite set of output events'';
* $S$ is ''a finite set of states'';
* $s_0 \in S$ is ''the initial state'';
* $\tau: S \rightarrow \mathbb_$ is ''the time advance function'' which defines the lifespan of a state where $\mathbb_$ is the set of non-negative rational numbers plus infinity.
* $\delta_x: S \times X \rightarrow S \times \$ 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 \in S$ is updated by $\tau(s')$ if $\delta_x(s)=(s',1)$, otherwise(i.e., $\delta_x(s)=(s',0)$), the schedule is preserved. (note: $\delta_x$ can be divided into two functions: $\rho: S \times X \rightarrow \$ and $\delta_:S \times X \rightarrow S$)
* $\delta_y: S \rightarrow Y^\phi \times S$ is ''the output and internal transition function'' where $Y^\phi = Y \cup \$ and $\phi \notin 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. (note: $\delta_y$ can be divided into two functions: $\lambda: S \rightarrow Y^\phi$ and $\delta_:S \rightarrow S$)

; 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= where $X$=; $Y$=; $S$=; $s_0$=Send for Player A, Wait for Player B; $\tau$(Send)=0.1,$\tau$(Wait)=$\infty$; $\delta_x$(Wait,?receive)=(Send,1), $\delta_x$(Send,?receive)=(Send,0); $\delta_y$(Send)=(!send, Wait), $\delta_y$(Wait)=($\phi$, 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= where $X$=; $Y$=; $S$=; $s_0$=I; $\tau$(T)=20 for the left slot, 40 for the right slot, $\tau$(I)=$\infty$; $\delta_x$(I, ?push)=(T,1), $\delta_x$(T,?push)=(T,0); $\delta_y$(T)=(!pop, I), $\delta_y$(I)=($\phi$, 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= where $X$=; $Y$=; $S$=; $s_0$=BG, $\tau$(BG)=0.5,$\tau$(BW)=0.5, $\tau$(G)=30, $\tau$(GR)=30,$\tau$(R)=2, $\tau$(W)=26, $\tau$(D)=2; $\delta_x$(G,?p)=(GR,0), $\delta_x$(s,?p)=(s,0) if s $\neq$G; $\delta_y$(BG)=(!g:1, BW), $\delta_y$(BW)=(!w:0, G),$\delta_y$(G)=($\phi$, G), $\delta_y$(GR)=(!g:0, R), $\delta_y$(R)=(!w:1, W), $\delta_y$(W)=(!w:0, D), $\delta_y$(D)=(!g:1, G);

Behaviors of FD-DEVS Models

; FD-DEVS is a sub-class of DEVS

A FD-DEVS model, M= is DEVS \mathcal= where

* $X,Y$ of $\mathcal$ are the same as those of $M$.
* $S'=\$
* $s_0'=(s_0,\tau(s_0))$
* Given a state $(s,t_s) \in S'$, $ta(s,t_s) = t_s.$
* Given a state $(s,t_s) \in S'$ and an input event $x \in X$,

$\delta_(s, t_s, t_e, x) = \begin (s',t_s - t_e) & \text \delta_x(s,x)=(s',0) \\ (s',\tau(s')) & \text \delta_x(s,x)=(s',1) \\ \end$

* Given a state $(s,t_s) \in S'$, $\delta_(s,t_s)=(s',\tau(s'))$ if $\delta_(s)=(y,s').$
* Given a state $(s,t_s) \in S'$, $\lambda(s,t_s)=y$ if $\delta_(s)=(y,s').$

For details of DEVS behavior, the readers can refer to Behavior of Atomic DEVS

; 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, t_s, t_e$) 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, $t_e$) is 0.1 which is the value of $t_s$. After changing into (Wait, inf, 0) when $t_e$ is reset by 0, Player A doesn't know when $t_e$ 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.

; 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, t_s, t_e$) in Fig. 4. Since the initial state of the toaster is "I" and its lifetime is infinity, the height of (Wait, inf, $t_e$) 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 $\delta_x$(T,?push)=(T,1).

Advantages

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. An algorithm generating a finite-vertex reachability graph (RG) has been introduced by Zeigler.

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 $t_, t_$ and $t_ - t_$. For example, for node (6) of Fig. 5, discrete state information is ((E,$\infty$),(T,40)), and time zone is $0 \le t_ \le 40, 0 \le t_ \le 40, -20 \le t_-t_ \le 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 of the arc denotes that elapsed time of 1 (that is $t_$ is reset by 0 when transition (6) to (5) occurs.

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.

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.

Disadvantages

Weak Expressiveness for describing nondeterminism

The features that all characteristic functions,$\tau, \delta_x, \delta_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# and XSY written in Python 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. This standard XML format was used for UML execution.

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:

# finiteness of event sets and state set,
# the lifespan of a state can be scheduled by a rational number or infinity, and
# 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 Requirements

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=

where

* $X$ is ''a finite set of input events'';
* $Y$ is ''a finite set of output events'';
* $S$ is ''a finite set of states'';
* $s_0 \in S$ is ''the initial state'';
* $\tau: S \rightarrow \mathbb_$ is ''the time advanced function'' which defines the lifespan of a state where $\mathbb_$ is the set of non-negative rational numbers plus infinity.
* $\delta_x: S \times X \rightarrow S$ is ''the external transition function'' which defines how an input event changes a state of the system.
* $\delta_y: S \rightarrow Y^\phi \times S$ is ''the output and internal transition function'' where $Y^\phi = Y \cup \$ and $\phi \notin 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. (note: $\delta_y$ can be divided into two functions: $\lambda: S \rightarrow Y^\phi$ and $\delta_:S \rightarrow S$)

; Formal Representation of Crosswalk Controller

The above controller shown in Fig. 2 can be written as M= where $X$=; $Y$=; $S$=; $s_0$=BG, $\tau$(BG)=0.5,$\tau$(BW)=0.5, $\tau$(G)=30, $\tau$(GR)=30,$\tau$(R)=2, $\tau$(W)=26, $\tau$(D)=2; $\delta_x$(G,?p)=GR, $\delta_x$(s,?p)=s if s $\neq$G; $\delta_y$(BG)=(!g:1, BW), $\delta_y$(BW)=(!w:0, G),$\delta_y$(G)=($\phi$, G), $\delta_y$(GR)=(!g:0, R), $\delta_y$(R)=(!w:1, W), $\delta_y$(W)=(!w:0, D), $\delta_y$(D)=(!g:1, G);

Behaviors of a 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 $t_s \in \mathbb_$ be the lifespan which is not continuously increasing but set by when a discrete event happens. Let t_e \in , \infty 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 \in S$ is associated with its lifespan and its elapsed time in the form of $(s, t_s, t_e)$. 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 $t_e$ can grow up to $t_e$ 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= is DEVS \mathcal= where

* $X,Y$ of $\mathcal$ are the same as those of $M$.
* $S'=\$
* $s_0'=(s_0,\tau(s_0))$
* Given a state $(s,t_s) \in S'$, $ta(s,t_s) = t_s.$
* Given a state $(s,t_s) \in S'$ and an input event $x \in X, \delta_(s, t_s, t_e, x) = (s',t_s - t_e) \text \delta_x(s,x)=s'.$
* Given a state $(s,t_s) \in S'$, $\delta_(s,t_s)=(s',\tau(s')$ if $\delta_(s)=(y,s').$
* Given a state $(s,t_s) \in S'$, $\lambda(s,t_s)=y$ if $\delta_(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. 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.

* 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.

* 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.

Disadvantages

* Less Expressiveness: OPNA problem

Let a total state $(s,t_s,t_e)$ of a SP-DEVS model be ''passive'' if $t_s = \infty$; 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, 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.

Tool

There is an open source library, called DEVS# 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

*

{{DEFAULTSORT:Devs
Automata (computation)
Formal specification languages