Der Einsatz von Seilen im Ingenieurbau ermöglicht häufig konkurrenzlos leichte, widerstandsfähige und zugleich wirtschaftliche Tragwerkslösungen. Voraussetzung hierfür ist eine wirklichkeitsnahe statische Bemessung der Seile. Das Ziel dieser Arbeit ist die Entwicklung eines „Open Source“ Computerprogrammes für die Schnittgrößenberechnung ebener Seilsysteme an zwei Aufhängepunkten. Dafür werden zunächst allgemeine und bemessungsrelevante Aspekte zum Bauteil Seil vorgestellt. Anschließend erfolgt die theoretische Herleitung von drei Berechnungsmodellen, welche für unterschiedliche Belastungsarten ausgelegt sind. Jedes dieser Berechnungsmodelle wird anhand eines praxisnahen Anwendungsbeispiels veranschaulicht. Auf Grundlage der theoretischen Herleitungen wird mithilfe der Mathematiksoftware „MATLAB“ ein Berechnungsprogramm für ebene Seiltragwerke entwickelt. Die Plausibilität dieses Programms wird durch Vergleichsrechnungen mit der Statiksoftware „RFEM“ im Rahmen einer Parameterstudie nachgewiesen. Innerhalb der Plausibilitätskontrolle können größtenteils Abweichungen von weniger als 5 % erzielt werden. Einzelne Versuche zeigen größere Abweichungen. Hierfür werden die Ursachen erschlossen und behoben, bzw. Anwendungsgrenzen definiert, um eine sichere Verwendung des Programms zu gewährleisten.:1 Einführung 10 1.1 Seile im Bauwesen 10 1.2 Zielsetzung 11 1.3 Literaturüberblick und aktueller Wissensstand 12 2 Allgemeine Ausführungen zum Seil 13 2.1 Materialien 13 2.2 Herstellung 14 2.3 Eigenschaften von Drahtseilen 16 2.4 Anwendungsgebiete 27 2.5 Typische Einwirkungen 28 3 Theoretische Betrachtung 36 3.1 Berechnungsmodell für ebene Seiltragwerke 36 3.2 Seil unter Eigengewicht 39 3.3 Seil unter beliebiger vertikaler Belastung 54 3.4 Seil unter beliebiger Belastung in Seilebene 62 3.5 Seil unter reiner Zugbelastung 75 3.6 Biegesteifes Seil 75 3.7 Seil mit nichtlinearem Materialverhalten 77 4 Entwicklung eines Programms zur Berechnung ebener Seiltragwerke 79 4.1 Entwicklung des Programms 79 4.2 Plausibilitätskontrolle 86 5 Zusammenfassung und Ausblick 97 Anhang A: Auszug aus der Zulassung für eine 7-drähtige Spannstahllitze 101 Anhang B: Auszug aus der Zulassung für vorgefertigte Drahtseile 107 Anhang C: Produktdatenblatt Spiralseil 112 Anhang D: Programmcode „SEIL“ 113 Anhang E: Verzeichnis der verwendeten Variablen in Programm „SEIL“ 130 Anhang F: Berechnungsparameter RFEM 136 Anhang G: Übersicht Versuchsreihe zur Herleitung von Gl. 4.3 138 Literaturverzeichnis 141 Normenverzeichnis 144 Bildquellenverzeichnis 146 / The usage of cables for engineering often provides unparalleled lightweight, durable, and economically viable structural solutions. A prerequisite for that is a realistic static design of these cables. The objective of this thesis is the development of an 'open source' computer program for calculating internal forces in planar cable systems with two support points. To achieve this, general and design-relevant aspects for cables are initially presented. Subsequently, three calculation models, each designed for different types of loading, are theoretically derived. Each of these calculation models is demonstrated by a practical application example. Based on the theoretical derivations, a calculation program for planar cable structures is developed by using the software „MATLAB“. The plausibility of this program is verified by comparative calculations with the statics software „RFEM“ in the context of a parameter study. Within the plausibility check, deviations of mostly less than 5% can be reached. A few tests show larger deviations. The causes for these are identified and emended, or application limits are defined to ensure the safe usage of the program.:1 Einführung 10 1.1 Seile im Bauwesen 10 1.2 Zielsetzung 11 1.3 Literaturüberblick und aktueller Wissensstand 12 2 Allgemeine Ausführungen zum Seil 13 2.1 Materialien 13 2.2 Herstellung 14 2.3 Eigenschaften von Drahtseilen 16 2.4 Anwendungsgebiete 27 2.5 Typische Einwirkungen 28 3 Theoretische Betrachtung 36 3.1 Berechnungsmodell für ebene Seiltragwerke 36 3.2 Seil unter Eigengewicht 39 3.3 Seil unter beliebiger vertikaler Belastung 54 3.4 Seil unter beliebiger Belastung in Seilebene 62 3.5 Seil unter reiner Zugbelastung 75 3.6 Biegesteifes Seil 75 3.7 Seil mit nichtlinearem Materialverhalten 77 4 Entwicklung eines Programms zur Berechnung ebener Seiltragwerke 79 4.1 Entwicklung des Programms 79 4.2 Plausibilitätskontrolle 86 5 Zusammenfassung und Ausblick 97 Anhang A: Auszug aus der Zulassung für eine 7-drähtige Spannstahllitze 101 Anhang B: Auszug aus der Zulassung für vorgefertigte Drahtseile 107 Anhang C: Produktdatenblatt Spiralseil 112 Anhang D: Programmcode „SEIL“ 113 Anhang E: Verzeichnis der verwendeten Variablen in Programm „SEIL“ 130 Anhang F: Berechnungsparameter RFEM 136 Anhang G: Übersicht Versuchsreihe zur Herleitung von Gl. 4.3 138 Literaturverzeichnis 141 Normenverzeichnis 144 Bildquellenverzeichnis 146

