Kaiserslautern - Fachbereich Informatik
Refine
Year of publication
- 2013 (18) (remove)
Document Type
- Doctoral Thesis (11)
- Preprint (4)
- Conference Proceeding (1)
- Habilitation (1)
- Master's Thesis (1)
Has Fulltext
- yes (18)
Keywords
- Chromium Browser (1)
- DFG (1)
- DPN (1)
- ECMAScript (1)
- Empfehlungssysteme (1)
- Energie (1)
- Imote2 (1)
- JavaScript (1)
- Kommunikation (1)
- Mood-based Music Recommendations (1)
- Quartz (1)
- Recommender Systems (1)
- Regelung (1)
- SDL (1)
- Scheduling (1)
- Socio-Semantic Web (1)
- Stimmungsbasierte Musikempfehlungen (1)
- Themenbasierte Empfehlungen von Ressourcen (1)
- Topic-based Resource Recommendations (1)
- Usage Control (1)
- concurrent (1)
- data-flow (1)
- distributed (1)
- embedded (1)
- inverses Pendel (1)
- message-passing (1)
- multicore (1)
- multithreading (1)
- out-of-order (1)
- parallel (1)
- synchronous (1)
Faculty / Organisational entity
In most cases in a safety analysis the influences of security problems are omitted or even forgotten. Because more and more systems are accessible from outside the system via maintenance interfaces, this missing security analysis is becoming a problem. This is why we propose an approach on how to extend the safety analysis by security aspects. Such a more comprehensive analysis should lead to systems that react in less catastrophic ways to attacks.
This thesis provides a fully automatic translation from synchronous programs to parallel software for different architectures, in particular, shared memory processing (SMP) and distributed memory systems. Thereby, we exploit characteristics of the synchronous model of computation (MoC) to reduce communication and to improve available parallelism and load-balancing by out-of-order (OOO) execution and data speculation.
Manual programming of parallel software requires the developers to partition a system into tasks and to add synchronization and communication. The model-based approach of development abstracts from details of the target architecture and allows to make decisions about the target architecture as late as possible. The synchronous MoC supports this approach by abstracting from time and providing implicit parallelism and synchronization. Existing compilation techniques translate synchronous programs into synchronous guarded actions (SGAs) which are an intermediate format abstracting from semantic problems in synchronous languages. Compilers for SGAs analyze causality problems, ensure logical correctness and the absence of schizophrenia problems. Hence, SGAs are a simplified and general starting point and keep the synchronous MoC at the same time. The instantaneous feedback in the synchronous MoC makes the mapping of these systems to parallel software a non-trivial task. In contrast, other MoCs such as data-flow processing networks (DPNs) directly match with parallel architectures. We translate the SGAs into DPNs,which represent a commonly used model to create parallel software. DPNs have been proposed as a programming model for distributed parallel systems that have communication paths with unpredictable latencies. The purely data-driven execution of DPNs does not require a global coordination and therefore DPNs can be easily mapped to parallel software for architectures with distributed memory. The generation of efficient parallel code from DPNs challenges compiler design with two issues: To perfectly utilize a parallel system, the communication and synchronization has to be kept low, and the utilization of the computational units has to be balanced. The variety of hardware architectures and dynamic execution techniques in processing units of these systems make a statically balanced distributed execution impossible.
The synchronous MoC is still reflected in our generated DPNs, which exhibits characteristics that allow optimizations concerning the previously mentioned issues. In particular, we apply a general communication reduction and OOO execution to achieve a dynamically balanced execution which is inspired from hardware design.
An huge amount of computational models and programming languages have been proposed
for the description of embedded systems. In contrast to traditional sequential programming
languages, they cope directly with the requirements for embedded systems: direct support for
concurrent computations and periodic interaction with the environment are only some of the
features they offer. Synchronous languages are one class of languages for the development of
embedded systems and they follow the fundamental principle that the execution is divided into
a sequence of logical steps. Thereby, each step follows the simplification that the computation
of the outputs is finished directly when the inputs are available. This rigorous abstraction leads
to well-defined deterministic parallel composition in general, and to deterministic abortion
and suspension in imperative synchronous languages in particular. These key features also
allow to translate programs to hardware and software, and also formal verification techniques
like model checking can be easily applied.
Besides the advantages of imperative synchronous languages, also some drawbacks can
be listed. Over-synchronization is an effect being caused by parallel threads which have to
synchronize for each execution step, even if they do not communicate, since the synchronization
is implicitly forced by the control-flow. This thesis considers the idea of clock refinement to
introduce several abstraction layers for communication and synchronization in addition to the
existing single-clock abstraction. Thereby, clocks can be refined by several independent clocks
so that a controlled amount of asynchrony between subsequent synchronization points can be
exploited by compilers. The declarations of clocks form a tree, and clocks can be defined within
the threads of the parallel statement, which allows one to do independent computations based
on these clocks without synchronizing the threads. However, the synchronous abstraction is
kept at each level of the abstraction.
Clock refinement is introduced in this thesis as an extension to the imperative synchronous
language Quartz. Therefore, new program statements are introduced which allow to define
a new clock as a refinement of an existing one and to finish a step based on a certain clock.
Examples are considered to show the impact of the behavior of the new statements to
the already existing statements, before the semantics of this extension is formally defined.
Furthermore, the thesis presents a compile algorithm to translate programs to an intermediate
format, and to translate the intermediate format to a hardware description. The advantages
obtained by the new modeling feature are finally evaluated based on examples.
Backward compatibility of class libraries ensures that an old implementation of a library can safely be replaced by a new implementation without breaking existing clients.
Formal reasoning about backward compatibility requires an adequate semantic model to compare the behavior of two library implementations.
In the object-oriented setting with inheritance and callbacks, finding such models is difficult as the interface between library implementations and clients are complex.
Furthermore, handling these models in a way to support practical reasoning requires appropriate verification tools.
This thesis proposes a formal model for library implementations and a reasoning approach for backward compatibility that is implemented using an automatic verifier. The first part of the thesis develops a fully abstract trace-based semantics for class libraries of a core sequential object-oriented language. Traces abstract from the control flow (stack) and data representation (heap) of the library implementations. The construction of a most general context is given that abstracts exactly from all possible clients of the library implementation.
Soundness and completeness of the trace semantics as well as the most general context are proven using specialized simulation relations on the operational semantics. The simulation relations also provide a proof method for reasoning about backward compatibility.
The second part of the thesis presents the implementation of the simulation-based proof method for an automatic verifier to check backward compatibility of class libraries written in Java. The approach works for complex library implementations, with recursion and loops, in the setting of unknown program contexts. The verification process relies on a coupling invariant that describes a relation between programs that use the old library implementation and programs that use the new library implementation. The thesis presents a specification language to formulate such coupling invariants. Finally, an application of the developed theory and tool to typical examples from the literature validates the reasoning and verification approach.
Compared to traditional software design, the design of embedded software is even more challenging: In addition to the correct implementation of the systems, one has to consider non-functional constraints such as real-time behavior, reliability, and energy consumption. Moreover, many embedded systems are used in safety-critical applications where errors can lead to enormous damages and even to the loss of human live. For this reason, formal verification is applied in many design flows using different kinds of formal verification methods.
The synchronous model of computation has shown to be well-suited in this context. Its core is the paradigm of perfect synchrony which assumes that the overall system behavior is divided into a sequence of reactions, and all computations within a reaction are completed in zero time. This temporal abstraction simplifies reactive programming in that developers do not have to bother about many low-level details related to timing, synchronization and scheduling. This thesis is dedicated to this design flow, and it presents the author's contributions to it.
Due to tremendous improvements of high-performance computing resources as well
as numerical advances computational simulations became a common tool for modern
engineers. Nowadays, simulation of complex physics is more and more substituting a
large amount of physical experiments. While the vast compute power of large-scale
high-performance systems enabled for simulating more complex numerical equations,
handling the ever increasing amount of data with spatial and temporal resolution
burdens new challenges to scientists. Huge hardware and energy costs desire for
ecient utilization of high-performance systems. However, increasing complexity of
simulations raises the risk of failing simulations resulting in a single simulation to be
restarted multiple times. Computational Steering is a promising approach to interact
with running simulations which could prevent simulation crashes. The large amount
of data expands gaps in the amount of data that can be calculated and the amount of
data that can be processed. Extreme-scale simulations produce more data that can
even be stored. In this thesis, I propose several methods that enhance the process
of steering, exploring, visualizing, and analyzing ongoing numerical simulations.
There is a growing trend for ever larger wireless sensor networks (WSNs) consisting of thousands or tens of thousands of sensor nodes (e.g., [91, 79]). We believe this trend will continue and thus scalability plays a crucial role in all protocols and mechanisms for WSNs. Another trend in many modern WSN applications is the time sensitivity to information from sensors to sinks. In particular, WSNs are a central part of the vision of cyber-physical systems and as these are basically closed-loop systems many WSN applications will have to operate under stringent timing requirements. Hence, it is crucial to develop algorithms that minimize the worst-case delay in WSNs. In addition, almost all WSNs consist of battery-powered nodes, and thus energy-efficiency clearly remains another premier goal in order to keep network lifetime high. This dissertation presents and evaluates designs for WSNs using multiple sinks to achieve high lifetime and low delay. Firstly, we investigate random and deterministic node placement strategies for large-scale and time-sensitive WSNs. In particular, we focus on tiling-based deterministic node placement strategies and analyze their effects on coverage, lifetime, and delay performance under both exact placement and stochastically disturbed placement. Next, we present sink placement strategies, which constitutes the main contributions of this dissertation. Static sinks will be placed and mobile sinks will be given a trajectory. A proper sink placement strategy can improve the performance of a WSN significantly. In general, the optimal sink placement with lifetime maximization is an NP-hard problem. The problem is even harder if delay is taken into account. In order to achieve both lifetime and delay goals, we focus on the problem of placing multiple (static) sinks such that the maximum worst-case delay is minimized while keeping the energy consumption as low as possible. Different target networks may need a corresponding sink placement strategy under differing levels of apriori assumptions. Therefore, we first develop an algorithm based on the Genetic Algorithm (GA) paradigm for known sensor nodes' locations. For a network where global information is not feasible we introduce a self-organized sink placement (SOSP) strategy. While GA-based sink placement achieves a near-optimal solution, SOSP provides a good sink placement strategy with a lower communication overhead. How to plan the trajectories of many mobile sinks in very large WSNs in order to simultaneously achieve lifetime and delay goals had not been treated so far in the literature. Therefore, we delve into this difficult problem and propose a heuristic framework using multiple orbits for the sinks' trajectories. The framework is designed based on geometric arguments to achieve both, high lifetime and low delay. In simulations, we compare two different instances of our framework, one conceived based on a load-balancing argument and one based on a distance minimization argument, with a set of different competitors spanning from statically placed sinks to battery-state aware strategies. We find our heuristics outperform the competitors in both, lifetime and delay. Furthermore, and probably even more important, the heuristic, while keeping its good delay and lifetime performance, scales well with an increasing number of sinks. In brief, the goal of this dissertation is to show that placing nodes and sinks in conventional WSNs as well as planning trajectories in mobility enabled WSNs carefully really pays off for large-scale and time-sensitive WSNs.
Recent progresses and advances in the field of consumer electronics, driven by display
technologies and also the sector of mobile, hand-held devices, enable new ways in
presenting information to users, as well as new ways of user interaction, therefore
providing a basis for user-centered applications and work environments.
My thesis focuses on how arbitrary display environments can be utilized to improve
both the user experience, regarding perception of information, and also to provide
intuitive interaction possibilities. On the one hand advances in display technologies
provide the basis for new ways of visualizing content and collaborative work, on the
other hand forward-pressing developments in the consumer market, especially the
market of smart phones, offer potential to enhance usability in terms of interaction
and therefore can provide additional benefit for users.
Tiled display setups, combining both large screen real estate and high resolution,
provide new possibilities and chances to visualize large datasets and to facilitate col-
laboration in front of a large screen area. Furthermore these display setups present
several advantages over the traditional single-user-workspace environments: con-
trary to single-user-workspaces, multiple users are able to explore a dataset displayed
on a tiled display system, at the same time, thus allowing new forms of collabora-
tive work. Based on that, face-to-face discussions are enabled, an additional value
is added. Large displays also allow the utilization of the user’s spatial memory, al-
lowing physical navigation without the need of switching between different windows
to explore information.
With Tiled++ I contributed a versatile approach to address the bezel problem. The
bezel problem is one of the Top Ten research challenges in the research field of LCD-
based tiled wall setups. By applying the Tiled++ approach a large high resolution
Focus & Context screen is created, combining high resolution focus areas with low
resolution context information, projected onto the bezel area.
Additionally the field of user interaction poses an important challenge, especially
regarding the utilization of large tiled displays, since traditional keyboard & mouse
interaction devices reached their limits. My focus in this thesis is on Mobile HCI.Devices like mobile phones are utilized to interact with large displays, since they
feature various interaction modalities and preserve user mobility.
Large public displays, as a modernized form of traditional bulletin boards, also en-
able new ways of handling information, displaying content, and user interaction.
Utilized in hot spots, Digital Interactive Public Pinboards can provide an adequate
answer to questions like how to approach pressing issues like disaster and crisis man-
agement for both responders as well as citizens and also new ways of how to handle
information flow (contribution & distribution & accession). My contribution to the
research field of public display environments was the conception and implementa-
tion of an easy-to-use and easy-to-set-up architecture to overcome shortcomings of
current approaches and to cover the needs of aid personnel.
Although being a niche, Virtual Reality (VR) environments can provide additional
value for visualizing specific content. Disciplines like earth sciences & geology, me-
chanical engineering, design, and architecture can benefit from VR environments. In
order to consider the variety of users, I introduce a more intuitive and user friendly
interaction metaphor, the ARC metaphor.
Visualization challenges base on being able to cope with more and more complex
datasets and to bridge the gap between comprehensibility and loss of information.
Furthermore the visualization approach has to be reasonable, which is a crucial
factor when working in interdisciplinary teams, where the standard of knowledge
is diverse. Users have to be able to conceive the visualized content in a fast and
reliable way. My contribution are visualization approaches in the field of supportive
visualization.
Finally, my work illuminates how the synthesis of visualization, interaction and dis-
play technologies enhance the user experience. I promote a holistic view. The user
is brought back into the focus of attention, provided with a tool-set to support him,
without overextending the abilities of, for example, non-expert users, a crucial factor
in the more and more interdisciplinary field of computer science.
Modellgetriebene Entwicklung von Kommunikationsprotokollen für drahtlos vernetzte Regelungssysteme
(2013)
Funkvernetzte Sensorsysteme sind heutzutage allgegenwärtig.
Sie werden sowohl in Rauchmeldern, in Raumtemperaturüberwachungen und Sicherheitssystemen eingesetzt.
Das Sensorsystem soll seine Aufgabe zuverlässig und über viele Jahre ohne Batteriewechsel erfüllen.
Durch die Vernetzung der Sensorsysteme und ihre immer komplexer werdenden Aufgaben wird die Programmierung in einer maschinennahen Sprache immer aufwändiger.
Die modellgetriebene Entwicklung erhöht die Wartbarkeit und reduziert die Entwicklungszeit wodurch im Allgemeinen die Produktqualität steigt.
In Folge der höheren Komplexität, der Abstraktion von der konkreten Hardwareplattform und den immer kürzere Produktentwicklungszeiten bleibt oft keine Zeit für Energieoptimierung, wodurch die Batterielaufzeit geringer ausfällt, als dies möglich wäre.
In dieser Arbeit werden verschiedene Ansätze vorgestellt, die es ermöglichen, bereits während der Modellierung den Stromverbrauch zu berücksichtigen und diesen zu optimieren.
Am Beispiel des inversen Pendels, einem sehr instabilen Regelungssystem, wird dazu mit Hilfe der modellgetriebenen Entwicklung eine funkvernetzte, verteilte Regelung spezifiziert.
Der aus der Spezifikation erzeugte Kode wird direkt auf den Sensorknoten ausgeführt und muß dazu performant und zuverlässig sein, um die Echtzeitanforderungen des Regelungssystems zu erfüllen, aber gleichzeitig so wenig Energie wie möglich zu verbrauchen.
m die Zuverlässigkeit der verteilten Regelung zu gewährleisten ist eine deterministische kollisionsfreie Datenübertragung über das drahtlose Kommunikationsmedium erforderlich.
Die Synchronisation ist eine weitere Voraussetzung zur Ermittlung eines konsistenten Systemzustands.
Most of the evolution in ambient assisted living is due to embedded
systems that dynamically adapt themself to react to environmental
changes or component/subsystem failures to maintain a certain level of
safety. Following this evolution fault tree analysis techniques have been
extended with concept for dynamic adaptation but resulting techniques
such as dynamic fault trees or state event fault trees analysis are not
widely used as expected.
In this report we describe a controlled experiment to analyze these two
techniques with regard to their applicability and efficiency in modeling
dynamic behavior of ambient assisted living systems.
Results of the experiment show that Dynamic Fault Trees are easier and more effective
to use, although they produce better results (models) with State Events Fault Trees.