An axiomatic semantics for iocos_ conformance relation

Abstract ioco s _ is a preorder on the states of a transition system with input and output actions. Its aim is to establish a new branching-time conformance framework. In this paper, we continue the study of ioco s _ . We consider an algebraic language ( BCCS ) with input and output actions. Then we define a structured operational semantics for the terms in BCCS . We prove that this operational semantics faithfully models the quiescent behaviour assumed by the conformance semantics. To model the test execution on systems, a language to express tests is described and the formal interaction between BCCS process terms and tests is defined. Then, we show that ioco s _ has a testing characterisation and an algorithm that produces a test suite for a given specification. The test suite produced by this algorithm discriminates exactly the implementations that are ioco s _ -conforming with that specification. The issue of effectively computing the ioco s _ relation is also addressed, we prove how the branching nature of ioco s _ makes it suitable to be solved as an instance of the Generalised Coarsest Partition Problem (GCCP). Finally, we describe a sound and ground-complete axiomatisation of ioco s _ for the syntactic terms in BCCS . That is, we propose a set of inequations characterising ioco s _ .