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.

Erlang Books

Recently we started some student projects on distributed programming in Erlang. Erlang is a functional programming language for developing distributed fault-tolerant applications with soft-realtime requirements. Erlang comes with a powerful library supporting common architectural patterns.

The distinguishing feature of Erlang is the combination of the functional paradigm with the actor communication model. Every recursive function can be easily turned into a process that communicates via asynchronous messages with other processes. The only state in an Erlang program is the state of the communication mailboxes. Hence, no variables are shared. Therefore, functions or processes can be safely replaced during runtime.

Furthermore, Erlang comes with its own virtual machine that fully exploits multi-core processors. Erlang demonstrates the advantages of a declarative language when developing distributed applications.
As a starter I recommend the book of Erlang's inventor Joe Armstrong:

For a deeper understanding of Erlang's framework library OTP I recommend:

Have fun with Erlang!

P.S: Erlang is not just fun. Amazon's distributed database web-service SimpleDB is written in Erlang.

My Student Projects for 2011/12

Creativity without reflection is dangerous!

These are my project proposals for student projects in the academic year 2011/12. 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.



MOMUTBUCK - Model-based Mutation Testing of a Controller for a Bucket Arm of a Wheel Loader
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 a given Java implementation. Especially, the combination of random and mutation testing shall be investigated. This project is related to our completed FP7 MOGENTES project and to the running TRUFAL project.

ERLBUCK - Developing the controller of the bucket arm of a wheel-loader in Erlang (taken)
The aim of this project is to investigate the language features of Erlang and develop a distributed implementation of the controller. A UML model, a Java implementation and test cases exists. The idea is to use test-driven development to develop the distributed solution.

AUTOFAULT - Fault Models in the Automotive Domain
Fault models capture typical faults that occur during the development of software. The task of this project is to analyze typical faults specific to the automotive application domain. The bug history at AVL shall be analyzed regarding common faults specific to the domain and user requirements. In model-based mutation testing, such fault models serve as a basis to develop mutation operators, injecting faults into a model. Then test cases are generated targeting these specific faults. This project is related to our completed FP7 MOGENTES project and to the running TRUFAL project.

ACTIONSAT - Action System to SMT Solver Translation
Action systems are a modeling framework well suited for modeling reactive systems, e.g. control logics of embedded systems. SMT Solvers are special SAT-Solvers extended with reasoning mechanisms for specific data types. SMT stands for SAT Modulo Theory. The aim is to develop a translator from the specification language of action systems to SMT-Lib, the standard input language for SMT solvers. Such a translation will enable the symbolic analysis of action system models, e.g., for test case generation.

• One option is to develop the translator in Prolog
• Another option is to use the new programming language Scala (taken)

ACTIONMIN - Action System to Minion Constraint Solver Translation
Action systems are a modeling framework well suited for modeling reactive systems, e.g. control logics of embedded systems. The Minion Constraint Solver is highly optimized solver for solving constraint satisfaction problems. The aim is to develop a translator from the specification language of action systems to the input language of Minion. Such a translation will enable the symbolic analysis of action system models, e.g., for test case generation

• One option is to develop the translator in Prolog
• Another option is to use the new programming language Scala

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.

ERLTOPDOWN - Systematic Distributed System Development in ERLANG (taken)
The aim of this project is to investigate the systematic top-down development of a sequential system description into a reliable distributed ERLANG application. ERLANG is a functional language for developing highly fault-tolerant distributed systems consisting of thousands of light-weight parallel processes. The student will start with the existing formal method RAISE and map the concepts to ERLANG programming.

CLOUDTCG - Distributed Test Case Generation in the CLOUD
Our group has considerable experience in developing model-based test case generators using mutation analysis. This technique subsumes other test case generation techniques, but is computationally expensive. We face state-space explosion problems known from model checking. One way to cope with this problem is to develop distributed test case generation algorithms. The idea is to use ERLANG as an implementation framework for these algorithms. The student shall develop a first prototype demonstrating the basic distributed architecture of such a new test case generator running in the cloud

DOMFAULTOSS - Domain Specific Fault Models in OSS
Fault models capture typical faults that occur during the development of software. The task of this project is to analyze typical faults specific to a certain application domain. The bug history of open-source software shall be analyzed regarding common faults specific to the domain and user requirements. In model-based mutation testing, such fault models serve as a basis to develop mutation operators, injecting faults into a model. Then test cases are generated targeting these specific faults.

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 completed 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.

Student Projects 2011

Photo: PhillipC

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

• ERLTOPDOWN - Systematic Distributed System Development in ERLANG
  The aim of this project is to investigate the systematic top-down development of a sequential
  system description into a reliable distributed ERLANG application. ERLANG is a functional language for developing highly fault-tolerant distributed systems consisting of thousands of light-weight parallel processes. The student will start with the existing formal method RAISE and map the concepts to ERLANG programming.
  
