Abschlussarbeiten

@mastersthesis{Petermann22,

title = {Comparison of Real-Time Plane Detection Algorithms on Intel RealSense},

author = {Lukas Petermann},

url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2023/01/BA_Petermann.pdf},

year  = {2022},

date = {2022-11-29},

urldate = {2022-11-29},

abstract = {Planar structures account for a significant portion of indoor man-made environments.

With advances in the field of Augmented Reality (AR), the automatic detection of planar

surfaces has become essential for recent AR applications. Often, these applications

operate under a strict temporal constriction, also referred to as real-time. Naturally, this

time restriction applies to the integrated plane detection algorithm as well. The technology

that provides real-time plane detection already exists. However, for different reasons,

these devices are often not suitable for the average consumer. This motivates the utilization

of consumer off-the-shelf hardware. Additionally, an appropriate plane detection

algorithm is needed. Decades of research yield a wide variety of different approaches.

As these methods are predominantly evaluated scientifically, the real-world applicability

poses an open question. Moreover, the inherent incomparability of most plane detection

algorithms renders a selection non-trivial.

This work evaluates the real-world applicability of real-time plane detection algorithms.

After considering current state-of-the-art plane detection algorithms, we select

four algorithms, namely RSPD, OPS, 3D-KHT, and OBRG. In a similar

approach, we select the 2D-3D-S dataset and compose the novel FIN dataset. We introduce

a definition of real-time and perform experiments on both datasets. Subsequently,

we compare the respective results. The results show that 3D-KHT is the only real-time

applicable plane detection algorithm in a realistic environment.},

keywords = {},

pubstate = {published},

tppubtype = {mastersthesis}

}

