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" [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. 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 [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.
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
where
is a finite set of input events; is a finite set of output events; is a finite set of states; is the initial state; is the time advance function which defines the lifespan of a state where is the set of non-negative rational numbers plus infinity. 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 is updated by if , otherwise(i.e., ), the schedule is preserved. is the output and internal transition function where and 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.
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. where ={ ?receive}; ={ !send}; ={ Send, Wait}; =Send for Player A, Wait for Player B; (Send)=0.1,(Wait)=; (Wait,?receive)=(Send,1), (Send,?receive)=(Send,0); (Send)=(!send, Wait), (Wait)=(, Wait).