Conformance Testing of Distributed Concurrent Systems with Executable Designs

Abstract. This paper presents a unified approach to test case generation and conformance test execution in a distributed setting. A model in the object-oriented, concurrent modeling language Creol is used both for generating test inputs and as a test oracle. For test case generation, we extend Dynamic Symbolic Execution (also called Concolic Execution) to work with multi-threaded models and use this to generate test inputs that maximize model coverage. For test case execution, we establish a conformance relation based on trace inclusion by recording traces of events in the system under test and replaying them in the model. User input is handled by generating a test driver that supplies the needed stimuli to the model. An industrial case study of the Credo project serves to demonstrate the approach. Keywords. Model-based testing, conformance testing, concolic execution, Creol, Maude.

• Type: Conference
• Year: 2008
• Where: FMCO
• Authors: Bernhard K. Aichernig, Andreas Griesmayer, Einar Broch Johnsen, Rudolf Schlatte, Andries Stam
• Keywords: FMCO 2008, Formal Methods, Test Case, Test Case Generation, Test Inputs