Abschlussarbeiten

Abschlussarbeiten

Bei Interesse an Abschlußarbeiten können Sie sich jederzeit an die Mitarbeiter des Fachgebiets oder an Frau Prof. Mezini wenden. Am Besten ist es wenn Sie sich vorher die aktuelle Liste der Forschungsthemen ansehen, da die allermeisten Arbeiten auch in diesen Bereichen vergeben werden. Sollten Sie ein Thema spannend finden, dann wenden Sie sich einfach an den Mitarbeiter, der das Thema bearbeitet. Haben Sie ein Thema aus dem Bereich Software Engineering / Softwaretechnik, dass Sie besonders spannend finden, welches aber nicht direkt zu einem der Forschungsthemen passt, dann sprechen Sie uns trotzdem einfach darauf an – vielleicht ergibt sich ja eine Betreuungsmöglichkeit.

  • 06.02.2017

    Debugging Big Data Applications

    Over the last few years, a vast amount of data has become available from a variety of heterogeneous sources, including social networks and cyber-physical systems. This state of the things has pushed recent research in the direction of investigating computing platforms and programming environments that support processing massive quantities of data. Systems like MapReduce, Spark, Flink, Storm, Hive, PigLating, Hadoop, HDFS have emerged to address the technical challenges posed by the nature of these computations, including parallelism, distribution, network communication and fault tolerance.

    The problem of debugging such applications, however, is still open. Traditional debuggers can hardly help because of the design of Bid Data frameworks: the code that developers write is not directly executed, but it is deployed on a system that features distribution, parallel execution, re-execution of slow computations and re-allocation of failed computations – all aspects that are not explicit in programmers’ code. To complicate things further, many Bid Data frameworks are based on a declarative functional programming model which clashes with the nature of the abstractions used by traditional debuggers (e.g., stepping over statements, inspecting state).

    This thesis aims at the design of a debugging system for Big Data applications. The objective is to use techniques for data provenance to track the flow of data in the application. This way, the location of a fault can be traced back to the root of the error significantly reducing the time required to debug Big Data software.

    References

    http://spark.apache.org

    Matei Zaharia, Mosharaf Chowdhury, Michael J. Franklin, Scott Shenker, and Ion Stoica. 2010. Spark: cluster computing with working sets. In Proceedings of the 2nd USENIX conference on Hot topics in cloud computing (HotCloud'10). USENIX Association, Berkeley, CA, USA, 10-10. weiter

  • 06.02.2017

    Analysis and Testing of Big Data Applications

    Over the last few years, a vast amount of data has become available from a variety of heterogeneous sources, including social networks and cyber-physical systems. This state of the things has pushed recent research in the direction of investigating computing platforms and programming environments that support processing massive quantities of data. Systems like MapReduce, Spark, Flink, Storm, Hive, PigLating, Hadoop, HDFS have emerged to address the technical challenges posed by the nature of these computations, including parallelism, distribution, network communication and fault tolerance.

    Despite the popularity of such systems, there has been little attention to aspects in the development process other than programming itself. For example, testing Big Data applications is an area that remains largely unexplored. This is even more surprising considering that testing has a long tradition in Software Engineering from a research standpoint (e.g., concoholic testing, mutation testing) as well as for practitioners, with established testing techniques and tools that are widespread in industry (e.g., JUnit).

    The goal of this thesis is to develop a testing methodology for Big Data applications focusing on the Apache Spark platform. The candidate will apply testing techniques based on symbolic execution to the setting of Big Data. Ideally, the thesis will include a comparison of different approaches as well as the development of a new methodology specifically tailored for Big Data.

    References

    http://spark.apache.org

    Matei Zaharia, Mosharaf Chowdhury, Michael J. Franklin, Scott Shenker, and Ion Stoica. 2010. Spark: cluster computing with working sets. In Proceedings of the 2nd USENIX conference on Hot topics in cloud computing (HotCloud'10). USENIX Association, Berkeley, CA, USA, 10-10. weiter

    Betreuer/in: Prof. Dr. Guido Salvaneschi

  • 17.08.2016

    Comparing Existing Tool Support for the Verification of a Type System’s Soundness

    Bachelorarbeit, Masterarbeit

    Type systems shall ensure that correctly typed programs do not get stuck during execution. More formally, type systems shall satisfy certain soundness criteria, for example, progress and preservation (see Pierce). However, proving the soundness of a type system by hand is a tedious and error-prone task. Therefore, it is desirable to make use of existing verification tools in order to create fully or at least partially machine-checked soundness proofs.

    Candidate tools for a formal verification of progress and preservation are for example Isabelle/HOL, Coq, Twelf, and Dafny. These theorem provers provide some support for automated verification of individual proof steps: For example, Isabelle Sledgehammer is a tactic that integrates automated first-order theorem provers such as the E-prover, SPASS, Vampire etc. into Isabelle. Dafny internally uses the SMT solver Z3 to automate proof steps. Twelf provides basic, but powerful support for automating some common forms of inductions which are typically used to prove properties about programming language specifications.

    Research Objective
    In this thesis, the student candidate shall evaluate how well these existing automation techniques are suited for facilitating the mechanisation of progress and preservation proofs. The student candidate shall use at least three existing verification tools (Isabelle/HOL and Dafny, and a third tool of her or his own choice) to formally prove progress and preservation of a type system specification for a subset of SQL and evaluate at least the following questions by experimenting with the formalised proofs:

    • Which general steps can each theorem prover automatically prove in the progress and preservation proof at hand?
    • Which steps cannot be automated, i.e. require manual interaction with the theorem prover?
    • How „much“ of the proofs can each prover automate, and what are sensible metrics to measure this quantity?
    • How does each of the theorem provers help with the discovery of proof steps?

    References

    weiter

    Betreuer/innen: Sylvia Grewe, M.Sc., Prof. Dr.-Ing. Mira Mezini

  • 05.08.2016

    Programming Languages for Software-Defined Networks

    Bachelorarbeit, Masterarbeit

    Software-Defined Networks (SDNs) provide a new way to configure computer networks. Special-purpose network devices with tightly coupled data and control planes are replaced by programmable switches managed by a logically centralized controller. The communication between the controller and these programmable switches is carried out using well-defined APIs (e.g., OpenFlow). Instead of configuring devices individually, network policies are implemented on top of the controller and then used by the controller to instruct individual network switches.However, SDN APIs like OpenFlow closely resemble the features provided by the hardware. OpenFlow uses a set of prioritized match-action rules as abstraction, which makes it difficult to write sophisticated network applications. For example, an application supporting multiple tasks at the same time must merge the switch-level rules required by each of the tasks into a single set of rules that can be installed on the switches. To overcome these limitations, different programming languages for SDNs have been proposed, that provide higher language abstractions on top of OpenFlow, including abstractions for querying the network state, basic service composition or language support for network verification.Developing new SDN language features requires a comparison with already existing languages, usually, in order to show that they increase the expressivity of the language while providing at least the same performance at runtime. However, currently it is quite cumbersome to compare different SDN languages, since they are implemented on top of different host languages, like Python, OCaml, Java and they usually provide only a small set of simple example application that are not directly comparable with each other.The goal of this thesis is to develop an extensible testbed for SDN applications that allows to compare SDN programming languages with respect to expressivity as well as performance and to provide a set of small- to medium-sized example applications that can be used for benchmarking and comparing the available language abstractions. Based on the results of the experiments, the next step will be to propose new language features that address the limitations of current solutions. weiter

    Betreuer/innen: Matthias Eichholz, M.Sc., Prof. Dr. Guido Salvaneschi

  • 04.01.2016

    Virtual Machine Support for Reactive Programming

    Just in time compiler – interpreter optimization

    Bachelorarbeit, Masterarbeit

    Over the last few years, reactive programming (RP) has gained the

    attention of researchers and practitioners for the potential to

    express otherwise complex reactive behavior in intuitive and

    declarative way. Implementations of RP have been proposed in several

    widespread languages, including Java, Python, Ruby, Javascript and

    Scala. Recently, concepts inspired by RP have been applied to

    production frameworks like Microsoft Reactive Extensions (Rx), which

    received great attention after the success story of the Netflix

    streaming media provider. Finally, a lot of attention in the frontend

    developers community is revealed by the increasing number of libraries

    that implement RP principles, among the others React.js, Bacon.js,

    Knockout, Meteor and Reactive.coffee.

    Performance remains, however, a major limitation of RP. Most RP

    implementations are based on libraries where the language runtime is

    agnostic to reactive abstractions. As a result, a number of aspects

    like change propagation, dependency tracking and memory management

    that could be specifically optimized can only benefit from general

    purpose optimization such as those provided by out of the box just in

    time compilers. Optimization at the virtual machine level has the

    potential to address these issues. weiter

    Betreuer/in: Prof. Dr. Guido Salvaneschi

  • 26.10.2015

    A library for safe composition of decoupled Event-based processes

    Bachelorarbeit, Masterarbeit

    The STG group at TU Darmstadt has formalised the E-calculus and a linear type system to model and statically validate composition of decoupled event-based processes, a.k.a. cooperative decoupled event-based processes. In the last decade, event-driven programming has become a major paradigm for developing distributed systems.

    Decoupling makes it possible for new components to get deployed at runtime respectively of existing components that can crash or leave without affecting others and enables modules underlying runtime components to be developed independently, e.g., in publish-subscribe systems, components are not bound to interfaces/modules of other components. However, it is an illusion to believe that one can just run components that were developed independently of each other. At least they need to agree on the content of the messages that they exchange. Yet, the latter alone does not mean that they will accomplish something useful. Hence, there is a need to ensure that they cooperate in a sound manner.

    In this project, the bachelor or master student will participate in the design and prototyping of the E-calculus and its type system as a library for a mainstream programming language, preferably Scala or Java to evaluate the practicality of the E-calculus and its type system. A performance evaluation for the library will be developed. The amount of work will be properly partitioned in relation to the degree (bachelor or master).

    The ideal student has taken a course or has prior industry or research experience in programming languages, event-driven programming, cooperative and publish-subscribe architectures. weiter

    Betreuer/in: Dr. Andi Bejleri

  • 26.10.2015

    A library for safe Concurrent, Distributed programming

    Bachelorarbeit, Masterarbeit

    The STG group at TU Darmstadt has formalised the calculus of structured interactions (CoSI) and the type theory of Essential Multiparty Session Types (EMST) to describe and statically validate safe and deadlock free interactions in concurrent, distributed systems. Multiparty session types is a well-established type theory that is highly attracting the attention of the programming language and software engineering communities.

    The CoSI and EMST aim to establish the foundations of session types and their transition to practice.

    In this project, the bachelor or master student will participate in the design and prototyping of CoSI and global types constructs, devising a library for a mainstream class-based language. The library must support constructs for structuring interactions: session initiation, external and internal choice, matching, and session channels, and the runtime environment that will deal with various characteristics of initiation.The student will use Scribble as a description language for our global types. Scribble is designed based on the ideas and typing strategy underlying the original MST. The amount of work will be properly partitioned in relation to the degree (bachelor or master).

    The ideal student has taken a course or has prior industry or research experience in programming languages and/or compilers. weiter

    Betreuer/in: Dr. Andi Bejleri

  • 24.09.2015

    A theorem prover plugin for Essential Multiparty Session Types

    The STG group at TU Darmstadt has formalised the calculus of structured interactions (CoSI) and the type theory of Essential Multiparty Session Types (EMST) to describe and statically validate safe and deadlock free interactions. Multiparty session types is a well-established type theory that is highly attracting the attention of the programming language and software engineering communities.

    The CoSI and EMST aim to establish the foundations of session types and their transition to practice. The fundamental properties of typed CoSI processes such as subject reduction, communication safety, and progress are established and proved.

    In this project, the bachelor or master student will participate in the design and prototyping of a plugin for a well-established theorem prover (preferably Isabelle or Coq) to assist the formal proofs of soundness for EMST. The plugin will consist in modelling the formal definition of CoSI and its type system in the preferable theorem prover. A test of the plugin will be developed, using the current proofs of soundness of Essential Multiparty Session Types.

    The ideal student has taken a course or has prior industry or research experience in interactive theorem provers (proof assistants) and formal proofs. weiter

    Betreuer/in: Dr. Andi Bejleri

  • 01.08.2015

    A dataflow-based programming model for Web applications

    Bachelorarbeit, Masterarbeit

    Betreuer/innen: Prof. Dr. Guido Salvaneschi, Prof. Dr.-Ing. Mira Mezini

  • 30.07.2015

    A debugging system for reactive programming.

    Bachelorarbeit, Masterarbeit

    Betreuer/innen: Prof. Dr. Guido Salvaneschi, Prof. Dr.-Ing. Mira Mezini

  • 30.07.2015

    Eclipse plugin for reactive programming.

    Bachelorarbeit, Masterarbeit

    Reactive programming is a recent programming paradigm that specifically supports the development of reactive applications. It provides dedicated language abstractions, like signals and events, that overcome the disadvantages of the traditional Observer pattern.

    Previous research on reactive programming has greatly improved the abstractions available to the developer. Other research areas focused on non-functional properties, like proving safety or time-bound execution of reactive applications.

    Interestingly, supporting reactive applications with dedicated tools and programming environments is a mostly unexplored area. However, the field is extremely promising, since reactive applications exhibit regular patterns that can be easily exploitable by the IDE. weiter

    Betreuer/innen: Prof. Dr. Guido Salvaneschi, Prof. Dr.-Ing. Mira Mezini

  • 30.07.2015

    Language integration of complex event processing

    Bachelorarbeit, Masterarbeit

    Betreuer/innen: Prof. Dr. Guido Salvaneschi, Prof. Dr.-Ing. Mira Mezini

  • 30.07.2015

    An empirical study on reactive programming.

    Bachelorarbeit, Masterarbeit

    Betreuer/innen: Prof. Dr.-Ing. Mira Mezini, Prof. Dr. Guido Salvaneschi

  • 26.03.2015

    Build-system migration to Pluto

    Bachelorarbeit, Masterarbeit

    Betreuer/innen: Dr. rer. nat. Sebastian Erdweg, Prof. Dr.-Ing. Mira Mezini

  • 17.11.2014

    Semi-automatic Verification of the Soundness of Type Systems.

    Bachelorarbeit, Masterarbeit

    Betreuer/innen: Prof. Dr.-Ing. Mira Mezini, Sylvia Grewe, M.Sc.

  • 21.05.2014

    Open Analyses Library

    Bachelorarbeit, Masterarbeit

    Betreuer/innen: Dr.-Ing. Michael Eichberg, Prof. Dr.-Ing. Mira Mezini

  • 03.02.2014

    Integrating Language Support for Geometric Algebra Computing into Scala

    Bachelorarbeit, Masterarbeit

    GA computing is a new way of geometrically intuitive computing. Based on the underlying Geometric Algebra (GA), it is very easy to compute with geometric objects such as spheres, planes and circles or to handle geometric operations and transformations. For example, the intersection of two spheres, which is a circle, can be simply expressed based on the outer product of the algebra. This technology leads to more compact algorithms for many engineering areas such as computer graphics, computer vision and robotics as well as for simulations, e.g. molecular dynamics simulation.

    The goal of this thesis is to build support for GA computing into Scala using SugarScala. SugarScala is a syntactically extensible variant of Scala where developers can introduce new language features through libraries. Using this technology, this thesis will design and integrate language constructs specific to GA computing. From here, there are two alternative directions:

    • Use lightweight modular staging to compile GA programs to highly-efficient code (the optimizations are well-known), and (time permitting) use Delite to run GA programs in parallel.
    • Design and implement a language on top of the SugarScala GA features that more easily allows experts from computer graphics, computer vision, robotics, or molecular dynamics to express GA programs.

    For further information contact Sebastian Erdweg. This thesis will be co-supervised by Dietmar Hildenbrand, expert in CA computing. weiter

    Betreuer/innen: Dr. rer. nat. Sebastian Erdweg, Prof. Dr.-Ing. Mira Mezini