Predicate abstraction is a key enabling technology for applying model checkers to programs written in mainstream languages. It has been used very successfully for debugging sequential system-level C code. Although model checking was originally designed for analysing concurrent systems, there is little evidence of fruitful applications of predicate abstraction to shared-variable concurrent software. The goal of the present thesis is to close this gap. We propose an algorithmic solution implementing predicate abstraction that targets safety properties in non-recursive programs executed by an unbounded number of threads, which communicate via shared memory or higher-level mechanisms, such as mutexes and broadcasts. As system-level code makes frequent use of such primitives, their correct usage is critical to ensure reliability. Monotonicity - the property that thread actions remain executable when other threads are added to the current global state - is a natural and common feature of human-written concurrent software. It is also useful: if every thread’s memory is finite, monotonicity often guarantees the decidability of safety properties even when the number of running threads is unspecified. In this thesis, we show that the process of obtaining finite-data thread abstrac tions for model checking is not always compatible with monotonicity. Predicate-abstracting certain mainstream asynchronous software such as the ticket busy-wait lock algorithm results in non-monotone multi-threaded Boolean programs, despite the monotonicity of the input program: the monotonicity is lost in the abstraction. As a result, the unbounded thread Boolean programs do not give rise to well quasi-ordered systems [1], for which sound and complete safety checking algorithms are available. In fact, safety checking turns out to be undecidable for the obtained class of abstract programs, despite the finiteness of the individual threads’ state spaces. Our solution is to restore the monotonicity in the abstract program, using an inexpensive closure operator that precisely preserves all safety properties from the (non-monotone) abstract program without the closure. As a second contribution, we present a novel, sound and complete, yet empirically much improved algorithm for verifying abstractions, applicable to general well quasi-ordered systems. Our approach is to gradually widen the set of safety queries during the search by program states that involve fewer threads and are thus easier to decide, and are likely to finalise the decision on earlier queries. To counter the negative impact of "bad guesses", i.e. program states that turn out feasible, the search is supported by a parallel engine that generates such states; these are never selected for widening. We present an implementation of our techniques and extensive experiments on multi-threaded C programs, including device driver code from FreeBSD and Solaris. The experiments demonstrate that by exploiting monotonicity, model checking techniques - enabled by predicate abstraction - scale to realistic programs even of a few thousands of multi-threaded C code lines.

