Modellbasierte Entwicklung ist ein prominentes Paradigma im Bereich eingebetteter Systeme. Hierbei bilden Modelle des Zielsystems die Grundlage aus der die weiteren Bestandteile des Systems sukzessive abgeleitet werden. Häufig anzutreffen sind auf diese Weise entwickelte eingebettete Systeme in Steuerungs- und Regelungstechnik-lastigen Anwendungsbereichen wie Industrieautomation, Automobilindustrie, Luft- und Raumfahrt oder (mobiler) Rotobik. Eine wichtige Rolle spielen dann grafische Modelle der Dynamik der Systeme und der dazugehörigen Regelungen. Aus diesen Modellen können im Idealfall zugunsten von Effizienz, Fehlerreduzierung und Kostenersparnis automatisichert Quelltexte generiert werden. Diese Arbeit beschäftigt sich mit der grafischen Modellierung und der automatischen Generierung der Steuerungssoftware eines humanoiden Roboters im Zuge des FUB-KIT Projekts. Hierzu wurde die weit verbreitete Softwareumgebung MATLAB mit der eng verbundenen Modellierungs- und Simulationssoftware Simulink derart erweitert, dass die Funktionalittät von DYNAMIXEL Aktuatoren mit grafischen Bausteinen in Simulink verwendet werden kann.

Swarms are a known and studied phenomenon in biology. In different scientific fields transferring of the swarm ideas is done to solve specific problems. In computer science swarm approaches are applied from computer graphics till mobile robotics. The main contribution of this master thesis is to transfer swarm behaviour to the autonomous car context of the AutoNOMOS Project of the Freie Universität Berlin - A Swarm Behaviour for Path Planning.  Therefore a processing pipeline is developed, which generates a driving plan for the autonomous car from swarm based data. A detailed description of the different processing steps is given. The steps include the topics: 1) Swarm member selection, 2) velocity matching, 3) swarm member trajectory based path planning, 4) abstracting data from swarm member trajectories to generate clustered data, 5) cluster based path planning, and 6) plan smoothing with linear regression. Furthermore, the developed approach is evaluated and experimental results in simulation and live tests on the autonomous car MadeInGermany are provided.

The automated theorem prover Leo was one of the first systems able to prove theorems in higher-order logic. Since the first version of Leo many other systems emerged and outperformed  Leo and its successor Leo-II. The Leo-III project's aim is to develop a new pover reclaiming the lead in the area of higher-order theorem proving.

Current competitive theorem provers sequentially manipulate sets of formulas in a global loop to obtain a proof. Nowadays in almost every area in computer science, concurrent and parallel approaches are increasingly used. Although some research towards parallel theorem proving has been done and even some systems were implemented, most modern theorem provers do not use any form of parallelism.

In this thesis we present an architecture for Leo-III that use parallelism in its  very core. To this end an agent-based blackboard architecture is employed. Agents denote independent programs which can act on their own. In comparison to classical theorem prover archiectures, the global loop is broken down to a set of tasks that can be computed in parallel. The results produced by all agents will be stored in a blackboard, a globally shared datastructure, thus visible to all other agents. For  a proof of concept example agents are given demonstrating an agent-based approach can be used to implement a higher-order theorem prover.

Church's Simple Theory of Types (STT), also referred to as classical higher-order logik, is an elegant and expressive formal system built on top of the simply typed λ-calculus. Its mechanisms of explicit binding and quantification over arbitrary sets and functions allow the representation of complex mathematical concepts and formulae in a concise and unambiguous manner. Higher-order automated theorem proving (ATP) has recently made major progress and several sophisticated ATP systems for higher-order logic have been developed, including Satallax, Osabelle/HOL and LEO-II. Still, higher-order theorem proving is not as mature as its first-order counterpart, and robust implementation techniques for efficient data structures are scarce.

In this thesis, a higher-order term representation based upon the polymorphically typed  λ-calculus is presented. This term representation employs spine notation, explicit substitutions and perfect term sharing for efficient term traversal, fast β-normalization and reuse of already  constructed terms, respectively.  An evaluation  of the term representation is performed on the basis of a heterogeneous benchmark set. It shows that while the presented term data structure performs quite well in general, the normalization results indicate that a context dependent choice of reduction strategies is beneficial.

