Lossy Communicating Finite State Machines

A network of communicating finite state machines (CFSM) consists of a set of finite state machines that communicate asynchronously with each other over (potentially) unbounded FIFO channels by sending and receiving typed messages. As a concurrency model, CFSMs has been widely used to specify and validate communications protocols. 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.