New journal article on model-based testing

Today, our new journal article appeared in the Science of Computer Programming journal of Elsevier.

It deals with the problem of automatically generating test-cases from mutated models:

Bernhard K. Aichernig, Elisabeth Jöbstl, and Stefan Tiran. Model-based mutation testing via symbolic refinement checking. Science of Computer Programming. 97 (2015): 383-404, Elsevier, 2015.

Here is a link to a free copy of it that works for 50 days.

Highlights:

• We deal with model- and mutation-based test case generation.
• The main focus lies on optimizations of the underlying conformance check.
• We explain the construction of test cases based on the conformance check.
• We allow for non-determinism in the test models.
• We demonstrate the effectiveness of our optimizations on industrial case studies.

Enjoy!

Integrating model-based testing and analysis tools via test case exchange

Our first publication in the MBAT project was presented at TASE 2012 and in a seminar given at UNU-IIST:

Bernhard K. Aichernig, Florian Lorber, and Stefan Tiran. Integrating model-based testing and analysis tools via test case exchange. In TASE 2012, 6th IEEE International Symposium on Theoretical Aspects of Software Engineering, July 4–6, Beijing, China, pages 119-126. IEEE Computer Society, 2012. (PDF)

In this paper we show an integration of two tools via test cases. For example test cases are generated from a model in Tool 1 and then model checked in another Tool 2. This is useful when a modeling tool does not support model checking as it is the case with most UML tools.

Abstract: Europe’s industry in embedded system design is currently aiming for a better integration of tools that support their development, validation and verification processes. The idea is to combine model-driven development with model-based testing and model-based analysis. The interoperability of tools shall be achieved with the help of meta-models that facilitate the mapping between different modelling notations. However, the syntactic and semantic integration of tools is a complex and costly task. A common problem is that different tools support different subsets of a language. Furthermore, semantic differences are a major obstacle to sound integration efforts.

 In this paper we advocate an alternative, more pragmatic approach. We propose the exchange of test cases generated from the models instead of exchanging the models themselves. The advantage is that test cases have a much simpler syntax and semantics, and hence, the mapping between different tools is easier to implement and to maintain. With a formal testing approach with adequate testing criteria a set of test cases can be viewed as partial models that can be formally analysed. We demonstrate an integration of our test case generator Ulysses with the CADP toolbox by means of test case exchange. We generate test cases in Ulysses and verify properties in CADP. We also generate test cases in CADP and perform a mutation analysis in Ulysses.

ICTSS 2012, Aalborg, Denmark

Photo: dinilu

I have been invited to serve on the Program Committee of ICTSS 2012, the 23rd IFIP Int. Conference on Testing Software and Systems, November 19-21, 2012 Aalborg, Denmark.

Please, consider submitting your testing work until June 11, 2012 (abstracts), June 18, 2012 (full papers).

Brian Nielsen, Aalborg University, DK and Carsten Weise, IVU Traffic Technologies, DE are the program chairs. For details see the conference homepage.

Last year, we presented a paper at ICTSS in Paris:

Christian Schwarzl, Bernhard K. Aichernig, and Franz Wotawa. Compositional random testing using extended symbolic transition systems. In Burkhart Wolff and Fatiha Zaïdi, editors, Testing Software and Systems - 23rd IFIP WG 6.1 International Conference, ICTSS 2011, Paris, France, November 7-10, 2011. Proceedings, volume 7019 of Lecture Notes in Computer Science, pages 179–194. Springer-Verlag, 2011. (PDF)

Towards Symbolic Model-Based Mutation Testing: Combining Reachability and Refinement Checking

We present our newest paper on model-based mutation testing accepted at MBT 2012.

Model-based mutation testing uses altered test models to derive test cases that are able to reveal whether a modelled fault has been implemented. This requires conformance checking between the original and the mutated model. This paper presents an approach for symbolic conformance checking of action systems, which are well-suited to specify reactive systems.

We also consider non-determinism in our models. Hence, we do not check for equivalence, but for refinement. We encode the transition relation as well as the conformance relation as a constraint satisfaction problem and use a constraint solver in our reachability and refinement checking algorithms.

Explicit conformance checking techniques often face state space explosion. First experimental evaluations show that our approach has potential to outperform explicit conformance checkers.

This research is part of the TRUFAL project.

Download PDF

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 two 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.

Semantics? Yes tester, you need it!

Once I had a testing project in industry in which we ran into the common situation that we did not know how to interpret a given requirement. Well, we asked the requirements manager for advice. Since it was a tricky question, he forwarded our request to the customer and to the developers. We were fortunate in getting quick responses. However, there was a problem: the answers were contradicting each other.

What had happened? Well, the customer and the developers had different interpretations of the requirements. There was a misunderstanding about this requirement. The consequence: the developers were implementing an incorrect system from the customers point of view.

So what about the tester? His understanding of the requirements is crucial. In the example above, the asking of us testers highlighted a serious problem. Without a clear understanding of the requirements, no reliable test verdict (pass or fail) can be given.

However, how do we know, if a tester understands the requirements? He could have made the same mistake as the developers. What if two testers (e.g. the customer's and the developer's) have different understandings of the requirements of a given SUT? Well, they would give different test verdicts: one might accept the SUT the other not. Is there a way to prevent such misunderstandings?

Not in general, because misunderstanding is a psychological process of wrong interpretation. However, we can limit the roots of such misinterpretations. We need to define the semantics, i.e. the meaning, of the requirements. And if nobody does it in a project, the tester should.

How do we define the semantics of requirements? Answer: by writing them in a formal notation with a precise semantics. There are modeling languages that come with a precise semantics, like VDM-SL, Z, B, Alloy, RAISE, CSP, LOTOS etc. These languages serve different purposes, but what they have in common is that their meaning is precisely defined, i.e. there is no ambiguity how to interpret what is written down.

Therefore, model-based testing should always apply models with a precise, formal semantics. Ok, most of the time a tester will not need it, because the meaning seems obvious, but as testers know, the rare cases matter. It even becomes more critical for model-based testing tools. If there is no precise standard semantics, different tools might behave differently for the same models. (A common problem of compilers for programming languages without precise semantics).

Here is my advice: if somebody tries to sells you a model-based testing technique, ask him if his notation has a formal semantics. If he answers positively, double-check and ask for formal proofs done in this notation. No proofs, no formal semantics. Don't accept notations with misunderstanding built in!

More on model-based testing with formal notations can be found in my publications.