@mastersthesis{sambandham2022deep,

title = {Deep Learning based Harmonization and Super-Resolution of Landsat-8 and Sentinel-2 images},

author = {Venkatesh Thirugnana Sambandham},

url = {https://cse.ovgu.de/files/thesis/sambandham2022deep.pdf},

year  = {2022},

date = {2022-04-19},

school = {Otto-von-Guericke-Universit\"{a}t Magdeburg},

abstract = {Earth Observation using remotely sensed images from satellite sensors has been a fas-

cinating topic of study in recent days. Landsat-8 by NASA and sentinel-2 (A\&B) by ESA

are two very prominent multi-spectral imaging satellite projects that provide open-

source data. Images from these sensors are used in monitoring vegetation changes,

urban development, catastrophe management ,and many cutting-edge applications.

However, these multi-spectral imaging sensors work in the visible to the infrared

region of the Electro-Magnetic Spectrum which could not penetrate through clouds.

Since majority of the earth’s surface is consistently covered with clouds, images from

these sensors over a cloud-covered region cannot be used. The combined use of

multi-spectral images from multiple image sources is a viable option to increase the

temporal availability of cloud-free images. However, such an approach brings in

many uncertainties in the analysis due to the differences in the configurations of the

imaging sensors and spatial resolution. Several types of research are already done

on bringing down the differences. This thesis explores a possibility of using a Deep

Learning based pipeline that brings down the spectral differences between the two

image sources, and therby improving the spatial resolution of landsat-8 image.

The dataset for this work is created using the images from both sensors that were

taken on the same day over the study area. The proposed pipeline has a compre-

hensive preprocessing step, which also includes the development of a band-pass

adjustment function that reduces the spectral differences of the common bands be-

tween the two imaging sensors. The preprocessing inputs are then upsampled using a

Convolution Neural Network based super-resolution architecture. To train this archi-

tecture the high-resolution sentinel-2 images are used as ground truth, the landsat-8

images are then brought to the resolution of sentinel-2. The best architecture for this

pipeline is a UNet based super-resolution model that fuses the pan-chromatic band

of landsat-8 with the multi-spectral bands and thereby upsampling the multi-spectral

bands.

The proposed pipeline improves the spatial details of the landsat-8 image and around

5% improvement in the SSIM metrics is observed. A significant drop in the pixel-

to-pixel NRMSE metrics between the images was also observed. In addition to that

significant improvements in the correlation between the derived bands of Normalized

Difference Vegetation Index(NDVI) and Normalized Difference Water Index(NDWI)

are also observed. The robustness of the pipeline is demonstrated by performing a

use-case scenario of field observation over a period. All the tools, libraries ,and the

data that are used in this work are from open sources and the whole work is easily

reproducible.},

keywords = {},

pubstate = {published},

tppubtype = {mastersthesis}

}

@mastersthesis{rao2022active,

title = {Active Learning and Transfer Learning for the efficient Labelling and Semantic Segmentation in Aerial Imagery},

author = {Rajatha Nagaraja Rao},

url = {https://cse.ovgu.de/files/thesis/rao2022active.pdf},

year  = {2022},

date = {2022-03-15},

school = {Otto-von-Guericke-Universit\"{a}t Magdeburg},

abstract = {Deep learning (DL) models are capable of performing semantic segmentation

(SS) in aerial imagery that helps us detect the various semantic features such as

buildings, roads, woodlands, water bodies and so on for use in several applica-

tions such as that of social and economic analysis. Since DL models are data

hungry, data collection and ground truth generation are pivotal to training these

DL models in a supervised setting. However, the annotations of interest may not

be readily available and must be generated manually by annotating aerial images

that span hundreds of kilometers which proves to be impractical on account of

the extraordinarily high financial and temporal resources required.

This thesis work contributes towards minimizing the labelling effort by cir-

cumventing the manual labelling of the entire dataset through the use of both the

transfer learning (TL) and active learning (AL) techniques. In the TL approach,

an extensive research of available aerial datasets is done and DL models are

pre-trained with suitable open-source aerial image datasets of varying ground

sampling distances (GSD). The last layers of the models are then fine-tuned using

a considerably small number of manually annotated samples in the ObViewSly

dataset. The AL approach deals with label scarcity by iteratively selecting the

most informative samples from an enormous unlabelled data pool which would

help the model to learn better and to grow more confident in its predictions. We

have used the entropy-based query strategy to rank and retrieve these samples

for labelling which are then used for iteratively re-training the model. A novel

technique called the AL guided TL (TL+AL) for SS in aerial imagery is proposed

in this work that combines the effectiveness of both the AL and TL approaches.

TL re-uses the learned representations from the source dataset and AL carefully

selects important samples to be annotated such that we ensure both efficiency in

labelling and good model performance. Also, the Shuffle-Unet model is proposed

as a part of this work which employs phase shift in place of maxpooling and

upsampling operations.

The AL, TL and TL+AL were investigated here with the U-Net and the pro-

posed Shuffle-Unet models which were able to achieve an IoU score of 0.75 by

judiciously annotating only 10% of the dataset. Through the entropy heatmaps,

it was demonstrated that the samples that have regions covered by shadow are

difficult to learn for the model. Variable GSDs lead to domain shift between the

datasets used in TL. This domain shift is also addressed here wherein the trained

model is adapted to detect semantic features in the ObViewSly dataset that has a

lower GSD than that of the source dataset used for pre-training in TL. Hence, our

approach attained good segmentation performance while incurring significantly

low labelling costs.},

keywords = {},

pubstate = {published},

tppubtype = {mastersthesis}

}

@mastersthesis{prabhu2021synth,

title = {Synth2Real : 3D-Furniture Reconstruction in Ersatz Environment},

author = {Kartik Prabhu},

url = {https://cse.ovgu.de/files/thesis/kprabhu2021synth.pdf},

year  = {2021},

date = {2021-10-18},

school = {Otto-von-Guericke-Universit\"{a}t Magdeburg},

abstract = {The field of Deep Learning is growing exponentially and has tremendous applications

in many domains. The key for training deep learning models is a large dataset. The

real-world dataset is cost-ineffective, time-consuming, difficult to obtain, and are

very limited. Synthetic data are easier to create and automate. This thesis aims to

check if images created using game engines(Unity) are photorealistic and valuable in

3D reconstruction tasks using Deep Neural Networks. To achieve this, we contribute

the following: (a)A Unity-based application to create synthetic furniture images in

an ersatz indoor environment. (b)We use the new synthetic dataset as a benchmark

for the 3D reconstruction task. (c)A comprehensive study on domain adaptation and

domain randomization.

We conducted a user survey with the proposed synthetic dataset, a real dataset,

and seven other proclaimed photorealistic synthetic datasets to check the photore-

alism. We see that the proposed dataset failed to highlight itself as a standalone

photorealistic dataset but faired against other automated datasets. We compare the

performance of baseline models with transfer learning and mixed training to check

the influence of the synthetic dataset. We check domain randomization by creating a

synthetic chair dataset with diferent parameters like light, textures, camera posi-

tion, etc. The domain gap between real and synthetic datasets is visualized using

t-Distributed Stochastic Neighbor Embedding (t-SNE) and quantitatively measured

with the Fr\'{e}chet Inception Distance (FID) score. Finally, these experimental results

demonstrate that the proposed dataset enhances the performances of Deep Neural

Net models for the 3D reconstruction task.},

keywords = {},

pubstate = {published},

tppubtype = {mastersthesis}

}

@mastersthesis{K\"{u}hne2020,

title = {Automated Collision-free Tasksequencing for Industrial Robots},

author = {Maximilian K\"{u}hne},

url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2021/02/MA_MaximilianKuehne.pdf},

year  = {2020},

date = {2020-11-18},

school = {Otto-von-Guericke-University Magdeburg},

abstract = {Die in der Industrie eingesetzten Robotermanipulatoren bieten meist durch die Anzahl ihrer Gelenke gewisse Freiheitsgrade, was ihnen die M\"{o}glichkeit gibt jeden beliebigen Punkt in ihrem Arbeitsraum zu erreichen. Dabei k\"{o}nnen sie sogar Punkte hinter Hindernissen anfahren. Ist ein Arbeitsraum jedoch frei von solchen Hindernissen, kann es f\"{u}r einen Punkt viele verschiedene Stellungen (Konfigurationen) f\"{u}r den Manipulator geben. Betrachtet man die Aufgabe, die vom Roboter an einem Werkst\"{u}ck vollzogen werden soll, ergibt sich daraus meist eine zus\"{a}tzlicher Freiheitsgrad. Daraus folgt eine gro\sse Menge an m\"{o}glichen L\"{o}sungen. Das f\"{u}hrt dazu, dass f\"{u}r eine automatisierte Optimierung der Aufgabenplanung, eine enorme Berechnungszeit entstehen kann. Will man bei dieser Optimierung noch darauf achten, dass der Roboter nicht mit sich selbst bzw. mit dem Werkst\"{u}ck oder anderen Objekten kollidiert, steigert das nochmals den ben\"{o}tigten Zeitaufwand. Deshalb wird in den meisten F\"{a}llen der Suchraum vereinfacht und die Kollisions\"{u}berpr\"{u}fung wird erst am Ende durchgef\"{u}hrt.

In dieser Masterarbeit soll eine Sequenzoptimierung rein im Konfigurationsraum des Roboters durchgef\"{u}hrt werden. Dabei sollen sich alle Pfade offline und kollisionsfrei mit Hilfe von zufallsbasierten Pfadplanern wie RRT bestimmen lassen. Die auftretenden Probleme hinsichtlich der Berechnungszeiten sollen mit Hilfe einer Parallelisierung verringert werden. Aus dieser Vorgehensweise ergeben sich

folgende Fragen:

(i) Wie l\"{a}sst sich eine Parallelisierung integrieren?

(ii) Welchen Einfluss hat die Form des Werkst\"{u}cks auf die Optimierung?

(iii) L\"{a}sst sich die Planung der Bearbeitung eines Werkst\"{u}cks automatisiert besser umsetzen als eine Planung durch den Menschen?},

keywords = {},

pubstate = {published},

tppubtype = {mastersthesis}

}

@mastersthesis{Klockmann2020,

title = {MWMA-SLAM: Manhattan-World-Multi-Agent-SLAM},

author = {Maximilian Klockmann},

url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2020/10/ma_klockmann-1.pdf},

year  = {2020},

date = {2020-10-20},

school = {Otto-von-Guericke-University Magdeburg},

abstract = {Einsatzkr\"{a}fte m\"{u}ssen sich regelm\"{a}\ssig zur Rettung von Opfern in unbekannten Umgebungen zurechtfinden. Dabei liegen nur selten Karten vor. Die Einsatzleitung muss die einzelnen Teams mittels Funk koordinieren und kann die Positionen nur absch\"{a}tzen. Um die Einsatzkr\"{a}fte zu unterst\"{u}tzen, k\"{o}nnen Multi-Agent-SLAM Algorithmen eingesetzt werden. Diese m\"{u}ssen jedoch datensparsam sein, um mit den Netzwerk-Bedingungen vor Ort zu funktionieren. Oftmals muss das Netzwerk selbst aufgespannt werden. 

F\"{u}r die Kartographierung vor Ort gibt es eine Vielzahl an verschiedenen Multi-Agent- SLAM-Algorithmen. Diese arbeiten \"{u}blicherweise mit RGBD-Bildern oder Punktwolken. Die berechneten Rotationen erreichen dabei eine hohe Genauigkeit mit weniger als 1,9 Grad Abweichung. In einigen SLAM-Algorithmen werden Ebenen als Eingabe verwendet [35, 8]. Diese Algorithmen arbeiten jedoch nur lokal und wurden nicht als Multi-Agent-SLAM entwickelt.

Ebenen haben durch ihre einfache, mathematische Darstellung ein hohes Potenzial, um Daten einzusparen. In der Koordinatenform m\"{u}ssen nur eine Normale und die Distanz zum Ursprung, also vier Dezimalzahlen, \"{u}bertragen werden. In dieser Arbeit wird untersucht, ob sich Ebenen auch f\"{u}r einen Multi-Agent-SLAM eignen. Es wurde der auf Ebenen basierende MWMA-SLAM konzipiert. Die lokalen Karten werden daf\"{u}r in Form von Ebenen \"{u}bertragen und auf dem Server miteinander gematcht. Untersucht wird neben der Tauglichkeit der Ebenen auch die ben\"{o}tigte Datenmenge f\"{u}r die \"{U}bertragung. 

Der Algorithmus wurde sowohl mit synthetischen als auch mit realen Daten getestet. Es wurde in den Tests gezeigt, dass die Verwendung von Ebenen funktioniert. In jeweils \"{u}ber 97% der F\"{a}lle konnte eine gute Rotation mit weniger als 0.2_ Abweichung berechnet werden. Eine gute Translation mit weniger als 1 mm Abweichung konnte in durchschnittlich 90% der F\"{a}lle berechnet werden. Der MAE der Rotation liegt bei 0,6 Grad.

Insgesamt hat sich gezeigt, dass das Konzept eines Ebenen basierten Multi-Agent-SLAMs funktioniert. Die Ergebnisse zeigen eine \"{a}hnlich gute Genauigkeit bei der Rotation wie andere Multi-Agent-SLAM-Algorithmen. F\"{u}r die Translation m\"{u}ssen jedoch noch Anpassungen in der Berechnung vorgenommen werden, um die Ergebnisse zu verbessern. Mit einer Gr\"{o}\sse von maximal 576 Byte f\"{u}r die \"{U}bertragung der einzelnen Testumgebungen, konnte.},

keywords = {},

pubstate = {published},

tppubtype = {mastersthesis}

}

@mastersthesis{Kirchheim2019,

title = {Self-Assessment of Visual Recognition Systems based on Attribution},

author = {Konstantin Kirchheim},

url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2020/01/MA_2019_KonstantinKirchheim.pdf},

year  = {2020},

date = {2020-03-01},

urldate = {2019-12-09},

school = {Otto-von-Guericke-University Magdeburg},

abstract = {Convolutional Neural Networks achieve state of the art results in various visual recognition  tasks like object  classification and  object detection.   While CNNs perform surprisingly well, it is difficult to retrace why they arrive at a certain prediction.  Additionally, they have been shown to be prone to certain errors. As CNN are increasingly deployed into physical systems - for example in self driving vehicles - undetected errors could result in catastrophic consequences. Approaches to prevent this include the usage of attribution based explanation methods to facilitate an understanding in the systems decision in hindsight, as well  as  the  detection  of  recognition  errors  at  runtime,  called  self-assessment. Some state-of-the-art self-assessment approaches aim to detect anomalies in the activation patterns of neurons in a CNN. 

This  work  explores  the  usage  of  attribution  based  explanations  for  self-assessment  of  CNNs.   We  build  multiple  self-assessment  models  and  evaluate their performance in various settings.  In our experiments, we find that, while self-assessment based on attribution does not outperform self-assessment based on  neural  activity  on  its  own,  it  always  surpasses  random  guessing.   Furthermore,  we find that self-assessment models using neural activation patterns as well as neural attribution can in some cases outperform models which do not consider attribution patterns.  Thus, we conclude that it might be possible to improve self-assessment models by including the explanation of the model into the assessment process.},

keywords = {},

pubstate = {published},

tppubtype = {mastersthesis}

}

@mastersthesis{SchottExtractionBA2018,

title = {Extraktion relevanter API-spezifischer Informationen zur automatischen Korrektur von Softwarefehlern},

author = {Kevin Michael Schott},

editor = {Sebastian Nielebock and Frank Ortmeier},

year  = {2018},

date = {2018-03-13},

school = {Otto-von-Guericke-Unviersit\"{a}t Magdeburg},

abstract = {Bekanntlich ist Softwareentwicklung nicht fehlerfrei. W\"{a}hrend der Fokus auf der Entwicklung neuer Komponenten liegen sollte, geht viel Zeit in die Behebung existierender Programmfehler verloren. Jene Programmfehler, welche das Softwaresystem in einen regressiven Zustand versetzen - sodass dieses nicht mehr ordnungsgem\"{a}\ss funktioniert - sind oftmals m\"{u}hselig zu beheben. Dadurch ist der zust\"{a}ndige Programmierer meist auf unbestimmte Zeit verpflichtet, diesen zu beheben, wodurch er dem Unternehmen nicht f\"{u}r die Weiterentwicklung zur Verf\"{u}gung steht. Dieser zeitliche Engpass kann monet\"{a}re R\"{u}ckschl\"{a}ge bedeuten, insbesondere wenn es sich um eine sicherheitskritische L\"{u}cke im Softwaresystem handelt. Die Dom\"{a}ne der automatischen Fehlerkorrektur will solchen Problemen entgegenwirken, indem versucht wird, ein Ansatz zu finden, der den entstandenen Fehler automatisch beheben kann oder dem Programmierer wenigstens einen L\"{o}sungsvorschlag liefert.

Heutzutage ist der Umgang mit Application-Programming-Interfaces (kurz APIs) beinahe allt\"{a}glich f\"{u}r jeden Programmierer, was einen Ansatz zur automatischen Korrektur von Softwarefehlern schwer bis gar nicht generalisieren l\"{a}sst. Deren Dokumentation ist oft nicht hinreichend oder unverst\"{a}ndlich. Dadurch wird die API falsch benutzt, sodass unter anderem Methodenaufrufe vergessen oder in falscher

Reihenfolge verwendet werden. J\"{u}ngste Studien zeigen zudem, dass bei circa jeder zweiten Fehlerbehebung mindestens eine API-spezifische \"{A}nderung vorgenommen werden muss, um den Fehler ganzheitlich zu beheben. Herk\"{o}mmliche Ans\"{a}tze zur automatischen Korrektur von Softwarefehlern k\"{o}nnen aufgrund ihrer generischen Natur diese Programmfehler oftmals nicht vollst\"{a}ndig beheben und m\"{u}ssen erweitert werden. Im Rahmen dieser Arbeit wird ein Konzept vorgestellt, mit dessen Hilfe diese Programmfehler m\"{o}glicherweise korrigiert werden k\"{o}nnen. Prim\"{a}r wird jedoch erforscht, welche Informationen aus einem API-spezifischen Kontext extrahiert und verarbeitet werden m\"{u}ssen, um eine Korrektur vornehmen zu k\"{o}nnen. Daf\"{u}r wird ein Prototyp entwickelt, der diese Informationsextraktion \"{u}bernimmt und \"{a}hnlichen Quellcode herunterl\"{a}dt, sodass in diesem potenziell eine richtige Benutzung der gesuchten API enthalten ist, welche als Korrektur des Fehlers dienen soll.},

keywords = {},

pubstate = {published},

tppubtype = {mastersthesis}

}

@mastersthesis{Veera2017,

title = {Multi-Objective Issue Tracking Framework},

author = {Balaji Satya Pradeep Veera},

editor = {Sebastian Nielebock and Frank Ortmeier},

year  = {2017},

date = {2017-07-28},

school = {Otto-von-Guericke-Unviersit\"{a}t Magdeburg},

abstract = {Assigning an issue reports to individual developers is typically a manual, time-consuming and tedious task for the triager. Many automated issue tracking systems have been proposed over the time to choose an optimal developer for an issue report. These Single-Objective approaches try to find a developer who has fixed similar issue reports in the past. Thus they find an optimal developer for an issue report. While choosing an optimal developer, the Single-Objective approaches don’t consider the severity of

the issue report and the workload of the developer. The assigned issue report might reassign to another developer if the first assigned developer is busy with other issue reports. To solve this problem, we propose a framework of automated issue tracking system called Multi-Objective Issue Tracking Framework (MOITF). MOITF considers the workload of the developer along with the severity of the issue report while choosing the developer. This approach analyzes the history of previously closed issue reports for making predictions to the new issue report. The problem of selecting a developer who has fixed similar issue reports in the past and had less workload is viewed as a Multi objective problem. The traditional non-dominated sorting algorithm is used to find non-dominated devel-

opers who have knowledge about the problem mentioned in the issue report and also have time to fix the issue report.},

keywords = {},

pubstate = {published},

tppubtype = {mastersthesis}

}

@mastersthesis{eiserlohJSearchRepair2017,

title = {Semantische Suche f\"{u}r automatische Fehlerkorrekturen im objektorientierten Paradigma},

author = {Matthias Eiserloh},

editor = {Sebastian Nielebock and Frank Ortmeier},

url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/07/BA_2017_EiserlohMatthias-1.pdf},

year  = {2017},

date = {2017-07-03},

school = {Otto-von-Guericke Universit\"{a}t Magdeburg},

type = {Bachelor Thesis},

keywords = {},

pubstate = {published},

tppubtype = {mastersthesis}

}

@mastersthesis{Bedau2017,

title = {Modellbasierte Sicherheitsanalyse eines Bahnhofsstellwerks},

author = {Ludwig Bedau},

editor = {Otto-von-Guericke-Universit\"{a}t Magdeburg},

url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2018/02/BA_2017_BedauLudwig.pdf},

year  = {2017},

date = {2017-03-31},

school = {Otto-von-Guericke-Universit\"{a}t Magdeburg},

abstract = {Stellwerke stellen eine zentrale Komponente fu¨r den sicheren Schienenverkehr dar. Um die korrekte Funktionsweise sicherzustellen und sicherheitskritische Zust¨ande auszuschlie\ssen, sind formale Methoden angebracht.

In dieser Arbeit soll gezeigt werden, wie in der Modellierungssprache SAML (Sys-tem Analaysis and Modeling Language) ein Baukastensystem erstellt wird, mit dem sich beliebige Stellwerke modellieren lassen. In Rahmen der Arbeit wird beschrie-ben, wie das reale System abstrahiert wurde, um das zu untersuchende Verhal-ten herauszustellen. Die Arbeit beschreibt weiterhin die Sicherheits- und Liveness-Spezifikationen, die zur Verifikation der generierten Bahnhofsstellwerke genutz wer-den. Im Anschluss wird an einem Beispiel die Modellierung eines Bahnhofsstellwerkes auf Basis des vorgestellten Baukastensystems gezeigt. Bei der Verifikation wurde ei-ne kleine Auswahl an Model-Checking-Tools genutzt. Ein Vergleich dieser Tools in Bezug auf das hier gestellte Problem sowie eine Auswertung der Erfahrungen, die w¨ahrend des Projektes gesammelt werden konnten, sollen den Abschluss bilden.},

keywords = {},

pubstate = {published},

tppubtype = {mastersthesis}

}

@mastersthesis{Wehmeier2017,

title = {Konzeption einer Architektur f\"{u}r (Big-)Data-Analysen im Industrie 4.0-Kontext},

author = {Leon Wehmeier},

editor = {Otto-von-Guericke-Universit\"{a}t Magdeburg},

year  = {2017},

date = {2017-01-30},

address = {Otto-von-Guericke-Universit\"{a}t Magdeburg},

keywords = {},

pubstate = {published},

tppubtype = {mastersthesis}

}

@mastersthesis{krolikowski2016,

title = {Einfluss unterschiedlicher Kommentararten auf die Lesbarkeit des Quellcodes},

author = {Dariusz Krolikowski},

editor = {Sebastian Nielebock and Frank Ortmeier},

url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2016/11/masterarbeit-krolikowski-1.pdf},

year  = {2016},

date = {2016-08-19},

school = {Otto-von-Guericke Universit\"{a}t Magdeburg},

keywords = {},

pubstate = {published},

tppubtype = {mastersthesis}

}

@mastersthesis{Anders2016,

title = {Indoor-Positionsbestimmung mit Hilfe von Bluetooth-Low-Energy-Beacons und Pedestrian Dead Reckoning},

author = {Anton Anders},

url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2016/08/BA_Anton_Anders.pdf},

year  = {2016},

date = {2016-03-29},

school = {Otto-von-Guericke-Universit\"{a}t Magdeburg},

type = {Bachelorarbeit},

keywords = {},

pubstate = {published},

tppubtype = {mastersthesis}

}

@mastersthesis{Klockmann2016,

title = {Analyse von Crowd-Simulation Algorithmen beim Durchqueren von Engstellen},

author = {Maximilian Klockmann},

url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2016/08/BA_Max_Klockmann.pdf},

year  = {2016},

date = {2016-03-09},

school = {Otto-von-Guericke-Universit\"{a}t Magdeburg},

type = {Bachelorarbeit},

keywords = {},

pubstate = {published},

tppubtype = {mastersthesis}

}

@mastersthesis{Bahl2015,

title = {Konzepte zur Optimierung des Betriebshofmanagements mit pervasiven Assistenzsystemen},

author = {Benedikt Bahl},

url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2016/08/MA_Benedikt_Bahl.pdf},

year  = {2015},

date = {2015-12-15},

school = {Otto-von-Guericke-Universit\"{a}t Magdeburg},

type = {Masterarbeit},

keywords = {},

pubstate = {published},

tppubtype = {mastersthesis}

}

@mastersthesis{BAHamann2015,

title = {Kopplung formaler Modelle mit realweltlichen Umgebungsmodellen},

author = {Dominik Hamannn},

editor = {Otto-von-Guericke-Universit\"{a}t Magdeburg},

url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/12/BAHamann2015.pdf},

year  = {2015},

date = {2015-12-14},

address = {Universit\"{a}tsplatz 2, 39106 Magdeburg},

school = {Otto-von-Guericke-Universit\"{a}t Magdeburg},

abstract = {Sicherheitskritische technische Systeme werden insbesondere in der Automobilindustrie und der Luftfahrt immer komplexer. Ein Ansatz, um die Sicherheit solcher Systeme zu \"{u}berpr\"{u}fen, besteht darin, ein Modell des Systems zu erstellen und dieses von einem Model Checker auf gef\"{a}hrdende Situationen zu \"{u}berpr\"{u}fen. Die Umgebung eines softwareintensiven Systems muss oft, aufgrund der Funktionsweise von Model Checkern und aufgrund von Restriktionen der verwendeten Sprache, mit einem hohen Abstraktionsgrad modelliert werden. Das betrift insbesondere Systeme, die nicht nur rein logische Aufgaben ausf\"{u}hren, sondern mittels Sensorik und Aktorik mit der realen Welt interagieren. Herrscht eine zu gro\sse Diskrepanz zwischen der realen Umgebung und dem Modell der Umgebung, tritt in dem Modell Fehlverhalten nicht auf, dass in der realen Welt auftreten w\"{u}rde. Die Ergebnisse eines Model Checkers sind dann f\"{u}r dieses Modell nicht aussagekr\"{a}ftig.



In dieser Arbeit wird eine Schnittstelle vorgestellt, mit der formale Modelle mit realweltlichen Umgebungsmodellen gekoppelt werden k\"{o}nnen. Dadurch wird getestet, inwiefern sich das Verhalten des formalen Modells in einer realistischen Umgebung von dem Verhalten einer abstrahierten Umgebung unterscheidet. Dieser Vergleich kann Aufschluss \"{u}ber die Validit\"{a}t des verwendeten Umgebungsmodells bringen.},

howpublished = {Bachelorarbeit},

keywords = {},

pubstate = {published},

tppubtype = {mastersthesis}

}

@mastersthesis{Heum\"{u}ller2015,

title = {Multi-Abstraction Model Based Software Development for Embedded Low-Cost Applications},

author = {Robert Heum\"{u}ller},

url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/01/thesis-1.pdf},

year  = {2015},

date = {2015-11-06},

keywords = {},

pubstate = {published},

tppubtype = {mastersthesis}

}

@mastersthesis{BA-Orth,

title = {Trace refinement with reduced interpolant automata for binary programs},

author = {Severin Orth},

url = {https://cse.cs.ovgu.de/cse/?attachment_id=1937},

year  = {2015},

date = {2015-09-14},

school = {Otto-von-Guericke-Universit\"{a}t Magdeburg},

keywords = {},

pubstate = {published},

tppubtype = {mastersthesis}

}

@mastersthesis{Huehne15,

title = {Innenraumlokalisierung von Mobilger\"{a}ten mittels Bluetooth LE},

author = {Patrick H\"{u}hne},

url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2016/08/BA_Patrick_H\"{u}hne.pdf},

year  = {2015},

date = {2015-06-22},

school = {Otto-von-Guericke-Universit\"{a}t Magdeburg},

type = {Bachelorarbeit},

keywords = {},

pubstate = {published},

tppubtype = {mastersthesis}

}

@mastersthesis{BARabeler2015,

title = {Abstraktion kontinuierlichen Verhaltens zur modellbasierten Sicherheitsanalyse},

author = {Ben Rabeler},

editor = {Otto-von-Guericke-Universit\"{a}t Magdeburg},

url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/06/ba_thesis_rabeler.pdf},

year  = {2015},

date = {2015-05-18},

abstract = {Die Sicherheit von technischen System ist in vielen Gebieten wie der Luftfahrt oder im Stra\ssenverkehr von elementarer Bedeutung f\"{u}r die Hersteller solcher Systeme wie f\"{u}r die Anwender. Ein Ansatz um die Sicherheit von diskreten Systemen zu zeigen, besteht darin, diese in einem diskreten Modell zu abstrahieren und anschlie\ssend mit einem Model Checker auf gef\"{a}hrdende Situationen zu \"{u}berpr\"{u}fen. Viele Szenarien in den Anwendungsbereichen wie der Luftfahrt oder dem Stra\ssenverkehr beruhen jedoch auf kontinuierlichem Systemverhalten. 

In dieser Arbeit wird ein Verfahren vorgestellt, das ein kontinuierliches System in diskrete Automaten abstrahiert, sodass diese Automaten mit einem symbolischen Model Checker auf eine Sicherheitsspezifikation \"{u}berpr\"{u}ft werden k\"{o}nnen. Das Verfahren wurde in Umgebung, in der diskrete Modelle erstellt und \"{u}berpr\"{u}ft werden

k\"{o}nnen, als Prototyp umgesetzt. Dieser dient dazu anhand von Experimenten Eigenschaften des Verfahrens herauszufinden.},

keywords = {},

pubstate = {published},

tppubtype = {mastersthesis}

}

@mastersthesis{Doerfler2015,

title = {Protokollautomat f\"{u}r die Kommunikation zwischen Ladestation und Elektrofahrzeug},

author = {Stephan D\"{o}rfler},

url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/05/thesis_doerfler_2015.pdf},

year  = {2015},

date = {2015-04-09},

school = {Otto-von-Guericke-Universit\"{a}t Magdeburg},

type = {Bachelorarbeit},

keywords = {},

pubstate = {published},

tppubtype = {mastersthesis}

}

@mastersthesis{Gonschorek2015,

title = {A Backward Model Checking Approach with Slicing},

author = {Tim Gonschorek},

editor = {Tim Gonschorek

},

year  = {2015},

date = {2015-02-25},

address = {Universit\"{a}tsplatz 2, 39106 Magdeburg},

school = {Otto-von-Guericke-University Magdeburg},

abstract = {As software intensive safety critical systems are more and more introduced in our daily lives, it must be ensured that those systems safe. One method for ensuring that a

system follows its given specication, i.e., does not have some unwanted behavior, is

model checking. Although, nowadays larger models can be veried, model checking

algorithms does not perform well in combination with complex real world problems.

To overcome this diculties, this thesis proposes a new backward model checking algorithm

using SMT programs instead of boolean encodings for representing the systems

state. Additionally, it uses model based slicing to reduce the impact of the complexity

of a given model. This thesis explains such an algorithm, which can be used for verifying

safety properties. Further, this thesis presents a prototypical implementation of

this algorithm. This prototype will be used to evaluate the algorithm in comparison to

the BDD and the IC3 algorithms implemented in the model checker nuXmv. The evaluation

shows that there are some cases where the proposed approach performs better

than the given BDD algorithm.},

keywords = {},

pubstate = {published},

tppubtype = {mastersthesis}

}

@mastersthesis{Plauschin2014,

title = {Klassifikation latenter Fingerspuren mithilfe von Smartphones},

author = {Mathias Plauschin},

url = {https://cse.cs.ovgu.de/cse/wp-content/uploads/2015/03/thesis_plauschin_2014.pdf},

year  = {2014},

date = {2014-11-30},

keywords = {},

pubstate = {published},

tppubtype = {mastersthesis}

}

@mastersthesis{Fritsch2014,

title = {Erh\"{o}hung von Quellcode-Wartbarkeit durch Entwurfsmusterautomatisierung},

author = {Michael Fritsch},

editor = {Sebastian Nielebock and Frank Ortmeier},

url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/04/MA_Fritsch1.pdf},

year  = {2014},

date = {2014-11-14},

keywords = {},

pubstate = {published},

tppubtype = {mastersthesis}

}

@mastersthesis{Dietze2014,

title = {Semantische Verikation von selbstbeschreibenden Geratekonfigurationen},

author = {Denis Dietze},

url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/03/thesis_dietze_2014.pdf},

year  = {2014},

date = {2014-09-30},

keywords = {},

pubstate = {published},

tppubtype = {mastersthesis}

}

@mastersthesis{Dittmann2014,

title = {Visualisierungskomponente f\"{u}r ein Hochspannungs-Gleichstrom-\"{U}bertragungs-Netz \"{U}berwachungssystem},

author = {Denny Dittmann},

url = {https://cse.cs.ovgu.de/cse/wp-content/uploads/2015/03/thesis_dittmann_2014.pdf},

year  = {2014},

date = {2014-09-30},

keywords = {},

pubstate = {published},

tppubtype = {mastersthesis}

}

@mastersthesis{thesis-jagla-2014,

title = {Cross-Platform Remote Control of Web-Based Media},

author = {Tim Benedict Jagla},

url = {https://cse.cs.ovgu.de/cse/wp-content/uploads/2015/03/thesis-jagla-2014.pdf},

year  = {2014},

date = {2014-06-19},

abstract = {A multitude of network and media related topics will be discussed in this work. From the basics of networking and different web communication techniques as well as media preparation and provision a concept will be derived to solve the problem of the general lack in web standard compliant browsers

for mobile devices within the domain of web applications. A prototypical implementation will be presented and critically examined.},

keywords = {},

pubstate = {published},

tppubtype = {mastersthesis}

}

@mastersthesis{thesis-heumueller-2014,

title = {VECS Dataflow - A SAML Language Extension Allowing Intuitive Creation of Formal Automata Specifications},

author = {Robert Heum\"{u}ller},

url = {https://cse.cs.ovgu.de/cse/wp-content/uploads/2015/03/thesis.pdf},

year  = {2014},

date = {2014-04-10},

type = {Bachelor's Thesis},

keywords = {},

pubstate = {published},

tppubtype = {mastersthesis}

}

@mastersthesis{thesis-nielebock-2013,

title = {Komposition gew\"{o}hnlicher Differentialgleichungen mit sicherheitsrelevanten Zustandsautomaten},

author = {Sebastian Nielebock},

url = {https://cse.cs.ovgu.de/cse/wp-content/uploads/2015/03/MA_Nielebock_final_version.pdf},

year  = {2013},

date = {2013-09-17},

keywords = {},

pubstate = {published},

tppubtype = {mastersthesis}

}

@mastersthesis{Gonschorek2013,

title = {Methodik zur Abstraktion kontinuierlicher Differentialgleichungen},

author = {Tim Gonschorek},

editor = {Tim Gonschorek},

url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/BA_2013_Gonschorek.pdf},

year  = {2013},

date = {2013-06-19},

address = {Universit\"{a}tsplatz 2, 39106 Magdeburg},

school = {Otto-von-Guericke-University Magdeburg},

abstract = {Reale Phanomene aus Natur und Technik konnen oft nur durch kontinuierliche Modelle

abgebildet werden. Mithilfe eines Modelchecker konnen Modelle auf Grundlage

einer vorgegebenen Spezikation automatisiert veriziert werden. Jedoch konnen

die meisten Modelchecker nur mit diskreten Modellen umgehen. Deshalb kann ein

kontinuierliches Modell nicht direkt mit einem Modelchecker gepruft werden. Diese

Arbeit prasentiert eine Methodik, mit der es moglich ist, kontinuierliche Modelle

sowohl im Zeitbereich, als auch im Wertebereich zu diskretisieren. Das Modell wird

dazu in einen endlichen, diskreten Zustandsautomaten umgewandelt. Es wird ein

konkretes Vorgehen erklart, um kontinuierliche Dierentialgleichungen in Dierenzengleichungen

umzuwandeln, die in Zustandsubergangen eingebunden werden konnen.

Dadurch wird es moglich, die Vorteile eins Modelcheckers fur die Verikation

kontinuierlicher Modelle zu nutzen. Um sicherzustellen, dass der erstellte Automat

das kontinuierliche Modell hinreichend abstrahiert, um mithilfe eines Modelcheckers

Aussagen treen zu konnen, wird die Methodik anhand eines Beispielmodells evaluiert.

Um die praktische Anwendbarkeit zu zeigen, wird ein komplexe Fallstudie von

einem Modelica-Modell in einen SAML-Automaten transformiert. DesWeiteren wird

die Architektur einer Java-Komponente vorgestellt, mit der eine Modelica-Datei in

eine SAML-Datei transformiert werden kann, um sie mithilfe eines Modelcheckers

gegen eine vorgegebene Spezikation zu verizieren. Diese Komponente soll als erste

Implementation eines Importers fur Modelica-Dateien in eine SAML Umgebung

dienen.},

keywords = {},

pubstate = {published},

tppubtype = {mastersthesis}

}

@mastersthesis{thesis-struck-2011,

title = {Approaches to Multi-Objective Optimization of Formal Specifications},

author = {Simon Struck},

url = {https://cse.cs.ovgu.de/cse/wp-content/uploads/2015/03/masterarbeit-struck.pdf},

year  = {2012},

date = {2012-01-17},

keywords = {},

pubstate = {published},

tppubtype = {mastersthesis}

}

@mastersthesis{thesis-lipaczewski-2011,

title = {Untersuchung von Prefetching-Strategien in Objekt-relationalen Mappern},

author = {Michael Lipaczewski},

url = {https://cse.cs.ovgu.de/cse/wp-content/uploads/2015/03/thesis-lipaczewski-2011.pdf},

year  = {2011},

date = {2011-04-03},

keywords = {},

pubstate = {published},

tppubtype = {mastersthesis}

}