KLUEDO | Fachbereich Informatik

Analysis and Verification of Complex Robot Systems using Behaviour-Based Control (2017)

Lisa Kiekbusch

The development of autonomous mobile robots is a major topic of current research. As those robots must be able to react to changing environments and avoid collisions also with moving obstacles, the fulfilment of safety requirements is an important aspect. Behaviour-based systems (BBS) have proven to meet several of the properties required for these kindsof robots, such as reactivity, extensibility and re-usability of individual components. BBS consist of a number of behavioural components that individually realise simple tasks. Their interconnection allows to achieve complex robot behaviour, which implies that correct connections are crucial. The resulting networks can get very large making them difficult to verify. This dissertation presents a novel concept for the analysis and verification of complex autonomous robot systems controlled by behaviour-based software architectures with special focus on the integration of environmental aspects into the processes. Several analysis techniques have been investigated and adapted to the special requirements of BBS. These include a structural analysis, which is used to find constraint violations and faults in the network layout. Fault tree analysis is applied to identify root causes of hazards and the relationship of system events. For this, a technique to map the behaviour-based control network to the structure of a fault tree has been developed. Testing and data analysis are used for the detection of failures and their root causes. Here, a new concept that identifies patterns in data recorded during test runs has been introduced. All of these methods cannot guarantee failure-free and safe robot behaviour and can never prove the absence of failures. Therefore, model checking as formal verification technique that proves a property to be correct for the given system, has been chosen to complement the set of analysis techniques. A novel concept for the integration of environmental influences into the model checking process is proposed. Environmental situations and the sensor processing chain are represented as synchronised automata similar to the modelling of the behavioural network. Tools supporting the whole verification process including the creation of formal queries in its environment have been developed. During the verification of large behavioural networks, the scalability of the model checking approach appears as a big problem. Several approaches that deal with this problem have been investigated and the selection of slicing and abstraction methods has been justified. A concept for the application of these methods is provided, that reduces the behavioural network to the relevant parts before the actual verification process. All techniques have been applied to the behaviour-based control system of the autonomous outdoor robot RAVON. Its complex network with more than 400 components allows for demonstrating the soundness of the presented concepts. The set of diﬀerent techniques provides a fundamental basis for a comprehensive analysis and verification of BBS acting in changing environments.

Analysis of Different Random Graph Models in the Identification of Network Motifs in Complex Networks (2017)

Wolfgang Schlauch

This thesis is concerned with different null-models that are used in network analysis. Whenever it is of interest whether a real-world graph is exceptional regarding a particular measure, graphs from a null-model can be used to compare the real-world graph to. By analyzing an appropriate null-model, a researcher may find whether the results of the measure on the real-world graph is exceptional or not. Deciding which null-model to use is hard and sometimes the difference between the null-models is not even considered. In this thesis, there are several results presented: First, based on simple global measures, undirected graphs are analyzed. The results for these measures indicates that it is not important which null-model is used, thus, the fastest algorithm of a null-model may be used. Next, local measures are investigated. The fastest algorithm proves to be the most complicated to analyze. The model includes multigraphs which do not meet the conditions of all the measures, thus, the measures themselves have to be altered to take care of multigraphs as well. After careful consideration, the conditions are met and the analysis shows, that the fastest is not always the best. The same applies for directed graphs, as is shown in the last part. There, another more complex measure on graphs is introduced. I continue testing the applicability of several null-models; in the end, a set of equations proves to be fast and good enough as long as conditions regarding the degree sequence are met.

Magnetic Field-based Localization System (2017)

Gerald Stephan Pirkl

