Homosexuality and the United Methodist Church: An Ecclesiological Dilemma

Since 1968 The United Methodist Church has publicly debated the status and roles of homosexual persons in the life of the Church, creating considerable conflict within the Denomination. Academic research on the question of homosexuality and the Church has often focused on theological understandings of homosexuality and on the ways the conflict reflects broader "culture wars" in society. Yet little attention has been given to how the Church's concrete practices and polity toward homosexual persons reflect underlying tensions within the ecclesiological identity of the Denomination. This dissertation proposes that the issue of homosexuality is a critically important case study for exploring the practical ecclesiology of The United Methodist Church. In an effort to identify tensions within contemporary United Methodism's practical ecclesiology, it traces in detail the history of the denominational debate over homosexuality since 1968 and articulates the diverse and often conflicting ecclesiological commitments embedded within that debate. Focusing on the debate itself as a practice of the Church, this dissertation illustrates the ways in which the controversy over sexuality reflects the Denomination's conflicted practical ecclesiology. By examining the rhetoric of the sexuality debates in The United Methodist Church from 1968 to 2008, and by articulating the ecclesiological commitments embedded in those debates, the dissertation reveals a fundamental conflict over interpretations of ecclesial unity. Moreover, the dissertation explores the extent to which the conflict over unity reflects ecclesiological tensions present in John Wesley's own practical ecclesiology; and it asks whether or not contemporary interpretations of United Methodist ecclesiology might provide a normative framework for assessing and resolving the underlying ecclesial conflict at work in sexuality debates. The dissertation concludes by exploring the practice of public narrative as a concrete strategy that might be employed by the Denomination to reconcile the diverging ecclesiological visions within the contemporary church so that a clear and consensual ecclesiology might emerge.

Building Responsive Systems from Physically-correct Specifications

Predictability - the ability to foretell that an implementation will not violate a set of specified reliability and timeliness requirements - is a crucial, highly desirable property of responsive embedded systems. This paper overviews a development methodology for responsive systems, which enhances predictability by eliminating potential hazards resulting from physically-unsound specifications. The backbone of our methodology is the Time-constrained Reactive Automaton (TRA) formalism, which adopts a fundamental notion of space and time that restricts expressiveness in a way that allows the specification of only reactive, spontaneous, and causal computation. Using the TRA model, unrealistic systems - possessing properties such as clairvoyance, caprice, in finite capacity, or perfect timing - cannot even be specified. We argue that this "ounce of prevention" at the specification level is likely to spare a lot of time and energy in the development cycle of responsive systems - not to mention the elimination of potential hazards that would have gone, otherwise, unnoticed. The TRA model is presented to system developers through the CLEOPATRA programming language. CLEOPATRA features a C-like imperative syntax for the description of computation, which makes it easier to incorporate in applications already using C. It is event-driven, and thus appropriate for embedded process control applications. It is object-oriented and compositional, thus advocating modularity and reusability. CLEOPATRA is semantically sound; its objects can be transformed, mechanically and unambiguously, into formal TRA automata for verification purposes, which can be pursued using model-checking or theorem proving techniques. Since 1989, an ancestor of CLEOPATRA has been in use as a specification and simulation language for embedded time-critical robotic processes.

OS Support for Portable Bulk Synchronous Parallel Programs

Predictability -- the ability to foretell that an implementation will not violate a set of specified reliability and timeliness requirements -- is a crucial, highly desirable property of responsive embedded systems. This paper overviews a development methodology for responsive systems, which enhances predictability by eliminating potential hazards resulting from physically-unsound specifications. The backbone of our methodology is the Time-constrained Reactive Automaton (TRA) formalism, which adopts a fundamental notion of space and time that restricts expressiveness in a way that allows the specification of only reactive, spontaneous, and causal computation. Using the TRA model, unrealistic systems – possessing properties such as clairvoyance, caprice, infinite capacity, or perfect timing -- cannot even be specified. We argue that this "ounce of prevention" at the specification level is likely to spare a lot of time and energy in the development cycle of responsive systems -- not to mention the elimination of potential hazards that would have gone, otherwise, unnoticed. The TRA model is presented to system developers through the Cleopatra programming language. Cleopatra features a C-like imperative syntax for the description of computation, which makes it easier to incorporate in applications already using C. It is event-driven, and thus appropriate for embedded process control applications. It is object-oriented and compositional, thus advocating modularity and reusability. Cleopatra is semantically sound; its objects can be transformed, mechanically and unambiguously, into formal TRA automata for verification purposes, which can be pursued using model-checking or theorem proving techniques. Since 1989, an ancestor of Cleopatra has been in use as a specification and simulation language for embedded time-critical robotic processes.

A Geometric Approach to Slot Alignment in Wireless Sensor Networks

Traditionally, slotted communication protocols have employed guard times to delineate and align slots. These guard times may expand the slot duration significantly, especially when clocks are allowed to drift for longer time to reduce clock synchronization overhead. Recently, a new class of lightweight protocols for statistical estimation in wireless sensor networks have been proposed. This new class requires very short transmission durations (jam signals), thus the traditional approach of using guard times would impose significant overhead. We propose a new, more efficient algorithm to align slots. Based on geometrical properties of space, we prove that our approach bounds the slot duration by only a constant factor of what is needed. Furthermore, we show by simulation that this bound is loose and an even smaller slot duration is required, making our approach even more efficient.