Jumpstart just-in-time signaling protocol: A formal description using extended finite state machines

We present a formal protocol description for a just-in-time (JIT) signaling scheme running over a core dense wavelength division multiplexing (DWDM) network that utilizes optical burst switches (OBSs). We apply an eight-tuple extended finite state machine (EFSM) model to formally specify the protocol. Using the EFSM model, we define the communication between a source client node and a destination client node through an ingress and one or multiple intermediate switches. We work on on-the-fly and persistent unicast connections. The communication between the EFSMs is handled through messages.