The INI has a new website!

This is a legacy webpage. Please visit the new site to ensure you are seeing up to date information.

An Isaac Newton Institute Programme

Logic and Algorithms

A fresh look at testing for asynchronous communication

28th June 2006

Author: Paul Gastin (ENS, Cachan)

Abstract

Testing is one of the fundamental techniques for verifying if a computing system conforms to its specification. Developing an efficient and exhaustive test suite is a challenging problem, especially in the setting of distributed systems. We take a fresh look at the theory of testing for message-passing systems based on a natural notion of observability in terms of input-output relations. We propose two notions of test equivalence: one which corresponds to presenting all test inputs up front and the other which corresponds to interactively feeding inputs to the system under test. We compare our notions with those studied earlier, notably the equivalence proposed by Tretmans. In Tretmans' framework, asynchrony is modelled using synchronous communication by augmenting the state space of the system with queues. We show that the first equivalence we consider is strictly weaker than Tretmans' equivalence and undecidable, whereas the second notion is incomparable. We also establish (un)decidability results for these equivalences.

This is a joint work with Puneet Bhateja and Madhavan Mukund from the Chennai Mathematical Institute