Stateless techniques for generating global and local test oracles for message-passing concurrent programs

A test oracle for a concurrent program is a method for checking whether an observed behavior of the program is consistent with the program's specification. specification models for message-passing concurrent programs are often expressed as, or can be translated into, a labeled transition system (LTS). Stateful techniques for generating test oracles from LTS specification models are often limited by the state explosion problem. In this paper, we present a stateless technique for generating global and local test oracles from LTS specification models. A global test oracle uses tests generated from a global LTS model of the complete system to verify a global implementation relation between the model of the system and its implementation. Global test oracles, however, may require too many test sequences to be executed by the implementation. A local test oracle verifies local implementation relations between individual component models and their implementation threads. Local tests are executed against individual threads, without testing the system as a whole. Verifying the local implementation relations implies that a corresponding global implementation relation holds between the complete system model and its implementation. Empirical results indicate that using local test oracles can significantly reduce the number of executed test sequences.