Model Based Testing for Concurrent Systems with Labeled Event Structures
Hernán Ponce-de-León, Stefan Haar, Delphine Longuet · 2013
Abstract. We propose a theoretical testing framework and a test generation algorithm for concurrent systems that are specified 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 definition 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 specification and prove that the generated test suite is complete for co-ioco. 1