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