Sizing and verification of communication buffers for communicating processes

A method is presented for minimal sizing and verification of communication buffers in an environment of communicating concurrent processes. Methods described in the literature based on lifetime analysis techniques are mainly suited for sizing buffers in a network of processes with non-conditional interactions. We consider a more general problem where the execution of each process inherently depends on complex interactions with other processes as well as its internal conditional behavior and propose the use of implicit state enumeration techniques to solve buffer sizing and verification for this case. A model of the network of processes and buffers is introduced that is transformed into a network of finite state machines by modeling communicating buffers as counters. The transformed network forms a finite state space model on which implicit state space exploration algorithms are applied. The model allows us to handle the buffer sizing and verification problems with processes that operate on different, but related clocks. To reduce the complexity of the state space, abstraction techniques can be used to produce simplified versions of finite state machines that hide away unnecessarily detailed information. The feasibility of the proposed approach is demonstrated by a practical example.