An axiomatic semantics for iocos_ conformance relation

iocos_ 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 iocos_. 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 iocos_ 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 iocos_-conforming with that specification. The issue of effectively computing the iocos_ relation is also addressed, we prove how the branching nature of iocos_ 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 iocos_ for the syntactic terms in BCCS. That is, we propose a set of inequations characterising iocos_.