New Journal Article on Test-Case Generation and Fault Propagation

Our new article on fault propagation and its relation to model-based test-case generation was just published:

Bernhard K. Aichernig, Elisabeth Jöbstl, and Martin Tappler. Does this fault lead to failure? Combining refinement and input-output conformance checking in fault-oriented test-case generation. Journal of Logical and Algebraic Methods in Programming, 85(5, Part 2):806–823, 2016. (PDF) (doi:10.1016/j.jlamp.2016.02.002)

The publisher Elsevier provides a free download of the original article until December 2.

The paper describes how we generate test-cases for reactive systems by

1. injecting faults into the models (mutation testing)
2. generating a test-case that triggers this fault (refinement checking)
3. extending the test-case until an observational failure could be produced (ioco checking).

We show that this is more efficient than previous approaches that search for observational equivalences directly, i.e. skipping Step 2.

Our case study of a car-alarm controller shows that for some subtle faults we need up to nine additional interactions until a fault becomes visible at the interface.

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.

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

Protocol conformance testing a SIP registrar

Photo: Tiptel

In recent years we have successfully applied model-based mutation testing to several implementations of communication protocols. In our work reported in

Bernhard K. Aichernig, Bernhard Peischl, Martin Weiglhofer, and Franz Wotawa. Protocol conformance testing a SIP registrar: an industrial application of formal methods. In Mike Hinchey and Tiziana Margaria, editors, Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), 10-14 September 2007, London, England, UK, pages 215–226. IEEE Computer Society, 2007. (PDF) (doi:10.1109/SEFM.2007.31)

we tested parts of the Session Initiation Protocol (SIP) used in internet telephony in order to register and connect communication partners.

Our case study targeted a commercial and an open-source (OpenSER) SIP registrar. Furthermore, we compared the mutation approach to a standard model-based test case generation technique. Our mutation technique generated 124 test cases, compared to 6000 test cases generated by the standard approach.

The 6000 tests discovered nine different faults in the commercial SIP registrar and four in the open-source registrar OpenSER.

Interesting was the fact that the comparatively small set of 124 mutation tests uncovered one additional fault in the commercial implementation that was not detected by the 6000 tests of the classical approach.

This is a further indication that mutation testing could play an important role in a mature testing process.

Another important contribution of this paper was to show how our mutation technique could be scaled to larger models. We sliced the models with the help of markers around the injected faults.

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.

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.

Journal Paper: Fault-Based Conformance Testing in Practice

Photo: marcusuke

We got our work on mutation testing of communication protocols published in the International Journal of Software and Informatics.

The article is part of a special double issue on Formal Methods edited by Prof. Dines Bjorner. The journal is published by the Chinese Academy of Science and has an international editing board.

Martin Weiglhofer, Bernhard Aichernig, and Franz Wotawa. Fault-based conformance testing in practice. International Journal of Software and Informatics, 3(2–3):375–411, June/September 2009. Copyright by Institute for Software, Chinese Academy of Science. (PDF)

In this work we present our results on testing two communcation protocols the Session Initiation Protocol and the Conference Protocol. The protocols are modeled in LOTOS and then mutation testing is applied on the LOTOS specs for generating test cases. We present detailed data of the test process including the nice result that we were able to find a new bug in an implementation that was not detected by random and scenario-based testing.

Paper abstract: Conforming to protocol specications is a critical issue in modern distributed software systems. Nowadays, complex service infrastructures, such as Voice-over-IP systems, are usually built by combining components of dierent vendors. If the components do not correctly implement the various protocol specications, failures will certainly occur. In the case of emergency calls this may be even life-threatening. Functional black-box conformance testing, where one checks the conformance of the implemented protocol to a specication becomes therefore a major issue. In this work, we report on our experiences and ndings when applying fault-based conformance testing to an industrial application. Besides a discussion on modeling and simplications we present a technique that prevents an application from implementing particular faults. Faults are modeled at the level of the specication. We show how such a technique can be adapted to specications with large state spaces and present results obtained when applying our technique to the Session Initiation Protocol and to the Conference Protocol. Finally, we compare our results to random and scenario based testing.

AI meets Formal Methods: Qualitative Reasoning and Action Systems

Photo: cokada

We got our work on combining Qualitative Reasoning Techniques with Action Systems accepted at ICFEM 2009 in Rio.

This year the conference was highly competitive with an acceptance rate below 30 percent. The paper integrates Qualitative Differential Equations into Back's Action System formalism for modeling hybrid systems. The work forms part of the MOGENTES Project and aims at model-based testing of hybrid systems.

To our knowledge this is the first time that Qualitative Differential Equations have been merged into a formal development technique. The results are not limited to Action Systems, but apply also to similar formalisms like e.g. Event-B.

Bernhard K. Aichernig, Harald Brandl, and Willibald Krenn. Qualitative action systems. In Proceedings of ICFEM 2009: 11th International Conference on Formal Engineering Methods, Dec 9-12, 2009, Rio de Janeiro, Lecture Notes in Computer Science. Springer-Verlag, 2009. in press. (PDF)

Paper abstract: An extension to action systems is presented facilitating the modeling of continuous behavior in the discrete domain. The original action system formalism has been developed by Back et al. in order to describe parallel and distributed computations of discrete systems, i.e. systems with discrete state space and discrete control. In order to cope with hybrid systems, i.e. systems with continuous evolution and discrete control, two extensions have been proposed: hybrid action sys- tems and continuous action systems. Both use dierential equations (relations) to describe continuous evolution. Our version of action systems takes an alternative approach by adding a level of abstraction: continuous behavior is modeled by Qualitative Dierential Equations that are the preferred choice when it comes to specifying abstract and possibly non-deterministic requirements of continuous behavior. Because their solutions are transition systems, all evolutions in our qualitative action systems are discrete. Based on hybrid action systems, we develop a new theory of qualitative action systems and discuss how we have applied such models in the context of automated test-case generation for hybrid systems.

Modeling and Testing Multi-Threaded Asynchronous Systems with Creol

Bosphorus bridge in Istanbul viewing from Asia to Europe.

After a long waiting period, yesterday our TTSS 2008 paper was published by Elsevier. The paper is a result of the CREDO project.

Bernhard Aichernig, Andreas Griesmayer, Rudolf Schlatte, and Andries Stam. Modeling and testing multi-threaded asynchronous systems with Creol. In Proceedings of the 2nd International Workshop on Harnessing Theories for Tool Support in Software (TTSS 2008), Istanbul, Turkey, 30 August 2008, volume 243 of Electronic Notes in Theoretical Computer Science, pages 3–14. Elsevier, July 2009. (PDF) (doi:10.1016/j.entcs.2009.07.002)

The paper describes a model-based testing technique for asynchronous, concurrent systems and shows how the modeling language Creol can serve as a test oracle. Creol is a nice object-oriented modeling language for distributed systems by University of Oslo. We applied the technique to a commercial agent-based information system.

The basic steps of our method are:

• Create an abstract model of the system under test (SUT) in Creol.
• Instrument the source code of the SUT by aspect-oriented programming techniques (here AspectC) for recording events.
• Execute tests on the SUT and record the events.
• Translate the event traces to Creol test cases.
• Replay the test case on the model.
• If successful: the test passed;
• If it fails: model check if there is a different non-deterministic path for this test case, if not the test failed.

Check out my other conference papers.