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 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 advanced 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 a state of the system. 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 Crosswalk Controller The above controller shown in Fig. 2 can be written as where ={?p}; ={!g:0, !g:1, !w:0, !w:1}; ={BG, BW, G, GR, R, W, D}; =BG, (BG)=0.5,(BW)=0.5, (G)=30, (GR)=30,(R)=2, (W)=26, (D)=2; (G,?p)=GR, (s,?p)=s if s G; (BG)=(!g:1, BW), (BW)=(!w:0, G),(G)=(, G), (GR)=(!g:0, R), (R)=(!w:1, W), (W)=(!w:0, D), (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 be the lifespan which is not continuously increasing but set by when a discrete event happens. Let 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