Student Projects 2013/14

This is a selection of my proposals for student projects in the academic year 2013/14.

Most of the topics can be scaled to small student projects, bachelor thesis projects, master thesis projects and in some cases up to dissertation subjects. The projects are not isolated but fit the current research agenda of my group. The students are supervised in meetings in two-week periods. Please, contact me, if you are interested

MBAT-AVL

This is a paid project in the context of our MBAT project. AVL Graz is looking for students assisting them in their tasks in the project. AVL, together with TU Graz, wants to evaluate existing model-based test case generation tools on their automotive demonstrators. The tasks involve modeling of the expected behavior, developing test-drivers and evaluate the tools with a common benchmark example.

This would be a master project, but it can be downscaled to different levels, e.g. by selecting a subset of tools.

TRUFAL-Prolog2Scala

This is a project in the context of our TRUFAL project. The plan is to port an existing test case generator implemented in Prolog to Scala. The test case generator implements model-based mutation testing and takes as input models Action Systems. The plan is to port this implementation to Scala and then parallelize the algorithms. This will be a bachelor or master project.

TRUFAL-Coverage

This is a project in the context of our TRUFAL project. The aim is to implement transition coverage of UML state machines into our existing test case generator. Experiments will be conducted comparing mutation coverage and random coverage to the new test selection strategy. The implementation language is Prolog.

TRUFAL-Case-Studies

The aim is to conduct several case studies using our model-based testing tools. The tasks may involve modeling of the system under test, implementation/selection of a benchmark system-under-test, implementation of a test-adapter, tool evaluation, and empirical studies. Comparisons with other tools, e.g. with Spec Explorer, is also possible.

Proof-based Development of Test Models

The aim of this project is to formally develop test models from informal requirements. The modeling language will be Event-B. The IDE will be the Eclipse platform Rodin. The development involves tool-supported correctness proofs over several refinement steps. For a master thesis an integration of our existing test case generators with Event-B would be a possible extension.

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.

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)