A term indexing data structure for  fast term retrieval based on various low-level criteria is presented and discussed. It supports symbol-based term retrieval, indexing of terms via structural properties, and subterm indexing.

The goal of this thesis is to present the first realtime honey bee waggle dance decoding system, and to establish a benchmark of detection rates and decoding quality. Honey bee research concerns a wide scientific community, but here are no automatic waggle dance detection and decoding systems in use. Hence the goal of this thesis is to create one.

This master's thesis first introduces the honey bee waggle dance communiction and motivates the need for an automatic decoding system. Then it examines related work and concludes that no such systems exist. First, I define the software requirements, then I present a detailed implementation. Finally, the presented algorithm is applied to video recordings and used in two experiment. Decoding quality is evaluated with precise video material. Detection results of six and four weeks live observations are evaluated. Decoder system's capability to reconstruct the location of a trained artificial food source is tested.

Evaluation results show that the realtime honey bee waggle dance decoding system can achieve 96.4% precision rate and 89.5% recall rate with recorded videos. The system shows 78.6% and 67.4% precision rates for live observations. On average decoded dance positions show 0mm error and a low standard deviation error. Waggle run duration decoding averagely exhibits an error of additional 97.79 ms and a standard deviation error of 138.52 ms. On average the decoding of honey bee dance directions shows -1.06° error and a standard deviation error of 35.83°. In the end I discuss different evaluation results and present further improvements for future works.

Autonomous vehicles of the future need maps with much more information than provided by the existing street maps. State of the art navigation systems already have digital maps, but they lack in detail, accuracy and assume a flat world. Based on the existing two dimensional map format RNDFGraph our autonomous car "MadeInGermany" has been using, this thesis shows the development process and application of a more detailed format covering the third dimension, the Advanced Road Network Definition Graph (ARNDGraph). Over 300 km of Berlin's road network were mapped and autonomously traveled. The experiments include runtime and file size comparisons between the RNDFGraph and the ARNDGraph.

With the growing interest to understand processes and functionn of the human brain, several interesting research projects have started all over the world. They try to take advantage of the increasing computing power to open new possibilities in neuroscience. Among them is The Virtual Brain (TBV), a neuroinformatics platform that simulates the dynamics of large-scale neural populations through computational models.

Despite a set of features that make TVB understandable for the user, it is still a complex siumlation tool. Specially, when considering users without deep knowledge in neuroscience and its computational principles. Therefore, in order to facilitate TVB's usability of the Graphical User Interface (GUI), an educational tool that helps the user to learn interactively, was required. In this thesis, I will present an add-on for The Virtual Brain called TVB-EduPack. It contains user-driven tutorials and adds a new feature that allows the creation of new tutorials by providing an easy-to-use scripting interface. Additionally, through a predefined and extendable set of user actions, it is possible for instance to use and display pre-computed simulation results.

This application is expected to improve significantly the manageability to the software of TVB. Specially, it can attract the attention of both, novice users interested in neurosciences as well as advanced researchers, who could make use of the tutorial authoring tool in order to publish and share their results with TVB's community.

In dieser Arbeit wird ein Algorithmus vorgestellt, der es ermöglicht, anhand des Optischen Flusses Kollisionen erkennen zu können. Sie ist eingebete in den Rahmen des Neurocopter-Projekts. Der Ansatz beruht auf dem Berechnen von durchschnittlichen Flüssen der in Teilbilder unterteilten Bildern. Diese Bilder werden von der an der Frontseite eines Quadrocopters angebrachten Kamera aufgenommen und von dem mitfliegenden Mini-PC verarbeitet. Die Einschätzung der Situationen erfolgt per Mustervergleich, mithilfe von multivarianten Normalverteilungen. Dabei wurden gute Ergebnisse erreicht, sofern sich die Bewegungen auf Translationen beschränken. Drehungen führen häufig zu falsch erkannten Kollisionen. Zudem führt der größere Winkel bei zunehmender Geschwindigkeit zu Problemen. Es gibt allerdings Möglichkeiten, diese Probleme zu lösen. Diese sollten in zukünftigen Arbeiten getestet werden.

