SP-DEVS
SP-DEVS abbreviating "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.
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: 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.
We want to control two lights of G and W with a set of timing constraints.
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.
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.
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.
(D)=(!g:1, G); To captured the dynamics of an atomic SP-DEVS, we need to introduce two variables associated to time.
be the lifespan which is not continuously increasing but set by when a discrete event happens.
shows a state trajectory associated with an event segment of the SP-DEVS model shown in Fig.
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.
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
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.
where 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 [Hwang05],[HCZF07] 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.
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 [Hwang05].
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[Hwang05].
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 [HCZF07].
This phenomenon was found first at [Hwang 05b] 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.
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 toating time is 20 seconds or 40 seconds.
There is an open source library, called DEVS# at http://xsy-csharp.sourceforge.net/DEVSsharp/, that supports some algorithms for finding safeness and liveness as well as Min/Max processing time bounds.
