Student Projects 2010

Photo: PhillipC

These are my project proposals for student projects in 2010. 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 weekly meetings.

• MOMUTSIP - Model-based Mutation Testing of the SIP Protocol: Model-based Mutation Testing is a black-box testing technique, where mutation testing is applied on the modeling level. We have developed an automated test case generator based on this technique. The aim of this project is to evaluate the tool and technique for the Session Initiation Protocol used in Voice-Over-IP applications. This project is related to our FP7 MOGENTES project.


• MOMUTCON - Model-based Mutation Testing of the Conference Protocol: Model-based Mutation Testing is a black-box testing technique, where mutation testing is applied on the modeling level. We have developed an automated test case generator based on this technique. The aim of this project is to evaluate the tool and technique for the Conference Protocol, a simple multicast chat box protocol. This project is related to our FP7 MOGENTES project.


• MOMUTSUR - Model-based Mutation Testing Survey: Model-based Mutation Testing is a black-box testing technique, where mutation testing is applied on the modeling level. We have developed an automated test case generator based on this technique. The aim of this project is to research related work and write a survey on the topic. This includes the study of related literature as well as the evaluation of other existing tools. This project is related to our FP7 MOGENTES project.


• SEMU - Semantic Mutations of UML State Chart Diagrams: Model-based Mutation Testing is a black-box testing technique, where mutation testing is applied on the modeling level. In model-based mutation testing a model is mutated by changing its syntax. The mutants represent bugs and test cases are generated to detect such bugs in an implementation. In this project we consider semantic mutations of models, i.e. what are the possible faulty interpretations of a given model. It is well-known that there are several possible interpretations of UML state charts. The student shall investigate the state of the art on this topic and describe the possible semantic variations. This semantic variations will be build into our UML-Action System translator for generating test cases. The idea is to generate test cases that will detect faulty behavior due to semantic misinterpretations. This project is related to our FP7 MOGENTES project.


• COCA - Concolic Execution of Action Systems: Concolic stands for concrete and symbolic execution and is a technique for systematically exploring the paths of a program. Prominent tools that use this technique are jCute and PEX. The aim of this project is to develop a concolic executor for Action Systems. Action systems are a modeling framework well suited for modeling reactive systems, e.g. control logics of embedded systems. The student will study the problem and develop a prototype for a subset of the language. We currently use Action Systems as input to our model-based testing tools in the FP7 project MOGENTES.


• SYMPRO - Symbolic Execution in Prolog: Symbolic execution is a technique we currently use for automated test case generation. In symbolic execution a program is executed with symbolic values. The result of such a symbolic execution is a formula describing all possible outputs dependent on the symbolic inputs. Prolog is well-suited to implement such a symbolic interpreter. The aim of this project is to use the professional prolog system Sicstus to develop a prototype symbolic interpreter for a small programming language. The idea is to exploit the Constraint Solvers of Sicstus Prolog in the style of constraint logic programming.


• MUTO - Mutation Operators for Object-Oriented Action Systems: (in progress) Model-based Mutation Testing is a black-box testing technique, where mutation testing is applied on the modeling level. In model-based mutation testing a model is mutated by changing its syntax. The mutants represent bugs and test cases are generated to detect such bugs in an implementation. The mutants are generated by so called mutation operators. A mutation operator is a rule how a certain syntactic term, e.g. a programming statement, should be changed. This changes or mutations represent faults. The aim of this project is to define a set of mutation operators for our Object-Oriented Action System modeling language. Based on this, a tool shall be developed that takes a model and the set of mutation operators and produces a number of mutated versions of this model (mutants). We use such mutants as input for our test case generator.


• MOMUTCAR - Model-based Mutation Testing of a Car Alarm System: (in progress) Model-based Mutation Testing is a black-box testing technique, where mutation testing is applied on the modeling level. We have developed an automated test case generator based on this technique. The aim of this project is to evaluate the tool and technique for an industrial case study of a car alarm system. This project is related to our FP7 MOGENTES project.

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.

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.

MOGENTES Project

I am the project manager and senior researcher for TU Graz in the MOGENTES project.

MOGENTES stands for Model-based Generation of Tests for Dependable Embedded Systems and is an European STREP project in the 7th EU framework programme.

The coordinator is the Austrian Institute of Technology.

MOGENTES aims at significantly enhancing testing and verification of dependable embedded systems by means of automated generation of test cases relying on development of new approaches as well as innovative integration of state-of-the-art techniques.

Driven by the needs of its industrial partners, it will address both testing of non-functional issues like reliability, e.g. by system stress and overload tests, and functional safety tests, meeting the requirements of standards such as IEC 61508, ISO WD 26262, or AUTOSAR.

MOGENTES will demonstrate that different domains with a wide variety of requirements can significantly benefit from a common model-based approach for achieving automated generation of efficient test cases and for verifying system safety correctness using formal methods and fault injection, as this approach increases system development productivity while achieving predictable system dependability properties. For that purpose, proof-of concept demonstrations will show the applicability of the developed technologies in two application domains: railway and automotive (on- and off-road).

In particular, MOGENTES aims at the application of these technologies in large industrial systems, simultaneously enabling application domain experts (with rather little knowledge and experience in usage of formal methods) to use them with minimal learning effort. All in all, MOGENTES will increase knowledge and develop new techniques and tools in the area of verification and validation of dependable embedded systems which can be applied in model-based development processes also by non-experts in formal methods.