Mathematical models have been used to capture the behaviour of biological systems, from low-level biochemical reactions to multi-scale whole-organ models. Models are typically based on experimentally-derived data, attempting to reproduce the observed behaviour through mathematical constructs, e.g. using Ordinary Differential Equations (ODEs) for spatially-homogeneous systems. These models are developed and published as mathematical equations, yet are of such complexity that they necessitate computational simulation. This computational model development is often performed in an ad hoc fashion by modellers who lack extensive software engineering experience, resulting in brittle, inefficient model code that is hard to extend and reuse. Several Domain Specific Languages (DSLs) exist to aid capturing such biological models, including CellML and SBML; however these DSLs are designed to facilitate model curation rather than simplify model development. We present research into the application of techniques from software engineering to this domain; starting with the design, development and implementation of a DSL, termed Ode, to aid the creation of ODE-based biological models. This introduces features beneficial to model development, such as model verification and reproducible results. We compare and contrast model development to large-scale software development, focussing on extensibility and reuse. This work results in a module system that enables the independent construction and combination of model components. We further investigate the use of software engineering processes and patterns to develop complex modular cardiac models. Model simulation is increasingly computationally demanding, thus models are often created in complex low-level languages such as C/C++. We introduce a highly-efficient, optimising native-code compiler for Ode that generates custom, model-specific simulation code and allows use of our structured modelling features without degrading performance. Finally, in certain contexts the stochastic nature of biological systems becomes relevant. We introduce stochastic constructs to the Ode DSL that enable models to use Stochastic Differential Equations (SDEs), the Stochastic Simulation Algorithm (SSA), and hybrid methods. These use our native-code implementation and demonstrate highly-efficient stochastic simulation, beneficial as stochastic simulation is highly computationally intensive. We introduce a further DSL to model ion channels declaratively, demonstrating the benefits of DSLs in the biological domain. This thesis demonstrates the application of software engineering methodologies, and in particular DSLs, to facilitate the development of both deterministic and stochastic biological models. We demonstrate their benefits with several features that enable the construction of large-scale, reusable and extensible models. This is accomplished whilst providing efficient simulation, creating new opportunities for biological model development, investigation and experimentation.

The research presented in this thesis is aimed at developing reliable information systems through the application of model-driven and formal techniques. These are techniques in which a precise, formal model of system behaviour is exploited as source code. As such a model may be more abstract, and more concise, than source code written in a conventional programming language, it should be easier and more economical to create, to analyse, and to change. The quality of the model of the system can be ensured through certain kinds of formal analysis and fixed accordingly if necessary. Most valuably, the model serves as the basis for the automated generation or configuration of a working system. This thesis provides four research contributions. The first involves the analysis of a proposed modelling language targeted at the model-driven development of information systems. Logical properties of the language are derived, as are properties of its compiled form---a guarded substitution notation. The second involves the extension of this language, and its semantics, to permit the description of workflows on information systems. Workflows described in this way may be analysed to determine, in advance of execution, the extent to which their concurrent execution may introduce the possibility of deadlock or blocking: a condition that, in this context, is synonymous with a failure to achieve the specified outcome. The third contribution concerns the validation of models written in this language by adapting existing techniques of software testing to the analysis of design models. A methodology is presented for checking model consistency, on the basis of a generated test suite, against the intended requirements. The fourth and final contribution is the presentation of an implementation strategy for the language, targeted at standard, relational databases, and an argument for its correctness, based on a simple, set-theoretic semantics for structure and operations.

Automatically generating a program from its specification eliminates a large source of errors that is often unavoidable in a manual approach. While a general purpose code generator is impossible to build, it is possible to build a practical code generator for a specific domain. This thesis investigates the theory behind Booster — a domain specific, object based specification language and automatic code generator. The domain of Booster is information systems — systems that consist of a rich object model in which the objects refer to each other to form a complicated network of associations. The operations of such systems are conceptually simple (changing the attributes of objects, adding or removing new objects and creating or destroying associations) but they are tricky to implement correctly. The thesis focuses on the theoretical foundation of the Booster approach, in particular on three contributions: semantics, model completion, and code generation. The semantics of a Booster model is a single abstract data type (ADT) where the invariants and the methods of all the classes in the model are promoted to the level of the ADT. This is different from the traditional view that considers each class as a separate ADT. The thesis argues that the Booster semantics is a better model of object oriented systems. The second important contribution is the idea of model completion — a process that augments the postconditions of methods with additional predicates that follow from the system’s invariant and the method’s original intention. The third contribution describes a simple but effective code generation technique that is based on interpreting postconditions as executable statements and uses weakest preconditions to ensure that the generated code refines its specification.

Knowledge Management Systems are deployed in organisations of all sizes to support the coordination and control of a range of intellectual assets, and the low cost infrastructures made available by the shift to ‘cloud computing’ looks to only increase the speed and pervasiveness of this move. However, their implementation has not been without its problems, and the development of novel interventions capable of supporting the mundane work of everyday organisational settings has ultimately been limited. A common source of trouble for those formulating such systems is said to be that some proportion of the knowledge held by a setting’s members is hidden from the undirected view of both The Organisation and its analysts - typically characterised as a tacit knowledge - and can therefore go unnoticed during the design and deployment of new technologies. Notwithstanding its utility, overuse of this characterisation has resulted in the inappropriate labelling of a disparate assortment of phenomena, some of which might be more appropriately re-specified as ‘hidden knowledges’: a standpoint which seeks to acknowledge their unspoken character without making any unwarranted claims regarding their cognitive status. Approaches which focus on the situated and contingent properties of the actual work carried out by a setting’s members - such as ethnomethodologically informed ethnography - have shown significant promise as a mechanism for transforming the role played by members’ practices into an explicit topic of study. Specifically they have proven particularly adept at noticing those aspects of members’ work that might ordinarily be hidden from an undirected view, such as the methodic procedures through which we can sometimes mean more than we can say in-just-so-many-words. Here - within the context of gathering the requirements for new Knowledge Management Systems to support the reuse of existing knowledge - the findings from the application of just such an approach are presented in the form of a Pattern Language for Knowledge Management Systems: a descriptive device that lends itself to articulating the role that such hidden knowledges are playing in everyday work settings. By combining these three facets, this work shows that it is possible to take a more meaningful approach towards noticing those knowledges which might ordinarily be hidden from view, and apply our new understanding of them to the design of Knowledge Management Systems that actively engage with the knowledgeable work of a setting’s members.

