004 Datenverarbeitung; Informatik
Refine
Year of publication
- 2009 (13) (remove)
Document Type
- Part of Periodical (6)
- Doctoral Thesis (3)
- Diploma Thesis (2)
- Bachelor Thesis (1)
- Master's Thesis (1)
Language
- English (13) (remove)
Keywords
- Bildverarbeitung (2)
- Akzeptanz (1)
- Automatische Klassifikation (1)
- BPMS (1)
- Bildsegmentierung (1)
- Bluetooth (1)
- CSCW (1)
- Coloskopie (1)
- Computersimulation (1)
- Darmpolyp (1)
Software is vital for modern society. The efficient development of correct and reliable software is of ever-growing importance. An important technique to achieve this goal is deductive program verification: the construction of logical proofs that programs are correct. In this thesis, we address three important challenges for deductive verification on its way to a wider deployment in the industry: 1. verification of thread-based concurrent programs 2. correctness management of verification systems 3. change management in the verification process. These are consistently brought up by practitioners when applying otherwise mature verification systems. The three challenges correspond to the three parts of this thesis (not counting the introductory first part, providing technical background on the KeY verification approach). In the first part, we define a novel program logic for specifying correctness properties of object-oriented programs with unbounded thread-based concurrency. We also present a calculus for the above logic, which allows verifying actual Java programs. The calculus is based on symbolic execution resulting in its good understandability for the user. We describe the implementation of the calculus in the KeY verification system and present a case study. In the second part, we provide a first systematic survey and appraisal of factors involved in reliability of formal reasoning. We elucidate the potential and limitations of self-application of formal methods in this area and give recommendations based on our experience in design and operation of verification systems. In the third part, we show how the technique of similarity-based proof reuse can be applied to the problems of industrial verification life cycle. We address issues (e.g., coping with changes in the proof system) that are important in verification practice, but have been neglected by research so far.
Entwicklung eines Regelungsverfahrens zur Pfadverfolgung für ein Modellfahrzeug mit Sattelanhänger
(2009)
Besides the progressive automation of internal goods traffic, there is an important area that should also be considered. This area is the carriage of goods in selected external areas. The use of driverless trucks in logistic centers can report economic efficiency. In particular, these precise control procedures require that trucks drive on predetermined paths. The general aim of this work is the adaption and evaluation of a path following control method for articulated vehicles. The differences in the kinematic behavior between trucks with one-axle trailer and semi-trailer vehicles will be emphasized. Additionally, the characteristic kinematic properties of semi-trailers for the adaptation of a control procedure will be considered. This control procedure was initially designed for trucks with one-axle trailer. It must work in forwards and backwards movements. This control process will be integrated as a closed component on the control software of the model vehicle. Thus, the geometry of the model vehicle will be specified, and the possible special cases of the control process will be discovered. The work also documents the most relevant software components of the implemented control process.
Colonoscopy is the gold standard for the detection of colorectal polyps that can progress into cancer. In such an examination, physicians search for polyps in endoscopic images. Thereby polyps can be removed. To support experts with a computer-aided diagnosis system, the University of Koblenz-Landau currently makes some efforts in research different methods for automatic detection. Comparable to traditional pattern recognition systems, features are initially extracted and a classifier is trained on such data. Afterwards, unknown endoscopic images can be classified with the previously trained classifier. This thesis concentrates on the extension of the feature extraction module in the existing system. New detection methods are compared to existing techniques. Several features are implemented, incorporating Graylevel Co-occurrence Matrices, Local Binary Patterns and Discrte Wavelet Transform. Different modifications on those features are applied and evaaluated.
This Thesis contributes by reporting on the current state of diffusion of collaboration information technology (CIT). The investigation concludes, with a high degree of certainty, that today we have a "satisfactory" diffusion level of some level-A CITs (mostly e-Mail, distantly followed by Audio Conferencing), and a "dissatisfactory" diffusion level of higher-level CITs (i.e. those requiring significant collaboration and cooperation among users, like Meeting Support Systems, Group Decision Support Systems, etc.). The potential benefits of the latter seem to be far from fully realised due to lack of user acceptance. This conclusion has gradually developed along the research cycle " it was suggested by Empirical Study I, and tested through Empirical Studies II and III. An additional, unplanned and rather interesting, finding from this study has been the recognition of large [mostly business] reporting on numerous Web 2.0 user-community produced collaboration technologies (most of them belonging to the category of "social software") and their metamorphosis from autonomous, "bottom-up" solutions into enterprise-supported infrastructures. Another contribution of this Thesis " again suggested by Empirical Study I, and tested through Empirical Studies II and III " pertains to the "process structure" of CIT diffusion. I have found that collaboration technology has historically diffused following two distinct (interdependent but orthogonal) diffusion paths " top-down (authority-based) and bottom-up. The authority-based diffusion path seems to be characterised by efforts aimed at "imposing" technologies on employees, the primary concern being to make sure that technology seamlessly and easily integrates into the organisational IT infrastructure. On the other hand, the bottom-up diffusion trail seems to be successful. The contribution of this investigation may be summarised as threefold: 1. This investigation consolidates most of the findings to date, pertaining to CIT adoption and diffusion, which have been produced by the CIT research community. Thus, it tells a coherent story of the dynamics of the community focus and the collective wisdom gathered over a period of (at least) one decade. 2. This work offers a meaningful framework within which to analyse existing knowledge " and indeed extends that knowledge base by identifying persistent problems of collaboration technology acceptance, adoption and diffusion. These problems have been repeatedly observed in practice, though the pattern does not seem to have been recognised and internalised by the community. Many of these problems have been observed in cases of CIT use one decade ago, five years ago, three years ago, and continue to be observed today in structurally the same form despite what is unarguably "rapid technological development". This gives me reason to believe that, at least some of the persistent problems of CIT diffusion can be hypothesised as "determining factors". My contribution here is to identify these factors, discuss them in detail, and thus tackle the theme of CIT diffusion through a structured historical narrative. 3. Through my contribution (2) above, I characterise a "knowledge-action gap" in the field of CIT and illuminate a potential path through which the research community might hope to bridge this gap. The gap may be operationalised as cognitive distance between CIT "knowledge" and CIT "action".
The STOR project aims at the development of a scientific component system employing models and knowledge for object recognition in images. This interim report elaborates on the requirements for such a component system, structures the application area by identifying a large set of basic operations, and shows how a set of appropriate data structures and components can be derived. A small case studies exemplifies the approach.
An empirical study to evaluate the location of advertisement panels by using a mobile marketing tool
(2009)
The efficiency of marketing campaigns is a precondition for business success. This paper discusses a technique to transfer advertisement content vie Bluetooth technology and collects market research information at the same time. Conventional advertisement media were enhanced by devices to automatically measure the number, distance, frequency and exposure time of passersby, making information available to evaluate both the wireless media as well as the location in general. This paper presents a study analyzing these data. A cryptographic one-way function protects privacy during data acquisition.
This thesis focuses on the utilization of modern graphics hardware (GPU) for visualization and computation purposes, especially of volumetric data from medical imaging. The considerable increase in raw computing power in recent years has turned commodity systems into high-performance workstations. In combination with the direct rendering capabilities of graphics hardware, "visual computing" and "computational steering" approaches on large data sets have become feasible. In this regard several example applications and concepts such as the "ray textures" have been developed and are discussed in detail. As the amount of data to be processed and visualized is steadily increasing, memory and bandwidth limitations require compact representations of the data. While the compression of image data has been investigated extensively in the past, the thesis addresses possibilities of performing computations directly on the compressed data. Therefore, different categories of algorithms are identified and represented in the wavelet domain. By using special variants of the compressed format, efficient implementations of essential image processing algorithms are possible and demonstrate the potential of the approach. From the technical perspective, the GPU-based framework "Cascada" has been developed in the course of this thesis. The introduction of object-oriented concepts to shader programming, as well as a hierarchical representation of computation and/or visualization procedures led to a simplified utilization of graphics hardware while maintaining competitive performance. This is shown with different implementations throughout the contributions, as well as two clinical projects in the field of diagnosis assistance. On the one hand the semi-automatic segmentation of low-resolution MRI data sets of the human liver is evaluated. On the other hand different possibilities in assessing abdominal aortic aneurysms are discussed; both projects make use of graphics hardware. In addition, "Cascada" provides extensions towards recent general-purpose programming architectures and a modular design for future developments.
This thesis evaluates automated techniques to remove objects from an image and proposed several modifications for the specific application of removing a colour checker from structure dominated images. The selection of approaches covers the main research field of image inpainting as well as an approach used in medical image processing. Their results are investigated to disclose their applicability to removing objects from structure-intense images. The advantages and disadvantages discovered in the process are then used to propose several modifications for an adapted inpainting approach suitable for removing the colour checker.
Hybrid systems are the result of merging the two most commonly used models for dynamical systems, namely continuous dynamical systems defined by differential equations and discrete-event systems defined by automata. One can view hybrid systems as constrained systems, where the constraints describe the possible process flows, invariants within states, and transitions on the one hand, and to characterize certain parts of the state space (e.g. the set of initial states, or the set of unsafe states) on the other hand. Therefore, it is advantageous to use constraint logic programming (CLP) as an approach to model hybrid systems. In this paper, we provide CLP implementations, that model hybrid systems comprising several concurrent hybrid automata, whose size is only straight proportional to the size of the given system description. Furthermore, we allow different levels of abstraction by making use of hierarchies as in UML statecharts. In consequence, the CLP model can be used for analyzing and testing the absence or existence of (un)wanted behaviors in hybrid systems. Thus in summary, we get a procedure for the formal verification of hybrid systems by model checking, employing logic programming with constraints.
In recent years, traceability has been more and more universally accepted as being a key factor for the success of software development projects. However, the multitude of different, not well-integrated taxonomies, approaches and technologies impedes the application of traceability techniques in practice. This paper presents a comprehensive view on traceability, pertaining to the whole software development process. Based on graph technology, it derives a seamless approach which combines all activities related to traceability information, namely definition, recording, identification, maintenance, retrieval, and utilization in one single conceptual framework. The presented approach is validated in the context of the ReDSeeDS-project aiming at requirements-based software reuse.