In August our FMCO 2008 paper was published:
Bernhard K. Aichernig, Andreas Griesmayer, Einar Broch Johnsen, Rudolf Schlatte, and Andries Stam. Conformance testing of distributed concurrent systems with executable designs. In Formal Methods for Components and Objects: 7th International Symposium, FMCO 2008, Sophia Antipolis, France, October 21–23, 2008, Revised, volume 5751 of Lecture Notes in Computer Science, pages 61–81, Berlin/Heidelberg, August 2009. Springer. (PDF) (doi:10.1007/978-3-642-04167-9_4)
The paper is a result of the CREDO project. It shows our testing process based on the modeling language Creol. Concolic execution on the model generates test stimuli and these are then executed on a system under test. During a test run the event traces are recorded and then replayed on the model. A small GUI helps to identify the controllable events for generating the test driver for Creol.
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.