• CLOUDTCG - Distributed Test Case Generation in the CLOUD
  Our group has considerable experience in developing model-based test case generators using mutation analysis. This technique subsumes other test case generation techniques, but is computationally expensive. We face state-space explosion problems known from model checking.
  One way to cope with this problem is to develop distributed test case generation algorithms.
  The idea is to use ERLANG as an implementation framework for these algorithms. The student shall
  develop a first prototype demonstrating the basic distributed architecture of such a new test case generator running in the cloud.
  
• ERLSIP Developing a SIP-Server in Erlang
  The aim of this project is to investigate the language features of Erlang and develop a server implementing (parts of) the SIP protocol. SIP (Session-Initiation-Protocol) is used in Voice-Over-IP applications. Other protocols, like the conference protocol are possible.
  
• DOMFAULT - Domain Specific Fault Models
  Fault models capture typical faults that occur during the development of software. The task of this project is to analyze typical faults specific to a certain application domain. The bug history of open-source software shall be analyzed regarding common faults specific to the domain and user requirements. In model-based mutation testing, such fault models serve as a basis to develop mutation operators, injecting faults into a model. Then test cases are generated targeting these specific faults.
  
• ACTIONSAT - Action System to SMT Solver Translation
  Action systems are a modeling framework well suited for modeling reactive systems, e.g. control logics of embedded systems. SMT Solvers are special SAT-Solvers extend with reasoning mechanisms for specific data types. SMT stands for SAT Modulo Theory. The aim is to develop a translator from the specification language of action systems to SMT-Lib, the standard input language for SMT solvers. Such a translation will enable the symbolic analysis of action system models, e.g., for test case generation.
  
• 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.

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.

Two in One: functional plus OO-programming in Scala

Photo: PyEuler

I believe in the functional first approach to teach computer programming to computer scientists. This means that students start with a functional programming language before programming in an imperative object-oriented style.

The advantage of this approach is that at the beginning the students can focus on problem solving writing functions with a given set of data structures ignoring the computer architecture. Only later they concentrate on how to implement such data-structures in an efficient way by exploiting the computer architecture.

From 1998-2001 I was involved in such a course to first year students of TU Graz. We started with SML in the first half-year  and then switched to Java. All this could now be done in the programming language Scala that combines the pros of both programming paradigms. 

I recommend to take a closer look at Scala. It might be the Java of the future. Scala combines features of both worlds. The most prominent features I've missed so long in OO languages are there:

• functions are values
• pattern matching
• higher order functions
• closures
• lazy evaluation
• Milner's type inference system

However, it is far from being un-orthodox with OO features like:

• all values are objects
• compiles to the Java Virtual Machine
• full overloading including operators
• (multiple) inheritance
• direct definition of (singleton) objects 
• support for concurrency

The power this combination of paradigms brings cannot be underestimated: Scala's control structures can be extended in the language itself. Hence, it is possible to write domain specific commands. An example is Scala's support for the Actor communication model known from Erlang. It has been defined purely in Scala and is included as a library. Voila! Parallel programming with Actors on the JVM.  Use the summer break to dive into Scala! Fun included.

Lecturing in China

From 2002 to 2006 I worked for the UN as a Research Fellow of UNU-IIST in Macao, a special administrative region of China. Part of the job was to hold advanced computer-science courses in developing countries. The participants were post-graduates, typically young assistant professors.

In 2003, at a course in Lanzhou I certainly got the most impressive welcome: my name on a banner at the entrance to the campus (see picture). In China protocol is important, but Lanzhou Jiatong University was special. As a UN representative I was also officially welcomed by the rector and interviewed by their campus TV. I must admit, I was slightly impressed. Even more so by the fact that they had their own hotel on campus in which I stayed.

The course title was Formal Methods in Software Development. Lanzhou Jiatong University, Lanzhou, China, December 15--19, 2003.

Teaching formal methods is fun!

The course participants.

Lecturing in Africa

From 2002 to 2006 I worked for the UN  as a Research Fellow of UNU-IIST in Macao, China. Part of the job was to hold advanced computer-science courses in developing countries. The participants were post-graduates, typically young assistant professors. 

Most fascinating and adventurous were my two courses in Africa, one in Lagos, Nigeria and one in Dakar, Senegal.

University of Lagos, Nigeria, Nov. 4-8, 2002

The course title was Formal Methods in Software Development. It was part of the School on Methods, Tools and Techniques for Industrial Software Development jointly organized by UNU-IIST and University of Lagos.

The Lagos course participants and their lecturer (guess who it is!).

Our lunch was colorful.

Universite Cheikh Anta Diop, Dakar, Senegal, November 24–28, 2003

The course in Dakar was on Foundations of Software Testing covering formal testing techniques.

The Dakar course participants and myself.

On the weekend there was time to enjoy the beauty of Africa.