SYANCO Winter School, Feb 8-12, Berlin

Photo: alles-schlumpf

I have been invited to lecture on the upcoming SYANCO Winter School in Berlin.

The International Winter School on Synthesis and Analysis of Component Connectors is taking place from 8 till the 12 of February 2010 at Park Inn Berlin-Alexanderplatz, Berlin, Germany. It is jointly organized by Coordination Languages Research Group (SEN3), Centrum Wiskunde & Informatica (CWI), the Netherlands and Faculty of Computer Science, TU Dresden, Germany.

I will give a 3 hours lecture on Model-based Mutation Testing: Foundations and Applications. This lecture gives an introduction to mutation testing on the modelling level.

The original idea of mutation testing on the source-code level goes back to the late 1970s and works as follows: The tester injects faults into a program under test, by deliberately changing its source code. This faulty versions of the program are called mutants. Then, test cases are executed on these mutants. If all the faults are detected, the set of test cases can be considered adequate. If the tests fail this quality assessment, then additional test cases should be designed until all faults are detected. The assumption is that other faults in the original program can be caught as well, if it is able to detect the injected faults. We show how this technique can be applied in model-based testing. The idea is to automatically generate test cases from mutated formal models. The test cases are designed to detect those bugs in a system under test that have been anticipated on the modelling level. In the course we will present (1) the general theory behind our technique, based on program semantics and refinement preorders, (2) map the theory to different modelling styles, including contracts and process algebras, and (3) discuss the model-based mutation testing of protocols and embedded systems.

Read More

SEFM 2010, 13-17 September, Pisa, Italy

Photo: Pisa 2007

I have been invited to serve on the Program Committee of SEFM 2010, the 8th IEEE International Conference on Software Engineering and Formal Methods. SEFM 2010 will take place in Pisa. Submission deadline for abstracts is 22 March 2010. The PC-chairs are Jose Luis Fiadeiro and Stefania Gnesi.

The aim of the conference is to bring together practitioners and researchers from academia, industry and government to advance the state of the art in formal methods, to facilitate their uptake in the software industry and to encourage their integration with practical engineering methods. Papers that combine formal methods and software engineering are especially welcome.

I served as a PC-Cochair for SEFM 2005. For information on the past SEFM conferences visit the general SEFM webpage.

Here the call for papers will be published as soon as it is out.

Read More

Fault-based Test Case Generation for Component Connectors

Photo: Matthew Stinson

Sun Meng at CWI had the idea to translate my UTP-theory of mutation testing to REO connectors. This resulted in a TASE 2009 paper published in July:

Bernhard K. Aichernig, Farhad Arbab, Lacramioara Astefanoaei, Frank S. de Boer, Sun Meng, and Jan Rutten. Fault-based test case generation for component connectors. In TASE 2009, Third IEEE International Symposium on Theoretical Aspects of Software Engineering, Tianjin, China, July 29–31, pages 147–154. IEEE Computer Society, July 2009. Copyright by IEEE. (PDF) (doi:10.1109/TASE.2009.14)

The paper demonstrates that the idea of formalizing basic software engineering concepts in Hoare and He's Unifying Theories of Programming really helps to transfer knowledge and technology. In this case mutation testing found a new application domain: component connectors for modeling coordination in service-oriented architectures.

Abstract. The complex interactions appearing in service-oriented computing make coordination a key concern in serviceoriented systems. In this paper, we present a fault-based method to generate test cases for component connectors from specifications. For connectors, faults are caused by possible errors during the development process, such as wrongly used channels, missing or redundant subcircuits, or circuits with wrongly constructed topology. We give test cases and connectors a unifying formal semantics by using the notion of design, and generate test cases by solving constraints obtained from the specification and faulty connectors. A prototype symbolic test case generator serves to demonstrate the automatizing of the approach.

More conference papers.

Read More

FMCO 2008: Conformance Testing of Distributed Concurrent Systems with Executable Designs

Photo: *clairity*

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.

More conference papers.

Read More