This dissertation describes an indoor localization system based on oscillating magnetic fields and the underlying processing architecture. The system consists of several fixed anchor points, generating the magnetic fields (transmitter), and wearable magnetic field measurement units, whose position should be determined (receiver). The system is evaluated in different environments and application areas. Additionally, various fields of application are discussed and assessed in ubiquitous and pervasive computing and Ambient Assisted Living. The fusion of magnetic field-based distance information and positions derived from LIDAR distance measurements is described and evaluated. The system architecture consists of three layers, a physical layer, a layer for position and distance estimation between a magnetic field transmitter and a receiver, and a layer which uses several measurements to different transmitters to estimate the overall position of a wearable measurement unit. Each layer covers different aspects which have to be taken care of when magnetic field information is processed. Especially the properties of the generated magnetic field information are considered in the processing algorithms. The physical layer covers the magnetic field generation and magnetic Field-Based information transfer, synchronization of a transmitter and the receivers and the description of the locally measured magnetic fields on the receiver side. After a transfer of this information to a central processing unit, the hardware specific signal levels are transformed to the levels of the theoretical magnetic field models. The values are then used to estimate candidate positions and distances. Due to symmetrical effects of the magnetic fields, it is only possible to reduce the receiver position to 8 points around the transmitter (one position in each of the octants of the coordinate system). The determined positions have a mean error of 108 cm, the average error of the distance is 40 cm. On top of this, the distance and position information against different transmitters are fused, this covers clock synchronization of transmitters, triggering and scheduling sequences and distance and position based localization and tracking algorithms. The magnetic-field-based indoor localization system has been evaluated in different applications and environments; the mean position error is 60 cm to 70 cm depending on the environment. A comparison against an RF-based indoor localization system shows the robustness of magnetic fields against RF shadows caused by big metal objects. We additionally present algorithms for regions of interest detection, working on raw magnetic field information and transformed position and distance information. Setups in larger areas can distinguish regions which are further than 50 cm apart, small scale coil setups (3 transmitters in 2m^3) allow to resolve regions below 20 cm. In the end, we describe a fusion algorithm for a wearable localization system based on 4 LIDAR distance measurement units and magnetic field-based distance estimation. The magnetic field indoor localization system provides distance proximity information which is used to resolve ambiguous position estimates of the LIDAR system. In a room (8m × 10m), we achieve a mean error of 8 cm.

Requirements-Aware, Template-Based Protocol Graphs for Service-Oriented Network Architectures (2016)

Abbas Siddiqui

