An approach to unfolding asynchronous communication protocols

Abstract

We present an approach to directly unfold asynchronous communication protocols that are modeled as a group of Extended Finite State Machines (EFSMs) communicating through shared message queues. A novel aspect of our approach is that we reduce the redundancy in representing the states of message queues by storing individual messages separately in our unfolding representation. Our approach can also take advantage of the compositional nature of these protocols to minimize the size of a complete finite prefix of their potentially infinite unfoldings. Our empirical results indicate that our approach can produce very compact state space representations. © Springer-Verlag Berlin Heidelberg 2005.