Habilitation

Yesterday, I have completed my habilitation process at TU Graz. The last step was a public 45 minutes talk on

"Model-Based Mutation Testing: From Semantics to Automated Test-Case Generation"

given to the faculty of computer science and the habilitation commission. After the talk I answered questions and defended my habilitation thesis.

The habilitation thesis with the title "Model-Based Mutation Testing: Theory and Application" was submitted in January. It consists of selected papers and a survey chapter.

The survey chapter is available for download: Survey Chapter Habilitationsschrift Aichernig.

The habilitation gives me the right to lecture any topic covered by my habilitation area "Practical Computer Science and Formal Methods in Computer Science". "Practical Computer Science" includes topics like Software Engineering and Programming Languages. "Formal Methods" are mathematically based techniques for the specification, development and verification of software and hardware systems.

More details regarding the history and concept of habilitation can be found on Wikipedia.

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.