Model Based Testing for Concurrent Systems with Labeled Event Structures

Submitted to a journal.Abstract. We propose a theoretical testing framework and a test generation algorithm for concurrent systems that are speci ed with true concurrency models, such as Petri nets or networks of automata. The semantic model of computation of such formalisms are labeled event structures, which allow to represent concurrency explicitly. The activity of testing relies on the de nition of a conformance relation that depends on the observable behaviors on the system under test. The ioco type conformance relations for sequential systems rely on the observation of sequences of inputs and outputs and blockings. However these relations are not capable of capturing and exploiting concurrency of non sequential behavior. We propose an extension of the ioco conformance relation for labeled event structures, named co-ioco, which allows to deal with explicit concurrency. We give an algorithm to build test cases from a given speci cation and prove that the generated test suite is complete for co-ioco