Exploring other planetary sufaces with autonomous robots is a very complex task and requires a lot of research. To give an impulse, the DLR organized the first SpaceBot Cup in 2013. The team Berlin Rockets from the Freie Universität constructed a six-legged robot to take part in the competition. This thesis presents an approach for the stochastic estimation of an object's pose. The estimate will be used by the robot to grasp the object.  The estimation is done with a particle filter that uses depth and color data from the robot's Kinect for Windows^TM. The object models consist of 3D point that are evenly distribued over the object's surface. Additionally, a few specific pixels from the vicinity of the object are also taken into account to reduce the rate of false positives. To test the particle filter, several test cases were conducted. The accuracy of the results is unfortunately very low, which shows that the measures taken did not have the desired effect.

The Beesbook project's goal is to gather information of unprecedented detail about the processes in a beehive. During the planned experiments, due to a high temporal and image resolution, a big amount of image data will be acquired (up to 300 Terabyte). This thesis, firstly, presents an approach to live transfer the recorded image data to a specialized data storage facility in a stable and efficient way. For that purpose, it has been elaborated how to use a previously established Gigabit connection to capacity. Secondly, due to the image analysis taking an estimated time of 700 years on one processor, a parallelization of the anaylsis has been developed. The presented approach uses the newly built supercomputer's batch queue and submits processing jobs continuously. The resulting program is applicable to all perfectly parallel problems. In fact, it can be compared to the Map-step of the well-known MapReduce programming model, but in a supercomputer environment instead of a compute cluster.

Im Rahmen des "Carolo-Cup"-Wettbewerbs konstruieren studentische Teams autonome Modellfahrzeuge, die in einer Testumgebung mit aufgebrachten Straßenmarkierungsn verschiedene Aufgaben zu erfüllen haben. Die Arbeit beschreibt, wie die Pose (Position und Orientierung) eines solchen Modellfahrzeugs in einem globalen Koordinatensystem während der Fahrt verfolgt werden kann, um diese direkt zur Fahrplanung zu verwenden.

Weil die Odometriedaten des Modellautos sehr ungenau sind, muss die daraus errechnete erste Schätzung der Pose mittels weiterer Sensorik korrigiert werden. Dazu wird eine omnidirektionale Kamera verwendet, um die Fahrspurmarkierungen zu erkennen und mit einer Karte abzugleichen.

Die resultierende Lokalisierung ist genau genug, um beispielsweise einer vorgegebenen Fahrspur zu folgen, ohne die Spurbegrenzungen zu überschreiten. Weiterhin kann die Lokalisierung auch zur Navigation genutzt werden und ermöglicht somit perspektivisch den Einsatz des Modellfahrzeugs in Szenarien, deren Komplexität über die des Carolo-Cup hinausgeht.

In den letzten Jahren ist die Rekonstruktion von 3D-Modellen in eine Vielzahl von Bereichen vorgedrungen. So können z.B. die erstellten Modelle für Filme oder Videospiele verwendet werden. Weitere Anwendungen reichen von Fahrassistenzsystemen, die den Fahrer mit zusätzlichen Informationen versorgen, bis hin zu autonom handelnden Robotern. Auch in der Visualisierung von Daten finden sich 3D-Modelle wieder, so können werdende Eltern schon vor der Geburt (per Ultraschall) ihr Kind dreidimensional betrachten.

Der Anwendungsbereich von Karten ist groß. Exakte Karten sind aus der heutigen Gesellschaft kaum mehr wegzudenken. Dank genauer Karten ist es heutzutage möglich, Waren und Menschen von einer Hälfte der Erde auf die andere zu transportieren, komplexe Bauvorhaben zu meistern und die Welt massiv umzugestalten. Heutzutage unterstützen Orthophotos Menschen auf allen gängigen Online-Kartendiensten. Sie vermitteln den Eindruck der Umgebung genauer als eine traditionelle Karte. Sie können auch automatisch auf Karteninformationen hin durchsucht werden.

