Finite & Deterministic Discrete Event System Specification
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.
FD-DEVS was originally named as "Schedule-Controllable DEVS" [Hwang05] 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.
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 [Hwang05].
But another time abstraction method [Dill89] which was invented by Prof. D. Dill can be applicable to obtain a finite-vertex reachability graph for FD-DEVS networks.
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.
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".
Consider a toaster in which there are two slots that have their own start knobs as shown in Fig.
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".
In other words, it stays at "Idle" forever unless it receives "?push" event.
We would give a model of FD-DEVS of a crosswalk light controller which is used for SP-DEVS in this Wikipedia.
3. shows an event segment (top) and the associated state trajectory (bottom) of Player A who plays the ping-pong game introduced in Fig.
3. the status of Player A is described as (state, lifespan, elapsed time)=(
Thus, this cyclic state transitions which move "Send" to "Wait" back and forth will go forever.
4. shows an event segment (top) and the associated state trajectory (bottom) of the left slot of the two-slot toaster introduced in Fig.
Like Fig.3, the status of the left slot is described as (state, lifespan, elapsed time)=(
Since the initial state of the toaster is "I" and its lifetime is infinity, the height of (Wait, inf,
4. illustrates the case ?push happens at time 40 and the toaster changes into (T, 20, 0).
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
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 [Dill89].
An algorithm generating a finite-vertex reachability graph (RG)has been introduced in [HZ06a], [HZ07].
5. shows the reachability graph of two-slot toaster which was shown in Fig.
In the reachability graph, each vertex has its own discrete state and time zone which are ranges of
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[HZ06b].
of FD-DEVS are deterministic can be seen as somehow a limitation to model the system that has non-deterministic behaviors.
1. has a stochastic lifespan at "Send" state, FD-DEVS doesn't capture the non-determinism effectively.
There are two open source libraries DEVS# written in C# at http://xsy-csharp.sourceforge.net/DEVSsharp/ and XSY written in Python at https://code.google.com/p/x-s-y/ that support some reachability graph-based verification algorithms for finding safeness and liveness.
