PhD Position in Model-based Testing

The Institute for Software Technology, Graz University of Technology, Austria,
has an opening for a Ph.D. position in model-based testing.

** Application deadline: October 20, 2014
** Salary: ~ EUR 36,600 per year before taxes
** The applicants should preferably have completed a Master's degree
     (or similar), or being on the verge of completing one.
** The candidate should preferably have a background in model-based
     testing or formal methods.

The Ph.D. research project focuses on the model-based testing of
non-functional requirements, like real-time, memory, and energy
constraints. The research is a continuation of the completed TRUFAL
project (http://trufal.wordpress.com). Research partners are AIT and
AVL. The theoretical work involves the selection and adaptation of
appropriate modelling languages, defining their formal semantics and
developing an appropriate testing theory. The practical work comprises
modelling, tool development and industrial case-studies.

The position is for 3 years and should lead to a PhD thesis at the Graz
University of Technology (TU Graz).

The PhD candidate will be supervised by Prof. Aichernig (see contact details below).

The application should include:

-    Application letter (max. 2 pages)
-    CV (summarising education, positions and academic work - scientific publications)
-    Copies of educational certificates, transcript of records and letters of recommendation
-    Documentation of English proficiency (if mother tongue not English)
-    List of publications and academic work that the applicant wishes
      to be considered (if any; no problems if there aren't any)
-    Names and contact details of 2-3 references (name, relation to candidate, e-mail and telephone number)
-    Foreign applicants are advised to attach an explanation of their University’s grading system.

For further information about the position, informal requests, etc., please contact
Bernhard Aichernig, email: aichernig AT ist.tugraz.at

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.