Filtern
Erscheinungsjahr
- 2007 (145) (entfernen)
Dokumenttyp
- Dissertation (64)
- Bericht (37)
- Preprint (14)
- Teil eines Periodikums (13)
- Studienarbeit (5)
- Arbeitspapier (4)
- Diplomarbeit (3)
- Wissenschaftlicher Artikel (2)
- Konferenzveröffentlichung (2)
- Habilitation (1)
Schlagworte
- Phasengleichgewicht (4)
- numerical upscaling (4)
- Dienstgüte (3)
- Elastoplastizität (3)
- Model checking (3)
- Networked Automation Systems (3)
- Netzwerk (3)
- Response-Zeit (3)
- Visualisierung (3)
- hub location (3)
Fachbereich / Organisatorische Einheit
- Fachbereich Mathematik (34)
- Fraunhofer (ITWM) (28)
- Fachbereich Maschinenbau und Verfahrenstechnik (20)
- Fachbereich Informatik (19)
- Fachbereich Sozialwissenschaften (10)
- Fachbereich Chemie (9)
- Fachbereich ARUBI (6)
- Fachbereich Biologie (6)
- Fachbereich Elektrotechnik und Informationstechnik (5)
- Fachbereich Wirtschaftswissenschaften (5)
Nichtlinearer Horizontaler Bettungsmodulansatz für Trägerbohlwände in mitteldicht gelagertem Sand
(2007)
In der allgemeinen Baugrubenstatik für Trägerbohlwände werden haltende Kräfte vor dem im Baugrund einbindenden Teil des Trägers dem Erdwiderstand gleichgesetzt. Der Erwiderstand kann jedoch nur im Grenzzustand vollständig mobilisiert werden, was ausreichend große Verschiebungen am Trägerfuß voraussetzt. Die Abhängigkeit der tatsächlich mobilisierten Erdwiderstandsspannungen von den Verschiebungen kann mathematisch durch den hori-zontalen Bettungsmodul ausgedrückt werden. Bislang liegen zum horizontalen Bettungsmodul nur grobe Näherungsansätze vor, die die tatsächlichen Wechselwirkungen zwischen Spannun-gen und Verschiebungen für beliebige Verschiebungsbilder nicht realitätsnah erfassen. Ziel dieser Arbeit ist eine realitätsnahe Beschreibung des horizontalen Bettungsmoduls und damit einer realistischere Berechnung des Trag- und Verformungsverhaltens von Trägerbohl-wänden. Zur Ermittlung des Bettungsmoduls in Größe und Verlauf sowie zur Untersuchung von Einflussfaktoren auf den Bettungsmodul werden dreidimensionale Berechnungen nach der Finiten-Elemente-Methode (FEM) durchgeführt. Dabei werden die maßgebendenden Einfluss-faktoren im Rahmen von Parameterstudien für in der Praxis häufig vorkommende Werte-intervalle untersucht. Die FEM-Berechnungen erfolgen für freistehende, einfach rückverankerte und zweifach rückverankterte Trägerbohlwände in mitteldicht gelagertem Sand. Den Berechnungen liegt ein nichtlineares, elastoplastisches Stoffgesetz zugrunde. Die FEM-Berechnungen werden an den Messergebnissen vorhandener Großversuche kalibriert. Die FEM-Parameterstudien belegen eine Abhängigkeit des Bettungsmoduls von der Verschiebung u, der Tiefe z/t und der Druckflächenbreite b. Aus den FEM-Parameterstudien abgeleitet wird ein iterativer, nichtlinearer Berechnungsansatz für den horizontalen Bettungsmodul ksh erarbeitet. Darüber hinaus wird als Anfangswert der Iteration in der Ingenieurpraxis ein einfacher, linearer Näherungsansatz für den horizontalen Bettungsmodul ermittelt.
Software stellt ein komplexes Werkzeug dar, das durch seine umfassenden Möglichkeiten die moderne Gesellschaft entscheidend geprägt hat. Daraus ergibt sich eine Abhängigkeit von Funktion und Fehlfunktion der Software, die eine an den funktionalen Anforderungen orientierte Entwicklung und Qualitätssicherung der Software notwendig macht. Die vorliegende Arbeit schafft durch Formalisierung und Systematisierung der Verfahren im funktionsorientierten Test eine fundierte Basis für eine Hinwendung zu den funktionsorientierten Techniken in Softwareentwicklung und –qualitätssicherung. Hierzu wird in der Arbeit zunächst ein formales Modell für das Vorgehen im dynamischen Test beschrieben, das sich an der Begriffsbildung der Literatur und dem Verständnis der Praxis orientiert. Das Modell beruht auf wenigen zentralen Annahmen, eignet sich für formale Untersuchungen und Nachweise und ist wegen seiner sehr allgemein gehaltenen Definitionen breit anwendbar und einfach erweiterbar. Auf dieser Basis werden Vorgehen und Verfahren zum funktionsorientierten Test analysiert. Zunächst wird dazu das Vorgehen im funktionsorientierten Test im Rahmen des Modells dargestellt. Darauf aufbauend werden zentrale Verfahren des funktionsorientierten Tests analysiert, die zum Gegenstand die systematische Prüfung der Umsetzung von weitgehend informal beschriebenen Anforderungen in einem Softwareprodukt haben. Betrachtet werden Verfahren der funktionalen Partitionierung, der funktionalen Äquivalenzklassenanalyse und Grenzwertbildung, Verfahren zur Prüfung von kausalen Zusammenhängen zwischen Ursachen und Wirkungen, Verfahren zur Prüfung von graphisch spezifizierter Funktionalität in Syntaxdiagrammen, Aktivitätsdiagrammen, Sequenz- und Kollaborationsdiagrammen und Petrinetzen, Verfahren zum Test zustandsbasierter Systeme sowie Ansätze einer funktionalen Dekomposition. Die Analyse und Diskussion der bekannten Verfahren im formalisierten Rahmenwerk führt zu zahlreichen Ergebnissen und Verfahrensergänzungen. So zeigt sich, dass in den klassischen, informalen Beschreibungen häufig Unklarheiten bestehen. Diese werden hier adressiert und durch Angabe von Kriterien präzisiert, Optimierungsmöglichkeiten werden aufgezeigt. Darüber hinaus wird an der einheitlichen formalen Darstellung der in der Literatur meist separat betrachteten Verfahren deutlich, welche Vergleichbarkeit zwischen den Verfahren besteht, welche Verfahrenskombinationen sinnvoll sind und wie durch ein kombiniert funktions- und strukturorientiertes Vorgehen eine hohe Aussagekraft in der analytischen Qualitätssicherung erreicht werden kann. Bei der Formulierung der Verfahren im Rahmen des Modells wird herausgearbeitet, wo zur Verfahrensdurchführung die kreative Leistung des Testers notwendig ist und welche Anteile formalisiert und damit automatisiert unterstützt werden können. Diese Betrachtungen bilden die Grundlage für die Skizzierung einer integrierten Entwicklungsumgebung, in der ein funktionsorientiertes Vorgehen in Entwicklung und Qualitätssicherung umgesetzt wird: Hier helfen funktionsorientierte Beschreibungsformen bei der Angabe der Spezifikation, ihrer Verfeinerung und ihrer Vervollständigung, sie unterstützen die Entwicklung durch Modellbildung, sie liefern die Basis für eine funktionsorientierte Testdatenselektion mit Adäquatheitsprüfung, sie können bei geeigneter Interpretierbarkeit über den Datenbereichen zur automatisierten Testfallgenerierung genutzt werden und unterstützen als suboptimale Testorakel eine automatisierte Auswertung des dynamischen Tests. Diese Skizze zeigt die praktische Umsetzbarkeit der vorwiegend theoretischen Ergebnisse dieser Arbeit und setzt einen Impuls für ein verstärktes Aufgreifen funktionsorientierter Techniken in Wissenschaft und Praxis.
Sepsis ist eine lebensbedrohliche Krankheit und eine der häufigsten Todesursachen auf Intensiv-Stationen. Eine der Hauptursachen für die Schwere dieser Krankheit ist die Lymphopenie, d. h. die apoptotische Depletion von Lymphozyten, die vor allem in der späten hypo-inflammatorischen Phase der Sepsis auftritt. Die dafür verantwortlichen Signalwege sind jedoch nicht im Detail geklärt. Die Liganden-vermittelte Aktivierung von PPARgamma (‚peroxisome proliferator activated receptor gamma’), einem wichtigen Regulator der Immunantwort, führt zur Apoptose in aktivierten T-Zellen. Daher postulierte ich, dass die PPARgamma-vermittelte Apoptose in T-Zellen zur Lymphopenie während der Sepsis beiträgt. Hierbei konnte ich zeigen, dass T-Zellen aus dem peripheren Blut von Sepsis-Patienten eine stark erhöhte PPARgamma-mRNA-Expression zeigten und in vitro stark erhöhte Apoptoseraten infolge einer Liganden-vermittelten PPARgamma-Aktivierung aufwiesen. Die hierfür erforderlichen PPARgamma-Liganden lagen im Plasma von Sepsis-Patienten vor. D. h. die PPARgamma-vermittelte Apoptose in T-Zellen könnte zur nachgewiesenen Lymphopenie während der Sepsis beitragen. Aufgrund der anti-inflammatorischen Wirkung von PPARgamma könnte dessen gezielte Aktivierung in der frühen hyper-inflammatorischen Phase durch Thiazolidindione (TZDs) als synthetische PPARgamma-Aktivatoren therapeutisch interessant sein. Da diese jedoch auch auf PPARgamma-unabhängigen Wegen den Zelltod in T-Zellen induzieren können, war es essentiell, die dafür verantwortlichen Signalwege zu klären. Dabei konnte ich feststellen, dass Ciglitazon Nekrose und Troglitazon Apoptose auf PPARgamma-unabhängigen Wegen bereits nach 4 h in Jurkat T-Zellen induzierten, wohingegen Rosiglitazon keinen Einfluss auf den Zelltod hatte. Die Inkubation der TZDs führte zur Produktion von reaktiven Sauerstoffspezies, welche eine wichtige Rolle bei der Ciglitazon-induzierten Nekrose, jedoch nur marginal bei der Troglitazon-induzierten Apoptose spielten. Durch Studien in submitochondrialen Partikeln konnte ich zeigen, dass die getesteten TZDs den Komplex I der mitochondrialen Atmungskette inhibierten, während nur Ciglitazon und Troglitazon zusätzlich den Komplex II hemmen konnten. Mit Hilfe synthetischer Atmungskette-Inhibitoren konnte ich weiterhin zeigen, dass die Zelltod-Induktion nach Ciglitazon und Troglitazon in Jurkat T-Zellen hauptsächlich auf der Hemmung des Komplexes II beruhte. Da die Ciglitazon-Inkubation zur Depletion des ATP-Gehaltes führte, erfolgte eine Nekrose-Induktion nach Ciglitazon, wohingegen Troglitazon den ATP-Gehalt nicht beeinflusste und daher Apoptose induzierte. Die von mir identifizierten PPARgamma-unabhängigen Mechanismen der Zelltod-Induktion durch TZDs könnten eventuell Nebenwirkungen bei TZD-basierten Therapien erklären.
This dissertation is intended to transport the theory of Serre functors into the context of A-infinity-categories. We begin with an introduction to multicategories and closed multicategories, which form a framework in which the theory of A-infinity-categories is developed. We prove that (unital) A-infinity-categories constitute a closed symmetric multicategory. We define the notion of A-infinity-bimodule similarly to Tradler and show that it is equivalent to an A-infinity-functor of two arguments which takes values in the differential graded category of complexes of k-modules, where k is a commutative ground ring. Serre A-infinity-functors are defined via A-infinity-bimodules following ideas of Kontsevich and Soibelman. We prove that a unital closed under shifts A-infinity-category over a field admits a Serre A-infinity-functor if and only if its homotopy category admits an ordinary Serre functor. The proof uses categories and Serre functors enriched in the homotopy category of complexes of k-modules. Another important ingredient is an A-infinity-version of the Yoneda Lemma.
Zwölf Testpflanzen des Weinbauinstituts Freiburg wurden auf deren Resistenzeigenschaften gegenüber dem Virusvektor Xiphinema index und dem GFLV getestet. Das Hauptziel dieser Arbeit lag in der Entwicklung eines in-vitro-Testsystems für Reben, das detaillierte Einblicke in das Wurzel-Nematoden-System erlaubt. Anhand dieses in-vitro-Testsystems konnten zwei unterschiedliche Reaktionen der Wurzeln dieser Testreben auf die Saugtätigkeit der Nematoden festgestellt werden. Es konnte sowohl eine Gallenbildung als auch eine Nekrosenbildung bei den unterschiedlichen Kreuzungen der Testpflanzen beobachtet werden. Alle Testpflanzen aus verschiedenen Kreuzungen zeigten eine Abwehrreaktion gegenüber den Nematoden. Dies resultierte in Auftreten von Transkripten der Phenylalanin-Ammonium-Lyase (PAL) und der Bildung von Superoxid-Radikalen. Bei zwei V. rotundifolia-Hybriden war zusätzlich die Callose-Synthase aktiv und es kam außerdem zu einer Callose-Deposition an den betroffenen Stellen im Wurzelgewebe. Bis auf Testpflanze 46, einem V. rotundifolia-Hybrid waren alle getesteten Reben nach vier Wochen Versuchsdauer sensitiv für eine Transmission des GFLV. Dieser Hybrid war an den Wurzeln durch die Saugtätigkeit der Nematoden nekrosenbildend und zeigte eine Callose-Synthase-Aktivität. X. index findet seine Wirtspflanzen durch Chemotaxis. Er orientiert sich anhand von Wurzelexudaten, die von Wurzeln ins Medium abgeben werden. Totes Wurzelgewebe kann der Nematode nicht lokalisieren und stellt keinen Stimulus dar. Bei knappem Nahrungsangebot nutzt der Nematode vorhandene Nahrungsressourcen aller Rebsorten mit verschiedenster Beschaffenheit. Mit dem Pflanzenhormon Methyljasmonat behandelte Wurzeln wurden gezielt gemieden. Zwei mit dem GFLV infizierte Rebflächen an verschiedenen Standorten zeigten innerhalb dreijähriger Beobachtung eine Zunahme von virustragenden Rebstöcken. Ein Hinweis auf die Verbreitung durch virusübertragende Nematoden konnte durch Bodenproben bisher nicht bestätigt werden.
Guaranteeing correctness of compilation is a ma jor precondition for correct software. Code generation can be one of the most error-prone tasks in a compiler. One way to achieve trusted compilation is certifying compilation. A certifying compiler generates for each run a proof that it has performed the compilation run correctly. The proof is checked in a separate theorem prover. If the theorem prover is content with the proof, one can be sure that the compiler produced correct code. This paper presents a certifying code generation phase for a compiler translating an intermediate language into assembler code. The time spent for checking the proofs is the bottleneck of certifying compilation. We exhibit an improved framework for certifying compilation and considerable advances to overcome this bottleneck. We compare our implementation featuring the Coq theorem prover to an older implementation. Our current implementation is feasible for medium to large sized programs.
Given a directed graph G = (N,A) with arc capacities u and a minimum cost flow problem defined on G, the capacity inverse minimum cost flow problem is to find a new capacity vector u' for the arc set A such that a given feasible flow x' is optimal with respect to the modified capacities. Among all capacity vectors u' satisfying this condition, we would like to find one with minimum ||u' - u|| value. We consider two distance measures for ||u' - u||, rectilinear and Chebyshev distances. By reduction from the feedback arc set problem we show that the capacity inverse minimum cost flow problem is NP-hard in the rectilinear case. On the other hand, it is polynomially solvable by a greedy algorithm for the Chebyshev norm. In the latter case we propose a heuristic for the bicriteria problem, where we minimize among all optimal solutions the number of affected arcs. We also present computational results for this heuristic.
GPU Stereo Vision
(2007)
To analyze scenery obstacles in robotics applications depth information is very valuable. Stereo vision is a powerful way to extract dense range information out of two camera images. In order to unload the CPU the intensive computation can be moved to GPU, taking advantage of the parallel processing capabilities of todays consumer level graphics hardware. This work shows how an efficient implementation on the GPU can be realized utilizing the NVIDIA Cuda framework.
Die fortschreitende Verbreitung von Ethernet-basierten Strukturen mit dezentralen und verteilten Anwendungen in der Automatisierung führt zu den so genannten netzbasier-ten Automatisierungssystemen (NAS). Diese sind zwar in Anschaffung und Betrieb kostengünstiger, moderner und flexibler als herkömmliche Strukturen, weisen jedoch nicht-deterministische Verzögerungen auf. Die genaue Analyse der resultierenden Antwortzeiten ist somit nicht nur Voraussetzung für den verantwortungsbewussten Einsatz dieser Technologie sondern ermöglicht es auch, bereits im Vorfeld von Umstrukturierungen oder Erweiterungen, Fragen der Verlässlichkeit zu klären. In diesem ersten von zwei Beiträgen wird hierfür zunächst die für die speziellen Bedürfnisse der Strukturbeschreibung von netzbasierten Automatisierungssystemen entwickelte Modellierungssprache DesLaNAS vorgestellt und auf ein einführendes Beispiel angewendet. Im zweiten Beitrag wird darauf aufbauend gezeigt, welchen Einfluss die einzelnen System-komponenten (SPS, Netzwerk, I/O-Karten) sowie netzbedingte Verhaltensmodi wie Synchronisation und die gemeinsame Nutzung von Ressourcen auf die Antwortzeiten des Gesamtsystems haben. Zur Analyse selbst wird die wahrscheinlichkeitsbasierte Modellverifikation (PMC) angewendet.
Modelling languages are important in the process of software development. The suitability of a modelling language for a project depends on its applicability to the target domain. Here, domain-specific languages have an advantage over more general modelling languages. On the other hand, modelling languages like the Unified Modeling Language can be used in a wide range of domains, which supports the reuse of development knowledge between projects. This thesis treats the syntactical and semantical harmonisation of modelling languages and their combined use, and the handling of complexity of modelling languages by providing language subsets - called language profiles - with tailor-made formal semantics definitions, generated by a profile tool. We focus on the widely-used modelling languages SDL and UML, and formal semantics definitions specified using Abstract State Machines.