War es noch vor einigen Jahrzehnten undenkbar, dass Privatpersonen die Investitionsschwelle für Luftaufnahmen schultern können, ist es heutzutage, dank dem Einzug von Digitalkameras und Multicoptern, preiswerter und einfacher denn je. Um den Materialaufwand so minimal wie möglich zu halten und den Einsatz und die Kosten von Spezialkomponenten zu vermeiden, aber auch da es schlichtweg manchmal nicht möglich ist, eine genaue Position der Kamera zu messen (z.B. bei historischen Aufnahmen, Fehlfunktion der GPS Hardware), widmet sich diese Arbeit der Erstellung vor Orthophotos ausschließlich anhand von Bildmaterial. Hierfür wurden sogenannte Multicopter und handelsübliche Digitalkameras verwendet. Durch den Einsatz von Computer-Vision-Algorithmen sollen aus Bilddaten Aufsichten der Szenen produziert werden können.

Mit Hilfe von Prototypen wird versucht, Probleme, die Konzept, Gestaltung und Anwendung einer Schnittstelle mit sich bringen können, möglichst früh aufzudecken. Das Konzept des Paper-Based-Prototyping hat sich in der Softwareentwicklung durchgesetzt. seine Vorteile sind der Einsatz in frühsten Entwicklungsphasen und die Förderung der kreativen und diskussionsorientierten Arbeit. So können aus Prototypen-Testungen erlangte Erkenntnisse rechtzeitig berücksichtigt werden und kostspielige Anpassungsmaßnahmen vermieden werden.

Existierende Ansätze, die Papier als zentrales Element des Desingprozesses zu bewahren versuchen, müssen die Interaktionslogik des Prototyps implementieren. Dabei wird Papier zunehmend verdrängt durch recht komplexe Technologien, wie großflächige Touchscreens, finger-tracking Systeme oder digitale Stifte. Die Verbreitung solcher Technologien ist durch ihre hohen Anschaffungskosten deutlich erschwert.

Diese Arbeit liefert eine neue Methode, um kostspielige Technologien zu vermeiden und dennoch ein genaueres papier-basiertes Prototyping zu ermöglichen. Es werden Konzepte und Erkenntnisse aus der Augmented Reality Entwicklung benutzt, um einen paper-tracking Ansatz zu entwicklen. In diesem können mittels Webcam und ausgedruckter Marker User Interface Elemente definiert werden.  Die Darstellungstechniken der AR werden mit einer Grafik-Bibliothek gekoppelt, indem die Marker und die darauf  gerenderten 3D-Modelle den Elementen der Benutzer-Schnittstelle entsprechen und als 2D-Abbildungen festgehalten werden. Mit Hilfe der Grafik-Bibliothek kann der Zustand der AR dokumentiert also in Form einer Bilddatei gespeichert oder ausgedruckt werden.

Eine Evaluation der entwickelten Technik erfolgte im Rahmen dieser Arbeit. Die Ergebnisse haben eine gute User Acceptance (UA) der neuen Methode ergeben. Die Probanden haben die gestellten Aufgaben gut gelöst und zeigten sich begeistert von der neuen Idee für das Prototyping. Der Versuch, AR-Ansätze für das Prototyping nutzbar zu machen, wurde bisher nicht unternommen.

Das Modellieren von Köpfen ist ein schwieriges Problem in der Computergrafik. Das liegt nicht nur daran, dass der menschliche Kopf ein hoch komplexes Objekt ist. Auch die Leistung des Gehirns, "echte" Menschen von "unechten"  zu unterscheiden, trägt einen großen Anteil dazu bei.

Diese Masterarbeit präsentiert zwei Algorithmen, in denen aus zwei orthogonalen Bildern einer Person mit Hilfe eines Formmodells ein 3D-Kopf der Person rekonstruiert wird. In den Bildern werden manuell Merkmalspunkte extrahiert, die als Zielpunktwolke für bestimmte Vertices des Formmodells dienen. Es wird versucht, das Formmodell an die Zielpunktwolke anzupassen. Dafür wird ein Iterative Closest Point (ICP) Algorithmus verwendet.

Der Algorithmus verwendet keine Texturinformationen. Das unterscheidet ihn von bisherigen Ansätzen. Am Ende wird die Güte der Ergebnisse durch die Ähnlichkeit des Modells zu den Personen auf den Fotos bewertet.