• Home
•  Up to Topics
•  Previous
•  Next

Hybrid Sys.

• Time/Events
• Hybrid Systems
• Mixed Systems
• Modal Models
• Loudness
• Timed Automata
• Parking Meter
• Protocols
• Internet

Network Protocol

Consider the network protocol:

Here, a timed automaton is used to cause retransmission when an acknowledgement fails to arrive within a specified amount of time (timeoutTime). The upper diagram shows the structure of the communication system. Everything begins when the sender produces a packet event. The SenderProtocol system reacts by producing a transmit event, which instructs its network interface card or NIC to launch the packet into the internet. The NIC is the physical device (such as the ethernet card in your desktop computer) that converts the packet into the appropriate electrical signal that is transmitted through the network. The internet transfers this signal to the NIC of the receiver. That NIC converts the signal back into the packet and forwards it to the ReceiverProtocol component. The ReceiverProtocol in turn forwards the packet to the e-mail application in the Receiver and simultaneously sends an acknowledgement packet, called ack, to its NIC. The receiver’s NIC sends the ack packet back through the network to the Sender. The sender’s NIC receives this packet and forwards an ack to the SenderProtocol. The SenderProtocol notifies the application that the packet was indeed delivered. The application can now send the next packet, and the cycle is repeated until the entire file is delivered.

In reality, the network may drop the packet so that it is not delivered to the receiver, who therefore will not send the corresponding ack. The SenderProtocol system is designed to take care of this contingency. It is a timed automaton with two modes, idle and timing, and one refinement state s corresponding to a clock. When SenderProtocol receives a packet it makes a transition to the timing mode, sends the output event transmit to its NIC, and resets s to a timeout value timeoutTime. In the timing mode, there are two possibile transitions. In the normal case, the input event ack is received before the guard timeout is satisfied. The transition to mode idle is taken, the output event ack is sent to the application, and the clock value s is reset to 0. The system waits for another packet from the application. In the second case, the guard timeout is satisfied (before event ack), and the self-loop transition is taken. In this case, the output event retransmit is sent to the NIC, and s is reset to timeoutTime. This SenderProtocol, therefore, will keep sending a packet until it receives ack.