Checking Asynchronously Communicating Components Using Symbolic Transition Systems

Abstract. Explicit behavioural interface description languages (BIDLs, protocols) are now recognized as a mandatory feature of component languages in order to address component reuse, coordination, adaptation and verification issues. Such protocol languages often deal with synchronous communication. However, in the context of distributed systems, components communicating asynchronously through mailboxes are much more relevant. In this paper, we advocate for the use of Symbolic Transition Systems as a protocol language which may deal also with this kind of communication. We then present how this generic formalism, specialized with different mailbox protocols, may be used to address verification issues related to the component mailboxes.

• Type: Conference
• Year: 2004
• Where: COOPIS
• Authors: Olivier Maréchal, Pascal Poizat, Jean-Claude Royer
• Keywords: COOPIS 2004, Explicit Behavioural Interface, Information Management, Protocol Language, Verification Issues