Lossy communicating finite state machines

In this paper we propose to extend the classical CFSM model by introducing a new type of actions - the deletion action. The resulted model is called lossy communicating finite state machines (LCFSMs). The LCFSM model remedies two weaknesses in classical CFSM model. We show that the LCFSM model allows specification and verification of unreliable communication channels with no need of extra CFSMs. The LCFSM model enables more succinct specification and verification of communication protocols that use unreliable communication channels. LCFSM paradigm can also be used to concisely model communication errors such as dropping datagrams in UDP due to lack of local buffers.