Rigidness of the Internet causes its architectural design issues such as interdependencies among the layers, no cross-layer information exchange, and applications dependency on the underlying protocols implementation. G-Lab (i.e., http://www.german-lab.de/) is a research project for Future Internet Architecture (FIA), which focuses on problems of the Internet such as rigidness, mobility, and addressing. Where the focus of ICSY (i.e., www.icsy) was on providing the flexibility in future network architectures. An approach so-called Service Oriented Network Architecture (SONATE) is proposed to compose the protocols dynamically. SONATE is based on principles of the service-oriented architecture (SOA), where protocols are decomposed in software modules and later they are put together on demand to provide the desired service. This composition of functionalities can be performed at various time-epochs (e.g., run-time, design-time, deployment-time). However, these epochs have trade-off in terms of the time-complexity (i.e., required setup time) and the provided flexibility. The design-time is the least time critical in comparison to other time phases, which makes it possible to utilize human-analytical capability. However, the design-time lacks the real-time knowledge of requirements and network conditions, what results in inflexible protocol graphs, and they cannot be changed at later stages on changing requirements. Contrary to the design-time, the run-time is most time critical where an application is waiting for a connection to be established, but at the same time it has maximum information to generate a protocol graph suitable to the given requirements. Considering limitations above of different time-phases, in this thesis, a novel intermediate functional composition approach (i.e., Template-Based Composition) has been presented to generate requirements aware protocol graphs. The template-based composition splits the composition process across different time-phases to exploit the less time critical nature and human-analytical availability of the design-time, ability to instantaneously deploy new functionalities of the deployment time and maximum information availability of the run-time. The approach is successfully implemented , demonstrated and evaluated based on its performance to know the implications for the practical use.

Safe and Cost-Efficient Mobile Robot Navigation in Aware Environments (2016)

Michael Arndt

When designing autonomous mobile robotic systems, there usually is a trade-off between the three opposing goals of safety, low-cost and performance. If one of these design goals is approached further, it usually leads to a recession of one or even both of the other goals. If for example the performance of a mobile robot is increased by making use of higher vehicle speeds, then the safety of the system is usually decreased, as, under the same circumstances, faster robots are often also more dangerous robots. This decrease of safety can be mitigated by installing better sensors on the robot, which ensure the safety of the system, even at high speeds. However, this solution is accompanied by an increase of system cost. In parallel to mobile robotics, there is a growing amount of ambient and aware technology installations in today's environments - no matter whether in private homes, offices or factory environments. Part of this technology are sensors that are suitable to assess the state of an environment. For example, motion detectors that are used to automate lighting can be used to detect the presence of people. This work constitutes a meeting point between the two fields of robotics and aware environment research. It shows how data from aware environments can be used to approach the abovementioned goal of establishing safe, performant and additionally low-cost robotic systems. Sensor data from aware technology, which is often unreliable due to its low-cost nature, is fed to probabilistic methods for estimating the environment's state. Together with models, these methods cope with the uncertainty and unreliability associated with the sensor data, gathered from an aware environment. The estimated state includes positions of people in the environment and is used as an input to the local and global path planners of a mobile robot, enabling safe, cost-efficient and performant mobile robot navigation during local obstacle avoidance as well as on a global scale, when planning paths between different locations. The probabilistic algorithms enable graceful degradation of the whole system. Even if, in the extreme case, all aware technology fails, the robots will continue to operate, by sacrificing performance while maintaining safety. All the presented methods of this work have been validated using simulation experiments as well as using experiments with real hardware.

Visual Analysis of Neuromuscular Junctions (2016)

Julia Portl

Synapses play a central role in the information propagation in the nervous system. A better understanding of synaptic structures and processes is vital for advancing nervous disease research. This work is part of an interdisciplinary project that aims at the quantitative examination of components of the neuromuscular junction, a synaptic connection between a neuron and a muscle cell. The research project is based on image stacks picturing neuromuscular junctions captured by modern electron microscopes, which permit the rapid acquisition of huge amounts of image data at a high level of detail. The large amount and sheer size of such microscopic data makes a direct visual examination infeasible, though. This thesis presents novel problem-oriented interactive visualization techniques that support the segmentation and examination of neuromuscular junctions. First, I introduce a structured data model for segmented surfaces of neuromuscular junctions to enable the computational analysis of their properties. However, surface segmentation of neuromuscular junctions is a very challenging task due to the extremely intricate character of the objects of interest. Hence, such problematic segmentations are often performed manually by non-experts and thus requires further inspection. With NeuroMap, I develop a novel framework to support proofreading and correction of three-dimensional surface segmentations. To provide a clear overview and to ease navigation within the data, I propose the surface map, an abstracted two-dimensional representation using key features of the surface as landmarks. These visualizations are augmented with information about automated segmentation error estimates. The framework provides intuitive and interactive data correction mechanisms, which in turn permit the expeditious creation of high-quality segmentations. While analyzing such segmented synapse data, the formulation of specific research questions is often impossible due to missing insight into the data. I address this problem by designing a generic parameter space for segmented structures from biological image data. Furthermore, I introduce a graphical interface to aid its exploration, combining both parameter selection as well as data representation.

A Generic Framework for Information Segmentation in Document Images: A part-based Approach (2016)

Sheraz Ahmed

This thesis presents a novel, generic framework for information segmentation in document images. A document image contains different types of information, for instance, text (machine printed/handwritten), graphics, signatures, and stamps. It is necessary to segment information in documents so that to process such segmented information only when required in automatic document processing workflows. The main contribution of this thesis is the conceptualization and implementation of an information segmentation framework that is based on part-based features. The generic nature of the presented framework makes it applicable to a variety of documents (technical drawings, magazines, administrative, scientific, and academic documents) digitized using different methods (scanners, RGB cameras, and hyper-spectral imaging (HSI) devices). A highlight of the presented framework is that it does not require large training sets, rather a few training samples (for instance, four pages) lead to high performance, i.e., better than previously existing methods. In addition, the presented framework is simple and can be adapted quickly to new problem domains. This thesis is divided into three major parts on the basis of document digitization method (scanned, hyper-spectral imaging, and camera captured) used. In the area of scanned document images, three specific contributions have been realized. The first of them is in the domain of signature segmentation in administrative documents. In some workflows, it is very important to check the document authenticity before processing the actual content. This can be done based on the available seal of authenticity, e.g., signatures. However, signature verification systems expect pre-segmented signature image, while signatures are usually a part of document. To use signature verification systems on document images, it is necessary to first segment signatures in documents. This thesis shows that the presented framework can be used to segment signatures in administrative documents. The system based on the presented framework is tested on a publicly available dataset where it outperforms the state-of-the-art methods and successfully segmented all signatures, while less than half of the found signatures are false positives. This shows that it can be applied for practical use. The second contribution in the area of scanned document images is segmentation of stamps in administrative documents. A stamp also serves as a seal for documents authenticity. However, the location of stamp on the document can be more arbitrary than a signature depending on the person sealing the document. This thesis shows that a system based on our generic framework is able to extract stamps of any arbitrary shape and color. The evaluation of the presented system on a publicly available dataset shows that it is also able to segment black stamps (that were not addressed in the past) with a recall and precision of 83% and 73%, respectively. %Furthermore, to segment colored stamps, this thesis presents a novel feature set which is based on intensity gradient, is able to extract unseen, colored, arbitrary shaped, textual as well as graphical stamps, and outperforms the state-of-the-art methods. The third contribution in the scanned document images is in the domain of information segmentation in technical drawings (architectural floorplans, maps, circuit diagrams, etc.) containing usually a large amount of graphics and comparatively less textual components. Further, as in technical drawings, text is overlapping with graphics. Thus, automatic analysis of technical drawings uses text/graphics segmentation as a pre-processing step. This thesis presents a method based on our generic information segmentation framework that is able to detect the text, which is touching graphical components in architectural floorplans and maps. Evaluation of the method on a publicly available dataset of architectural floorplans shows that it is able to extract almost all touching text components with precision and recall of 71% and 95%, respectively. This means that almost all of the touching text components are successfully extracted. In the area of hyper-spectral document images, two contributions have been realized. Unlike normal three channels RGB images, hyper-spectral images usually have multiple channels that range from ultraviolet to infrared regions including the visible region. First, this thesis presents a novel automatic method for signature segmentation from hyper-spectral document images (240 spectral bands between 400 - 900 nm). The presented method is based on a part-based key point detection technique, which does not use any structural information, but relies only on the spectral response of the document regardless of ink color and intensity. The presented method is capable of segmenting (overlapping and non-overlapping) signatures from varying backgrounds like, printed text, tables, stamps, logos, etc. Importantly, the presented method can extract signature pixels and not just the bounding boxes. This is substantial when signatures are overlapping with text and/or other objects in image. Second, this thesis presents a new dataset comprising of 300 documents scanned using a high-resolution hyper-spectral scanner. Evaluation of the presented signature segmentation method on this hyper-spectral dataset shows that it is able to extract signature pixels with the precision and recall of 100% and 79%, respectively. Further contributions have been made in the area of camera captured document images. A major problem in the development of Optical Character Recognition (OCR) systems for camera captured document images is the lack of labeled camera captured document images datasets. In the first place, this thesis presents a novel, generic, method for automatic ground truth generation/labeling of document images. The presented method builds large-scale (i.e., millions of images) datasets of labeled camera captured / scanned documents without any human intervention. The method is generic and can be used for automatic ground truth generation of (scanned and/or camera captured) documents in any language, e.g., English, Russian, Arabic, Urdu. The evaluation of the presented method, on two different datasets in English and Russian, shows that 99.98% of the images are correctly labeled in every case. Another important contribution in the area of camera captured document images is the compilation of a large dataset comprising 1 million word images (10 million character images), captured in a real camera-based acquisition environment, along with the word and character level ground truth. The dataset can be used for training as well as testing of character recognition systems for camera-captured documents. Various benchmark tests are performed to analyze the behavior of different open source OCR systems on camera captured document images. Evaluation results show that the existing OCRs, which already get very high accuracies on scanned documents, fail on camera captured document images. Using the presented camera-captured dataset, a novel character recognition system is developed which is based on a variant of recurrent neural networks, i.e., Long Short Term Memory (LSTM) that outperforms all of the existing OCR engines on camera captured document images with an accuracy of more than 95%. Finally, this thesis provides details on various tasks that have been performed in the area closely related to information segmentation. This includes automatic analysis and sketch based retrieval of architectural floor plan images, a novel scheme for online signature verification, and a part-based approach for signature verification. With these contributions, it has been shown that part-based methods can be successfully applied to document image analysis.

Advances in Theory and Applicability of Stochastic Network Calculus (2016)

Michael Beck

Stochastic Network Calculus (SNC) emerged from two branches in the late 90s: the theory of effective bandwidths and its predecessor the Deterministic Network Calculus (DNC). As such SNC’s goal is to analyze queueing networks and support their design and control. In contrast to queueing theory, which strives for similar goals, SNC uses in- equalities to circumvent complex situations, such as stochastic dependencies or non-Poisson arrivals. Leaving the objective to compute exact distributions behind, SNC derives stochastic performance bounds. Such a bound would, for example, guarantee a system’s maximal queue length that is violated by a known small prob- ability only. This work includes several contributions towards the theory of SNC. They are sorted into four main contributions: (1) The first chapters give a self-contained introduction to deterministic net- work calculus and its two branches of stochastic extensions. The focus lies on the notion of network operations. They allow to derive the performance bounds and simplifying complex scenarios. (2) The author created the first open-source tool to automate the steps of cal- culating and optimizing MGF-based performance bounds. The tool automatically calculates end-to-end performance bounds, via a symbolic approach. In a second step, this solution is numerically optimized. A modular design allows the user to implement their own functions, like traffic models or analysis methods. (3) The problem of the initial modeling step is addressed with the development of a statistical network calculus. In many applications the properties of included elements are mostly unknown. To that end, assumptions about the underlying processes are made and backed by measurement-based statistical methods. This thesis presents a way to integrate possible modeling errors into the bounds of SNC. As a byproduct a dynamic view on the system is obtained that allows SNC to adapt to non-stationarities. (4) Probabilistic bounds are fundamentally different from deterministic bounds: While deterministic bounds hold for all times of the analyzed system, this is not true for probabilistic bounds. Stochastic bounds, although still valid for every time t, only hold for one time instance at once. Sample path bounds are only achieved by using Boole’s inequality. This thesis presents an alternative method, by adapting the theory of extreme values. (5) A long standing problem of SNC is the construction of stochastic bounds for a window flow controller. The corresponding problem for DNC had been solved over a decade ago, but remained an open problem for SNC. This thesis presents two methods for a successful application of SNC to the window flow controller.

An Adaptive and Dynamic Simulation Framework for Incremental, Collaborative Classifier Fusion (2016)

Gernot Bahle Andreas Poxrucker George Kampis Paul Lukowicz

Abstract. To investigate incremental collaborative classifier fusion techniques, we have developed a comprehensive simulation framework. It is highly flexible and customizable, and can be adapted to various settings and scenarios. The toolbox is realized as an extension to the NetLogo multi-agent based simulation environment using its comprehensive Java- API. The toolbox has been integrated in two di↵erent environments, one for demonstration purposes and another, modeled on persons using re- alistic motion data from Zurich, who are communicating in an ad hoc fashion using mobile devices.

Symbolic Simulation of Mixed-Signal Systems with Extended Affine Arithmetic (2016)

Carna Radojicic

Mixed-signal systems combine analog circuits with digital hardware and software systems. A particular challenge is the sensitivity of analog parts to even small deviations in parameters, or inputs. Parameters of circuits and systems such as process, voltage, and temperature are never accurate; we hence model them as uncertain values (‘uncertainties’). Uncertain parameters and inputs can modify the dynamic behavior and lead to properties of the system that are not in specified ranges. For verification of mixed- signal systems, the analysis of the impact of uncertainties on the dynamical behavior plays a central role. Verification of mixed-signal systems is usually done by numerical simulation. A single numerical simulation run allows designers to verify single parameter values out of often ranges of uncertain values. Multi-run simulation techniques such as Monte Carlo Simulation, Corner Case simulation, and enhanced techniques such as Importance Sampling or Design-of-Experiments allow to verify ranges – at the cost of a high number of simulation runs, and with the risk of not finding potential errors. Formal and symbolic approaches are an interesting alternative. Such methods allow a comprehensive verification. However, formal methods do not scale well with heterogeneity and complexity. Also, formal methods do not support existing and established modeling languages. This fact complicates its integration in industrial design flows. In previous work on verification of Mixed-Signal systems, Affine Arithmetic is used for symbolic simulation. This allows combining the high coverage of formal methods with the ease-of use and applicability of simulation. Affine Arithmetic computes the propagation of uncertainties through mostly linear analog circuits and DSP methods in an accurate way. However, Affine Arithmetic is currently only able to compute with contiguous regions, but does not permit the representation of and computation with discrete behavior, e.g. introduced by software. This is a serious limitation: in mixed-signal systems, uncertainties in the analog part are often compensated by embedded software; hence, verification of system properties must consider both analog circuits and embedded software. The objective of this work is to provide an extension to Affine Arithmetic that allows symbolic computation also for digital hardware and software systems, and to demonstrate its applicability and scalability. Compared with related work and state of the art, this thesis provides the following achievements: 1. The thesis introduces extended Affine Arithmetic Forms (XAAF) for the representation of branch and merge operations. 2. The thesis describes arithmetic and relational operations on XAAF, and reduces over-approximation by using an LP solver. 3. The thesis shows and discusses ways to integrate this XAAF into existing modeling languages, in particular SystemC. This way, breaks in the design flow can be avoided. The applicability and scalability of the approach is demonstrated by symbolic simulation of a Delta-Sigma Modulator and a PLL circuit of an IEEE 802.15.4 transceiver system.

Fachbereich Informatik

Filtern

Autor

Erscheinungsjahr

Dokumenttyp

Sprache

Schlagworte

668 Treffer