Testing Multi-Threaded Programs by Transformation to Hoare’s CSP

The problem of testing multi-threaded programs by viewing the program as Hoare’s CSP specification or Communicating State Machines is addressed. We describe an approach to transform Java threads into equivalent Hoare’s CSP specification and discuss its implementation. The CSP based abstract view of the Java program aids developers create more effective tests addressing coverage of not only the underlying individual state models but also the interactions among concurrent or communicating state machines. Code coverage criteria of a multi-threaded program are defined in terms of intra-thread and inter-thread state transitions where the latter reflect implicit transitions from the notification node of one thread to the wait node of another interacting thread. The coverage criterion for a multi-threaded program for inter-thread communication is based on covering transition from each notify node to corresponding wait node. State transition coverage is used in general, however, coverage is more rigorous, when it comes to thread interactions and synchronized blocks, by approximating path coverage. Functional tests are designed for testing a case study namely producer and consumer problem and a corresponding table of edge or branch (or state transition or process transition) coverage is shown highlighting coverage achieved.