A Synchronization Flow Analysis of Concurrent Objects in AIBO OPEN-R Programs Based on Communicating Processes

We propose a compositional analysis method for synchronization flow in AIBO OPEN-R programs based on communicating processes. Concurrent objects of AIBO programs with the OPEN-RAPI are synchronized by two types of signals: ready and notify. Focusing on these signals, we describe abstract behavior of AIBO programs in the pi-calculus preserving the source code structure. We model-check deadlock freeness and interactions order of AIBO programs based on this abstract behavior. Since a primary issue in model-checking is the state space explosion in the behavioral model, we present a decomposing method to reduce the combination of states of concurrent objects. Since our translation to the pi-calculus preserves the syntactical structure of source code, when a counter-example is pointed out, our method enables not only to detect the violation of property of the whole system, but also to point out which component may cause the violation. We developed a prototype translator from AIBO OPEN-R programs to abstract description in the pi-calculus. We show that an application of our decomposing method enables to practically model- check properties by existing tools in two examples of AIBO programs.