On the Verification of Asynchronously Communicating Systems

Abstract

Recent software is mostly constructed by reusing and composing existing components abstracted as finite state machines. Asynchronous communication is a classic interaction mechanism used for such software systems. However, analyzing communicating systems interacting asynchronously via FIFO buffers is an undecidable problem. A typical approach is to check whether the system is bounded, and if not, the corresponding state space can be made finite by limiting the presence of communication cycles in behavioral models or by fixing buffer sizes. In this talk, we focus on infinite systems and we do not restrict the system by imposing any arbitrary bounds. We first present the synchronizability property and then introduce a notion of stability for non-synchronizable systems. We prove that once the system is stable for a specific buffer bound, it remains stable whatever larger bounds are chosen for buffers. Synchronizability and stability allow us to check certain properties on the system for specific bounds and to ensure that the system will preserve these properties whatever larger bounds are used for buffers. We will also overview several properties of interest that communicating systems must satisfy when obtained via projection from choreography specifications.