Despite the association between hippocampal atrophy and a vast array of highly debilitating neurological diseases, such as Alzheimer’s disease and frontotemporal lobar degeneration, tools to accurately and robustly quantify the degeneration of this structure still largely elude us. In this thesis, we firstly evaluate previously-developed hippocampal segmentation methods (FMRIB’s Integrated Registration and Segmentation Tool (FIRST), Freesurfer (FS), and three versions of a Classifier Fusion (CF) technique) on two clinical MR datasets, to gain a better understanding of the modes of success and failure of these techniques, and to use this acquired knowledge for subsequent method improvement (e.g., FIRSTv3). Secondly, a fully automated, novel hippocampal segmentation method is developed, termed Fast Marching for Automated Segmentation of the Hippocampus (FMASH). This combined region-growing and atlas-based approach uses a 3D Sethian Fast Marching (FM) technique to propagate a hippocampal region from an automatically-defined seed point in the MR image. Region growth is dictated by both subject-specific intensity features and a probabilistic shape prior (or atlas). Following method development, FMASH is thoroughly validated on an independent clinical dataset from the Alzheimer’s Disease Neuroimaging Initiative (ADNI), with an investigation of the dependency of such atlas-based approaches on their prior information. In response to our findings, we subsequently present a novel label-warping approach to effectively account for the detrimental effects of using cross-dataset priors in atlas-based segmentation. Finally, a clinical application of MR hippocampal segmentation is presented, with a combined MR-PET analysis of wholefield and subfield hippocampal changes in Alzheimer’s disease and frontotemporal lobar degeneration. This thesis therefore contributes both novel computational tools and valuable knowledge for further neurological investigations in both the academic and the clinical field.

Model checking is an automatic formal verification technique for establishing correctness of systems. It has been widely used in industry for analysing and verifying complex safety-critical systems in application domains such as avionics, medicine and computer security, where manual testing is infeasible and even minor errors could have dire consequences. In our increasingly parallelised world, concurrency has become pivotal and seamlessly woven within programming paradigms, however, extremely challenging when it comes to modelling and establishing correctness of intended behaviour. Tools for model checking concurrent systems face severe limitations due to scalability problems arising from the need to examine all possible interleavings (schedules) of executions of parallel components. Moreover, concurrency poses additional challenges to model checking, giving rise to phenomena such as nondeterminism, deadlock, livelock, etc. In this thesis we focus on adapting and developing novel model-checking techniques for concurrent systems in the setting of the process algebra CSP and its primary model checker FDR. CSP allows for a compact modelling and precise analysis of event-based concurrency, grounded on synchronous message passing as a fundamental mechanism of inter-component communication. In particular, we investigate techniques based on symbolic model checking, static analysis and abstraction, all of them exploiting the compositionality inherent in CSP and targeting to increase the scale of systems that can be tractably analysed. Firstly, we investigate symbolic model-checking techniques based on Boolean satisfiability (SAT), which we adapt for the traces model of CSP. We tailor bounded model checking (BMC), that can be used for bug detection, and temporal k-induction, which aims at establishing inductiveness of properties and is capable of both bug finding and establishing the correctness of systems. Secondly, we propose a static analysis framework for establishing livelock freedom of CSP processes, with lessons for other concurrent formalisms. As opposed to traditional exhaustive state-space exploration, our framework employs a system of rules on the syntax of a process to calculate a sound approximation of its fair/co-fair sets of events. The rules either safely classify a process as livelock-free or report inconclusiveness, thereby trading accuracy for speed. Finally, we develop a series of abstraction/refinement schemes for the traces, stable-failures and failures-divergences models of CSP and embed them into a fully automated and compositional CEGAR framework. For each of those techniques we present an implementation and an experimental evaluation on a set of CSP benchmarks.

No description available.

No description available.