A theory of testing for asynchronous concurrent systems
Gul Agha, Prasannaa Thati · 2003
Testing equivalence is a notion of process equivalence that is widely used for establishing semantic correspondence between concurrent systems. Testing equivalence can be used to formally establish the fact that a given since the definition of testing equivalence involves a universal quantification over all possible contexts, proving equivalences between processes is a difficult task. In this dissertation, we present a collection of proof techniques and decision procedures for establishing testing equivalences between asynchronous concurrent systems. The process model that will be our primary focus is the π-calculus, which has been one of the most popular models of concurrency since its introduction a decade-and-a-half ago. We study a collection of typed variants of π-calculus that enforce several ontological commitments in addition to those in the basic π-calculus. These commitments capture ubiquitous computational phenomena such as asynchrony, locality, object paradigm, and restrictions on pointer comparisons. We investigate testing equivalence on several variants of π-calculus with combinations of these features. The result is a collection of proof techniques that can be applied to reason about a rich class of systems that exhibit these computational features. The central idea behind our proof techniques for testing equivalence is to obtain semantic characterizations of the equivalence that do away with universal quantification over contexts. Using these characterizations one can thus establish an equivalence by simply comparing the semantic mappings interactions with all possible contexts of use. We use these semantic characterizations to obtain both complete axiomatizations of the equivalence and decision procedures for it over restricted classes of processes. We have also implemented some of the variants of π-calculus and the proof techniques we have developed for establishing equivalences over them.