Kaiserslautern - Fachbereich Elektrotechnik und Informationstechnik
Refine
Year of publication
Document Type
- Doctoral Thesis (93) (remove)
Has Fulltext
- yes (93)
Keywords
- Mobilfunk (10)
- Model checking (5)
- mobile radio (4)
- Formal Verification (3)
- MIMO (3)
- Niederspannungsnetz (3)
- OFDM (3)
- System-on-Chip (3)
- Verifikation (3)
- Bounded Model Checking (2)
Faculty / Organisational entity
Property-Driven Design
(2021)
We introduce Property-Driven Design, a tool-flow that guarantees formal soundness be- tween ESL and RTL and thus enables a shift-left of general functional verification by moving HW verification to higher abstraction layers. In addition, by generating a formal Verification IP (VIP) automatically from ESL descriptions, the entry hurdle to formal methods is reduced considerably, opening them to a wider audience, which effectively ‘democratizes’ them. Short feedback cycles reduce time spent on RTL verification and lead to higher-quality designs.
Mit dem Vorhandensein elektrischer Energie und moderner Sensorik an elektrisch unterstützten Fahrrädern eröffnen sich neue Möglichkeiten der Entwicklung von Fahrerassistenzsystemen am Pedelec zur Erhöhung der Sicherheit und des Fahrkomforts. Die Leistungsfähigkeit solcher Systeme kann durch die Nutzung von Inertialsensorik weiter gesteigert werden. Jedoch müssen solche Sensoren, vor allem bei sicherheitsrelevanten Assistenzsystemen, zuverlässige, robuste und plausible Sensordaten liefern. Hieraus ergibt sich das Thema dieser Arbeit: die Evaluation von Inertialsensorik für Fahrerassistenzsysteme am Pedelec anhand systematischer Untersuchung der Fahrdynamik.
Durch simulative und experimentelle Untersuchungen der MEMS-Sensorik und der Fahrdynamik, basierend auf Testkatalogen, werden die Anforderungen an Inertialsensorik abgeleitet und die Störbarkeit der Drehrate analysiert. Dabei führt die Betrachtung verschiedener Sensortypen, Fahrszenarien und Anbaupositionen zu der Erkenntnis, dass bspw. die Anbauposition am Sattelrohr und in der Antriebseinheit besonders geeignet sind. Vor allem der betrachtete Automotive-MEMS-Sensor liefert auch bei potentiell kritischen Vibrationen bei einer Fahrt über Kopfsteinpflaster oder über Treppenstufen sowie bei Bremsenquietschen zuverlässig plausible Sensordaten.
Zusätzlich zeigt eine Betrachtung der Auswirkungen von Sensorfehlern auf eine Datenfusion, d.h. der Berechnung der Raumwinkel, dass vor allem die Minimierung des Offset-Fehlers, bspw. durch eine Langzeitkorrektur, sinnvoll erscheint und resultierende Winkelfehler minimieren kann.
Die Untersuchung der Fahrdynamik betrachtet insbesondere das Fahrszenario (kritische) Kurvenfahrt. Anhand der Fahrdaten zahlreicher Pedelec-Nutzer werden eine Methode zur Erkennung von Kurvenfahrten sowie theoretische Ansätze zur Vermeidung einer kritischen Kurvenfahrt durch einen aktiven Lenkeingriff realisiert.
Small embedded devices are highly specialized platforms that integrate several pe- ripherals alongside the CPU core. Embedded devices extensively rely on Firmware (FW) to control and access the peripherals as well as other important functionality. Customizing embedded computing platforms to specific application domains often necessitates optimizing the firmware and/or the HW/SW interface under tight re- source constraints. Such optimizations frequently alter the communication between the firmware and the peripheral devices, possibly compromising functional correct- ness of the input/output behavior of the embedded system. This poses challenges to the development and verification of such systems. The system must be adapted and verified to each specific device configuration.
This thesis presents a formal approach to formulate these verification tasks at several levels of abstraction, along with corresponding HW/SW co-equivalence checking techniques for verifying correct I/O behavior of peripherals under a modified firmware. The feasibility of the approach is shown on several case studies, including industrial driver software as well as open-source peripherals. In addition, a subtle bug in one of the peripherals and several undocumented preconditions for correct device behavior were detected by the verification method.
Beamforming performs spatial filtering to preserve the signal from given directions of interest while suppressing interfering signals and noise arriving from other directions.
For example, a microphone array equipped with beamforming algorithm could preserve the sound coming from a target speaker and suppress sounds coming from other speakers.
Beamformer has been widely used in many applications such as radar, sonar, communication, and acoustic systems.
A data-independent beamformer is the beamformer whose coefficients are independent on sensor signals, it normally uses less computation since the coefficients are computed once. Moreover, its coefficients are derived from the well-defined statistical models, then it produces less artifacts. The major drawback of this beamforming class is its limitation to the interference suppression.
On the other hand, an adaptive beamformer is a beamformer whose coefficients depend on or adapt to sensor signals. It is capable of suppressing the interference better than a data-independent beamforming but it suffers from either too much distortion of the signal of interest or less noise reduction when the updating rate of coefficients does not synchronize with the changing rate of the noise model. Besides, it is computationally intensive since the coefficients need to be updated frequently.
In acoustic applications, the bandwidth of signals of interest extends over several octaves, but we always expect that the characteristic of the beamformer is invariant with regard to the bandwidth of interest. This can be achieved by the so-called broadband beamforming.
Since the beam pattern of conventional beamformers depends on the frequency of the signal, it is common to use a dense and uniform array for the broadband beamforming to guarantee some essential performances together, such as frequency-independence, less sensitive to white noise, high directivity factor or high front-to-back ratio. In this dissertation, we mainly focus on the sparse array of which the aim is to use fewer sensors in the array,
while simultaneously assuring several important performances of the beamformer.
In the past few decades, many design methodologies for sparse arrays have been proposed and were applied in a variety of practical applications.
Although good results were presented, there are still some restrictions, such as the number of sensors is large, the designed beam pattern must be fixed, the steering ability is limited and the computational complexity is high.
In this work, two novel approaches for the sparse array design taking a hypothesized uniform array as a basis are proposed, that is, one for data-independent beamformers and the another for adaptive beamformers.
As an underlying component of the proposed methods, the dissertation introduces some new insights into the uniform array with broadband beamforming. In this context, a function formulating the relations between the sensor coefficients and its beam pattern over frequency is proposed. The function mainly contains the coordinate transform and inverse Fourier transform.
Furthermore, from the bijection of the function and broadband beamforming perspective, we propose the lower and upper bounds for the inter-distance of sensors. Within these bounds, the function is a bijective function that can be utilized to design the uniform array with broadband beamforming.
For data-independent beamforming, many studies have focused on optimization procedures to seek the sparse array deployment. This dissertation presents an alternative approach to determine the location of sensors.
Starting with a weight spectrum of a virtual dense and uniform array, some techniques are used, such as analyzing a weight spectrum to determine the critical sensors, applying the clustering technique to group the sensors into different groups and selecting representative sensors for each group.
After the sparse array deployment is specified, the optimization technique is applied to find the beamformer coefficients. The proposed method helps to save the computation time in the design phase and its beamformer performance outperforms other state-of-the-art methods in several aspects such as the higher white noise gain, higher directivity factor or more frequency-independence.
For adaptive beamforming, the dissertation attempts to design a versatile sparse microphone array that can be used for different beam patterns.
Furthermore, we aim to reduce the number of microphones in the sparse array while ensuring that its performance can continue to compete with a highly dense and uniform array in terms of broadband beamforming.
An irregular microphone array in a planar surface with the maximum number of distinct distances between the microphones is proposed.
It is demonstrated that the irregular microphone array is well-suited to sparse recovery algorithms that are used to solve underdetermined systems with subject to sparse solutions. Here, a sparse solution is the sound source's spatial spectrum that need to be reconstructed from microphone signals.
From the reconstructed sound sources, a method for array interpolation is presented to obtain an interpolated dense and uniform microphone array that performs well with broadband beamforming.
In addition, two alternative approaches for generalized sidelobe canceler (GSC) beamformer are proposed. One is the data-independent beamforming variant, the other is the adaptive beamforming variant. The GSC decomposes beamforming into two paths: The upper path is to preserve the desired signal, the lower path is to suppress the desired signal. From a beam pattern viewpoint, we propose an improvement for GSC, that is, instead of using the blocking matrix in the lower path to suppress the desired signal, we design a beamformer that contains the nulls at the look direction and at some other directions. Both approaches are simple beamforming design methods and they can be applied to either sparse array or uniform array.
Lastly, a new technique for direction-of-arrival (DOA) estimation based on the annihilating filter is also presented in this dissertation.
It is based on the idea of finite rate of innovation to reconstruct the stream of Diracs, that is, identifying an annihilating filter/locator filter for a few uniform samples and the position of the Diracs are then related to the roots of the filter. Here, an annihilating filter is the filter that suppresses the signal, since its coefficient vector is always orthogonal to every frame of signal.
In the DOA context, we regard an active source as a Dirac associated with the arrival direction, then the directions of active sources can be derived from the roots of the annihilating filter. However,
the DOA obtained by this method is sensitive to noise and the number of DOAs is limited.
To address these issues, the dissertation proposes a robust method to design the annihilating filter and to increase the degree-of-freedom of the measurement system (more active sources can be detected) via observing multiple data frames.
Furthermore, we also analyze the performance of DOA with diffuse noise and propose an extended multiple signal classification algorithm that takes diffuse noise into account. In the simulation,
it shows, that in the case of diffuse noise, only the extended multiple signal classification algorithm can estimate the DOAs properly.
The nondestructive testing of multilayered materials is increasingly applied in
both scientific and industrial fields. In particular, developments in millimeter
wave and terahertz technology open up novel measurement applications, which
benefit from the nonionizing properties of this frequency range. One example is
the noncontact inspection of layer thicknesses. Frequently used measuring and
analysis methods lead to a resolution limit that is determined by the bandwidth
of the setup. This thesis analyzes the reliable evaluation of thinner layer thicknesses
using model-based signal processing.
Code coverage analysis plays an important role in the software testing process. More recently, the remarkable effectiveness of coverage feedback has triggered a broad interest in feedback-guided fuzzing. In this work, we discuss static instrumentation techniques for binary-level coverage analysis without compiler support. We show that the proposed techniques are precise, efficient, and transparent significantly beyond the state of the art.
We implement these techniques into two tools, namely, Spedi and bcov. Both tools are open source and publicly available. Spedi shows that the disassembly and function identification of stripped binaries can be highly accurate without resort to any external information. We build on these important results in bcov where we statically instrument x86-64 ELF binaries to track code coverage. However, improving efficiency and scaling to large real-world software required an orchestrated effort combining several techniques.
First, we bring a well-known probe pruning technique, for the first time, to binary-level instrumentation and effectively leverage its notion of superblocks to reduce overhead. Second, we introduce sliced microexecution, a robust technique for jump table analysis which improves CFG precision and enables us to instrument jump table entries. Additionally, smaller instructions in x86-64 pose a challenge for inserting detours. To address this challenge, we aggressively exploit padding bytes. Also, we introduce a greedy scheme to systematically host detours in neighboring basic blocks.
We evaluate bcov on a corpus of 95 binaries compiled from eight popular and well-tested packages like FFmpeg and LLVM. Two instrumentation policies, with different edge-level precision, are used to patch all functions in this corpus - over 1.6 million functions. Our precise policy has average performance and memory overheads of 14% and 22%, respectively. Instrumented binaries do not introduce any test regressions. The reported coverage is highly accurate with an average F-score of 99.86%. Finally, our jump table analysis is comparable to that of IDA Pro on gcc binaries and outperforms it on clang binaries.
Our work demonstrates that static instrumentation can offer unique advantages in comparison to established methods like compiler instrumentation and dynamic binary instrumentation. It also opens the door for many interesting applications of static instrumentation, which can go well beyond coverage analysis.
Ein Beitrag zur Zustandsschätzung in Niederspannungsnetzen mit niedrigredundanter Messwertaufnahme
(2020)
Durch den wachsenden Anteil an Erzeugungsanlagen und leistungsstarken Verbrauchern aus dem Verkehr- und Wärmesektor kommen Niederspannungsnetze immer näher an ihre Betriebsgrenzen. Da für die Niederspannungsnetze bisher keine Messwerterfassung vorgesehen war, können Netzbetreiber Grenzverletzungen nicht erkennen. Um dieses zu ändern, werden deutsche Anschlussnutzer in Zukunft flächendeckend mit modernen Messeinrichtungen oder intelligenten Messsystemen (auch als Smart Meter bezeichnet) ausgestattet sein. Diese sind in der Lage über eine Kommunikationseinheit, das Smart-Meter-Gateway, Messdaten an die Netzbetreiber zu senden. Werden Messdaten aber als personenbezogene Netzzustandsdaten deklariert, so ist aus Datenschutzgründen eine Erhebung dieser Daten weitgehend untersagt.
Ziel dieser Arbeit ist es eine Zustandsschätzung zu entwickeln, die auch bei niedrigredundanter Messwertaufnahme für den Netzbetrieb von Niederspannungsnetzen anwendbare Ergebnisse liefert. Neben geeigneten Algorithmen zur Zustandsschätzung ist dazu die Generierung von Ersatzwerten im Fokus.
Die Untersuchungen und Erkenntnisse dieser Arbeit tragen dazu bei, den Verteilnetzbetreibern bei den maßgeblichen Entscheidungen in Bezug auf die Zustandsschätzung in Niederspannungsnetzen zu unterstützen. Erst wenn Niederspannungsnetze mit Hilfe der Zustandsschätzung beobachtbar sind, können darauf aufbauende Konzepte zur Regelung entwickelt werden, um die Energiewende zu unterstützen.
In today’s world, mobile communication has become one of the most widely used technologies corroborated by growing number of mobile subscriptions and extensive usage of mobile multimedia services. It is a key challenge for the network operators to accommodate such large number of users and high traffic volume. Further, several day-to-day scenarios such as public transportation, public events etc., are now characterized with high mobile data
usage. A large number of users avail cellular services in such situations posing
high load to the respective base stations. This results in increased number of dropped connections, blocking of new access attempts and blocking of handovers (HO). The users in such system will thus be subjected to poor
Quality of Experience (QoE). Beforehand knowledge of the changing data traffic dynamics associated with such practical situations will assist in designing
radio resource management schemes aiming to ease the forthcoming congestion situations. The key hypothesis of this thesis is that consideration and utilization of additional context information regarding user, network and his environment is valuable in designing such smart Radio Resource Management(RRM) schemes. Methods are developed to predict the user cell transitions, considering the fact that mobility of the users is not purely random but rather direction oriented. This is particularly used in case of traffic dense moving network or group of users moving jointly in the same vehicle (e.g., bus, train, etc.) to
predict the propagation of high load situation among cells well in advance.
This enables a proactive triggering of load balancing (LB) in cells anticipating
the arrival of high load situation and accommodating the incoming user group or moving network. The evaluated KPIs such as blocked access
attempts, dropped connections and blocked HO are reduced.
Further, everyday scenario of dynamic crowd formation is considered as another potential case of high load situation. In real world scenarios such as open air festivals, shopping malls, stadiums or public events, several mobile users gather to form a crowd. This poses high load situation to the respective serving base station at the site of crowd formation, thereby leading to congestion. As a consequence, mobile users are subjected to poor QoE due to high dropping and blocking rates. A framework to predict crowd formation in a cell is developed based on coalition of user cell transition prediction, cluster detection and trajectory prediction. This framework is suitably used to prompt context aware load balancing mechanism and activate a small cell at the probable site of crowd formation. Simulations show that proactive LB
reduces the dropping of users (23%), blocking of users (10%) and blocked
HO (15%). In addition, activation of a Small Cell (SC) at the site of frequent
crowd formation leads to further reductions in dropping of users (60%),
blocking of users (56%) and blocked HO (59%).
Similar to the framework for crowd formation prediction, a concept is developed for predicting vehicular traffic jams. Many vehicular users avail broadband cellular services on a daily basis while traveling. The density of such vehicular users change dynamically in a cell and at certain sites (e.g.
signal lights), traffic jams arise frequently leading to a high load situation at
respective serving base station. A traffic prediction algorithm is developed
from cellular network perspective as a coalition strategy consisting of schemes to predict user cell transition, vehicular cluster/moving network detection, user velocity monitoring etc. The traffic status indication provided by the algorithm is then used to trigger LB and activate/deactivate a small cell suitably. The evaluated KPIs such as blocked access attempts, dropped connections
and blocked HO are reduced by approximately 10%, 18% and 18%, respectively due to LB. In addition, switching ON of SC reduces blocked access attempts, dropped connections and blocked HO by circa 42%, 82% and 81%, respectively.
Amidst increasing number of connected devices and traffic volume, another key issue for today’s network is to provide uniform service quality
despite high mobility. Further, urban scenarios are often characterized by
coverage holes which hinder service continuity. A context aware resource allocation scheme is proposed which uses enhanced mobility prediction to facilitate service continuity. Mobility prediction takes into account additional information about the user’s origin and possible destination to predict next road segment. If a coverage hole is anticipated in upcoming road, then additional
resources are allocated to respective user and data is buffered suitably.
The buffered data is used when the user is in a coverage hole to improve service continuity. Simulation shows improvement in throughput (in coverage
hole) by circa 80% and service interruption is reduced by around 90%, for a
non-real-time streaming service. Additionally, investigation of context aware procedures is carried out with a focus on user mobility, to find commonalities among different procedures and a general framework is proposed to support mobility context awareness. The new information and interfaces which are required from various entities
(e.g., vehicular infrastructure) are discussed as well.
Device-to-Device (D2D) communications commonly refer to the technology
that enables direct communication between devices, hence relieving the
base station from traffic routing. Thus, D2D communication is a feasible
solution in crowded situations, where users in proximity requesting to communicate with one another could be granted D2D links for communication, thereby easing the traffic load to serving base station. D2D links can potentially
reuse the radio resources from cellular users (known as D2D underlay) leading to better spectral utilization. However, the mutual interference can hinder system performance. For instance, if D2D links are reusing cellular uplink resources then D2D transmissions cause interference to cellular uplink at base station. Whereas, cellular transmissions cause interference to
D2D receivers. To cope up with such issues, location aware resource allocation
schemes are proposed for D2D communication. The key aim of such RA scheme is to reuse resources with minimal interference. The RA scheme based on virtual sectoring of a cell leads to approximately 15% more established
links and 25% more capacity with respect to a random resource allocation. D2D transmissions cause significant interference to cellular links with
which they reuse physical resource blocks, thereby hindering cellular performance. Regulating D2D transmissions to mitigate the aforementioned problem would mean sub-optimal exploitation of D2D communications. As
a solution, post-resource allocation power control at cellular users is proposed.
Three schemes namely interference aware power control, blind power
control and threshold based power control are discussed. Simulation results
show reductions in dropping of cellular users due to interference from D2D
transmissions, improvement in throughput at base station (uplink) while not hindering the D2D performance.
Indoor positioning system (IPS) is becoming more and more popular in recent years in industrial, scientific and medical areas. The rapidly growing demand of accurate position information attracts much attention and effort in developing various kinds of positioning systems that are characterized by parameters like accuracy,robustness,
latency, cost, etc. These systems have been successfully used in many applications such as automation in manufacturing, patient tracking in hospital, action detection for human-machine interacting and so on.
The different performance requirements in various applications lead to existence of greatly diverse technologies, which can be categorized into two groups: inertial positioning(involving momentum sensors embedded on the object device to be located) and external sensing (geometry estimation based on signal measurement). In positioning
systems based on external sensing, the input signal used for locating refers to many sources, such as visual or infrared signal in optical methods, sound or ultra-sound in acoustic methods and radio frequency based methods. This dissertation gives a recapitulative survey of a number of existence popular solutions for indoor positioning systems. Basic principles of individual technologies are demonstrated and discussed. By comparing the performances like accuracy, robustness, cost, etc., a comprehensive review of the properties of each technologies is presented, which concludes a guidance for designing a location sensing systems for indoor applications. This thesis will lately focus on presenting the development of a high precision IPS
prototype system based on RF signal from the concept aspect to the implementation up to evaluation. Developing phases related to this work include positioning scenario, involved technologies, hardware development, algorithms development, firmware generation, prototype evaluation, etc.. The developed prototype is a narrow band RF system, and it is suitable for a flexible frequency selection in UHF (300MHz3GHz) and SHF (3GHz30GHz) bands, enabling this technology to meet broad service preferences. The fundamental of the proposed system classified itself as a hyperbolic position fix system, which estimates a location by solving non-linear equations derived from time difference of arrival (TDoA) measurements. As the positioning accuracy largely depends on the temporal resolution of the signal acquisition, a dedicated RF front-end system is developed to achieve a time resolution in range of multiple picoseconds down to less than 1 pico second. On the algorithms aspect, two processing units: TDoA estimator and the Hyperbolic equations solver construct the digital signal processing system. In order to implement a real-time positioning system, the processing system is implemented on a FPGA platform. Corresponding firmware is generated from the algorithms modeled in MATLAB/Simulink, using the high level synthesis (HLS) tool HDL Coder. The prototype system is evaluated and an accuracy of better than 1 cm is achieved. A better performance is potential feasible by manipulating some of the controlling conditions such as ADC sampling rate, ADC resolution, interpolation process, higher frequency, more stable antenna, etc. Although the proposed system is initially dedicated to indoor applications, it could also be a competitive candidate for an outdoor positioning service.
Ethernet has become an established communication technology in industrial automation. This was possible thanks to the tremendous technological advances and enhancements of Ethernet such as increasing the link-speed, integrating the full-duplex transmission and the use of switches. However these enhancements were still not enough for certain high deterministic industrial applications such as motion control, which requires cycle time below one millisecond and jitter or delay deviation below one microsecond. To meet these high timing requirements, machine and plant manufacturers had to extend the standard Ethernet with real-time capability. As a result, vendor-specific and non-IEEE standard-compliant "Industrial Ethernet" (IE) solutions have emerged.
The IEEE Time-Sensitive Networking (TSN) Task Group specifies new IEEE-conformant functionalities and mechanisms to enable the determinism missing from Ethernet. Standard-compliant systems are very attractive to the industry because they guarantee investment security and sustainable solutions. TSN is considered therefore to be an opportunity to increase the performance of established Industrial-Ethernet systems and to move forward to Industry 4.0, which require standard mechanisms.
The challenge remains, however, for the Industrial Ethernet organizations to combine their protocols with the TSN standards without running the risk of creating incompatible technologies. TSN specifies 9 standards and enhancements that handle multiple communication aspects. In this thesis, the evaluation of the use of TSN in industrial real-time communication is restricted to four deterministic standards: IEEE802.1AS-Rev, IEEE802.1Qbu IEEE802.3br and IEEE802.1Qbv. The specification of these TSN sub-standards was finished at an early research stage of the thesis and hardware prototypes were available.
Integrating TSN into the Industrial-Ethernet protocols is considered a substantial strategical challenge for the industry. The benefits, limits and risks are too complex to estimate without a thorough investigation. The large number of Standard enhancements makes it hard to select the required/appropriate functionalities.
In order to cover all real-time classes in the automation [9], four established Industrial-Ethernet protocols have been selected for evaluation and combination with TSN as well as other performance relevant communication features.
The objectives of this thesis are to
(1) Provide theoretical, simulation and experimental evaluation-methodologies for the timing performance analysis of the deterministic TSN-standards mentioned above. Multiple test-plans are specified to evaluate the performance and compatibility of early version TSN-prototypes from different providers.
(2) Investigate multiple approaches and deduce migration strategies to integrate these features into the established Industrial-Ethernet protocols: Sercos III, Profinet IRT, Profinet RT and Ethernet/IP. A scenario of coexistence of time-critical traffic with other traffic in a TSN-network proves that the timing performance for highly deterministic applications, e.g. motion-control, can only be guaranteed by the TSN scheduling algorithm IEEE802.1Qbv.
Based on a requirements survey of highly deterministic industrial applications, multiple network scenarios and experiments are presented. The results are summarized into two case studies. The first case study shows that TSN alone is not enough to meet these requirements. The second case study investigates the benefits of additional mechanisms (Gigabit link-speed, minimum cycle time modeling, frame forwarding mechanisms, frame structure, topology migration, etc.) in combination with the TSN features. An implementation prototype of the proposed system and a simulation case study are used for the evaluation of the approach. The prototype is used for the evaluation and validation of the simulation model. Due to given scalability constraints of the prototype (no cut-through functionalities, limited number of TSN-prototypes, etc…), a realistic simulation model, using the network simulation tool OMNEST / OMNeT++, is conducted.
The obtained evaluation results show that a minimum cycle time ≤1 ms and a maximum jitter ≤1 μs can be achieved with the presented approaches.