Refine
Document Type
- Doctoral Thesis (4) (remove)
Keywords
- Optimierung (4) (remove)
Faculty / Organisational entity
Most software systems are described in high-level model or programming languages. Their runtime behavior, however, is determined by the compiled code. For uncritical software, it may be sufficient to test the runtime behavior of the code. For safety-critical software, there is an additional aggravating factor resulting from the fact that the code must satisfy the formal specification which reflects the safety policy of the software consumer and that the software producer is obliged to demonstrate that the code is correct with respect to the specification using formal verification techniques. In this scenario, it is of great importance that static analyses and formal methods can be applied on the source code level, because this level is more abstract and better suited for such techniques. However, the results of the analyses and the verification can only be carried over to the machine code level, if we can establish the correctness of the translation. Thus, compilation is a crucial step in the development of software systems and formally verified translation correctness is essential to close the formalization chain from high-level formal methods to the machine-code level. In this thesis, I propose an approach to certifying compilers which achieves the aim of closing the formalization chain from high-level formal methods to the machine-code level by applying techniques from mathematical logic and programming language semantics. I propose an approach called foundational translation validation (FTV) in which the software producer implements an FTV system comprising a compiler and a specification and verification framework (SVF) which is implemented in higher-order logic (HOL). The most important part of the SVF is an explicit translation contract which comprises the formalizations of the source and the target languages of the compiler and the formalization of a binary translation correctness predicate corrTrans(S,T) for source programs S and target programs T. The formalizations of the languages are realized as deep embeddings in HOL. This enables one to declare the whole program in a formalized language as a HOL constant. The predicate formally specifies when T is considered to be a correct translation of S. Its definition is explicitly based on the program semantics definitions provided by the translation contract. Subsequent to the translation, the compiler translates the source and the target programs into their syntactic representations as HOL constants, S and T, and generates a proof of corrTrans(S,T). We call a compiler which follows the FTV approach a proof generating compiler. Our approach borrows the idea of representing programs in correctness proofs as logic constants from the foundational proof-carrying code (FPCC) approach. Novel features that distinquish our approach from further approaches to certifying compilers, such as proof-carrying code (PCC) and translation validation (TV) are the following: Firstly, the presence of an explicit translation contract formalized in HOL: The approaches PCC and TV do not formalize a translation contract explicitly. Instead of this, they incorporate operational semantics and translation correctness criterion in translation validation tools on the programming language level. Secondly, representation of programs in correctness proofs as logic constants: The approaches PCC and the TV translate programs into their representations as semantic abstractions that serve as inputs for translation validation tools. Thirdly, certification of program transformation chains: Unlike the TV approach, which certifies single program transformations, the FTV approach achieves the aim of certifying whole chains of program transformations. This is possible due to the fact that the translation contract provides, for all programming languages involved in the program transformation chain, definitions of program semantics functions which map programs to mathematical objects that are elements of a set with an (at least) partial order "<=". Then, the proof makes use of the fact that the relation "<=" is transitive. In this thesis, the feasibility of the FTV approach is exemplified by the implementation of an FTV system. The system comprises a compiler front-end that certifies its optimization phase and an accompanying SVF that is implemented in the theorem prover Isabelle/HOL. The compiler front-end translates programs in a small C-like programming language, performs three optimizations: constant folding, dead assignment elimination, and loop invariant hoisting, and generates translation certificates in the form of Isabelle/HOL theories. The main focus of the thesis is on the description of the SVF and its translation verification techniques.
Die über mehr als 100 Jahre gewachsenen komplexen Strukturen der Wasserver- und Abwasserentsorgungssysteme müssen sich zunehmend neuen Herausforderungen stellen. Die Forderung nach einer Anpassung hin zu flexiblen und nachhaltigen Systemen bedingt einen hohen Neu- und Umbaubedarf im Bestand. Als Alternativen und Ergänzung bestehender Systeme werden neben einer naturnahen Regenwasserbewirtschaftung auch Neuartige Sanitärsysteme diskutiert. Eine Umstellung bestehender Systeme auf Siedlungsebene findet hierbei allerdings äußert selten statt. Hierfür ist die Erarbeitung von Umgestaltungsstrategien erforderlich, um finanzielle Mittel und ökologischen Nutzen zu optimieren.
In dieser Arbeit wird ein multi-kriterielles lineares Optimierungsmodell genutzt, in dem Methoden der Projektplanungs- und Netzwerkflussprobleme verknüpft werden. Als wesentliche Nebenbedingung wird die Einhaltung der Funktionsfähigkeit der sich wandelnden Systeme und als Zielfunktionen werden ökonomische und ökologische Kosten eingeführt. Lösungen des formulierten mathematischen Problems sind Pareto-optimale funktionsfähige und zulässige Strategien der weitreichenden Integration einer ressourcenorientierten Abwasserbewirtschaftung. Als Ergebnis liegt ein Instrument vor, dass die Entscheidungsfindung zur Umgestaltung von bestehenden siedlungswasserwirtschaftlichen Infrastrukturen unterstützt und mögliche Kosten und Folgewirkungen zeitlich und räumlich differenziert aufzeigen kann.
Das Optimierungsmodell wurde an zwei Untersuchungsgebieten angewandt und optimale Umgestaltungsstrategien zu unterschiedlichen nachhaltigen Zielzuständen analysiert sowie eine Sensitivitätsanalyse bezüglich wichtiger Optimierungsparameter durchgeführt. Die Ergebnisse zeigen, dass die generelle Umsetzbarkeit einer weitreichenden Teilstromseparation gewährleistet ist, wenn neue Elemente zur Bewirtschaftung, Behandlung und Ableitung zeitlich optimiert integriert werden. Mögliche Umgestaltungen werden keine linearen Anpassungen an Zielwerte, Veränderungen von Umweltauswirkungen oder Kostenflüsse verursachen. Es ergeben sich vielmehr über den Umsetzungszeitraum veränderliche Verläufe, die je nach Zielgewichtung von ökonomischen und ökologischen Kosten große Wirkungen zu Beginn oder zum Ende der Betrachtungsdauer zeigen. Vor allem die Gewichtung der beiden Kosten und die Auswahl der zu minimierenden ökologischen Kriterien haben einen großen Einfluss auf die gefundenen Umgestaltungsstrategien. Die jeweiligen Empfehlungen zum Umgestaltungszeitraum, der Zielgewichtung und zur allgemeinen Vorgabe der Optimierungskriterien leiten sich vor allem aus der Veranlassung für eine Systemumgestaltung ab. Die für den spezifischen Anwendungsfall optimale Umgestaltungsstrategie kann sich nur durch Diskussion mit den Entscheidungsträgern vor Ort ergeben. Das Modell hat sich hierbei als sehr gut geeignetes Werkzeug zur Analyse der Systeme herausgestellt.
Es konnte gezeigt werden, dass eine Erweiterung derzeitiger Bewertungsmethoden hin zu Methoden, die zeitlich und räumlich differenzierte Aussagen für den ökologischen und ökonomischen Zustand ermöglichen, erforderlich ist. Die alleinige Planung und Betrachtung des zukünftigen Systemzustandes ist nicht ausreichend zur Beurteilung der Wirkungen einer weitreichenden Implementierung ressourcenorientierter Abwasserbewirtschaftung.
The main two problems of continuous-time financial mathematics are option pricing and portfolio optimization. In this thesis, various new aspects of these major topics of financial mathematics will be discussed. In all our considerations we will assume the standard diffusion type setting for securitiy prices which is today well-know under the term "Black-Scholes model". This setting and the basic results of option pricing and portfolio optimization are surveyed in the first chapter. The next three chapters deal with generalizations of the standard portfolio problem, also know as "Merton's problem". Here, we will always use the stochastic control approach as introduced in the seminal papers by Merton (1969, 1971, 1990). One such problem is the very realistic setting of an investor who is faced with fixed monetary streams. More precisely, in addition to maximizing the utility from final wealth via choosing an investment strategy, the investor also has to fulfill certain consumption needs. Also the opposite situation, an additional income stream can now be taken into account in our portfolio optimization problem. We consider various examples and solve them on one hand via classical stochastic control methods and on the other hand by our new separation theorem. This together with some numerical examples forms Chapter 2. Chapter 3 is mainly concerned with the portfolio problem if the investor has different lending and borrowing rates. We give explicit solutions (where possible) and numerical methods to calculate the optimal strategy in the cases of log utility and HARA utility for three different modelling approaches of the dependence of the borrowing rate on the fraction of wealth financed by a credit. The further generalization of the standard Merton problem in Chapter 4 consists in considering simultaneously the possibilities for continuous and discrete consumption. In our general approach there is a possibility for assigning the different consumption times different weights which is a generalization of the usual way of making them comparable via discounting. Chapter 5 deals with the special case of pricing basket options. Here, the main problem is not path-dependence but the multi-dimensionality which makes it impossible to give usuefull analytical representations of the option price. We review the literature and compare six different numerical methods in a systematic way. Thereby we also look at the influence of various parameters such as strike, correlation, forwards or volatilities on the erformance of the different numerical methods. The problem of pricing Asian options on average spot with average strike is the topic of Chapter 6. We here apply the bivariate normal distribution to obtain an approximate option price. This method proves to be very reliable and e±cient for the valuation of different variants of Asian options on average spot with average strike.
Die enorme Nachfrage nach neuartigen Naturstoffen sowie Leitstrukturen für die (Teil-) Synthese pharmazeutischer Produkte verlangt ständig nach neuen Innovationen. Ein bedeutender Impuls ist dabei von der Marinen Biotechnologie zu erwarten, die seit einigen Jahren versucht, die sich bietenden medizinischen Potentiale auszuschöpfen. So können neuartige Wirkstoffe bzw. die für deren Produktion verantwortlichen Organismen und Enzyme isoliert und bereitgestellt werden. Häufig ist das Wachstum der Organismen jedoch stark limitiert sowie eine Produktion der Ziel-Metabolite nur unter bestimmten Bedingungen möglich, weshalb ein enormes Interesse an neuen Optimiermethoden zur Lösung des Problems besteht. Neuartige Lösungsansätze sollten daher im Rahmen dieser Arbeit verfolgt werden. Untersucht wurde eine „biochemische“ Wachstums- und Produktionsoptimierung mariner Bakterien durch einen Zusatz von Homoserinlactonen zum Kultivierungsmedium. Dabei konnte neben einem verbesserten Wachstum diverser Prokaryonten eine leichte Variation im Metabolitspektrum ermittelt sowie eine geringfügig erhöhte Produktion biologisch aktiver Substanzen detektiert werden. Soll das Wachstum von (marinen) Mikroorganismen optimiert werden, wird vom Anwender häufig eine unstrukturierte one-factor-at-a-time-Methode angewendet. Da diese in der Regel keine Beeinflussung der zu optimierenden variablen Parameter beachtet, wurden in dieser Arbeit alternativ rechnergestützte Optimierungen zur Umgehung dieses Problems durchgeführt. Zum Einsatz kam dabei eine Kombination aus einem Genetischen Algorithmus, welcher die Identifikation des globalen Optimums erlaubt und einem Simplex-Algorithmus, der zur Verfeinerung des bereits aufgefundenen Optimums dient. Hiermit konnte die Produktion einer marinen L-Serindehydratase im Rahmen einer Nährmediumsoptimierung um mehr als 50 % im Vergleich zum Referenzmedium gesteigert werden. Des Weiteren wurde ein im Polyketidscreening positiv aufgefallenes Bakterium (Halomonas marina) als Modellorganismus für ein neuartiges rechnergestütztes Verfahren eingesetzt, welches eine schnelle Identifizierung der Güte von Wachstumsparametern erlaubt und dabei eine repetitiv geführte Batch-Betriebsweise von Bioreaktoren nutzt. Ein weiterer Schwerpunkt dieser Arbeit ist die Charakterisierung einer rekombinant exprimierten Tryptophan-5-Halogenase. Hierbei konnte nach der Identifizierung des Aktivitätsoptimums hinsichtlich des einzustellenden pH-Werts sowie der Temperatur die Halbwertszeit des Enzyms bei verschiedenen Temperaturen bestimmt und mittels 2 D-Gelelektrophorese der pI-Wert des Enzyms erstmalig determiniert werden. Ein Fokus dieser Untersuchungen lag auf der Optimierung der Enzymkinetik. Dabei konnte insgesamt eine Verbesserung der Ausbeute um den Faktor 1,6 erzielt werden.
