2026-06-01T10:16:51Zhttps://riuma.uma.es/rest/oai/request

oai:riuma.uma.es:10630/74432026-02-03T12:09:39Zcom_10630_2254col_10630_37959

00925njm 22002777a 4500 dc Salaün, Gwen author 2014-04-29 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. http://hdl.handle.net/10630/7443 Ingeniería del software On the Verification of Asynchronously Communicating Systems