Generators and goal-directed evaluation provide a rich programming paradigm when combined with traditional control structures in an imperative language. Icon is a language whose goal-directed evaluation is integrated with traditional control structures. This integration provides powerful mechanisms for formulating many complex programming operations in concise and natural ways. However, generators, goal-directed evaluation, and related control structures introduce implementation problems that do not exist for languages with only conventional expression evaluation. This dissertation presents an implementation model using recursion that serves as a basis for both an interpreter and a compiler. Furthermore, in the case of the compiler, optimizations can be performed to improve the efficiency of Icon programs, mainly by reducing the general evaluation strategy whenever possible. The dissertation describes a compile-time semantic analysis used to gather information about the properties of expressions and how they are used at their lexical sites. The optimizations that can be performed using this information are illustrated in the context of the compiler model described in the dissertation.

The HP2623 graphics terminal emulator is implemented on the PC for use with the Starbase graphics package provided on the departmental HP9000 series 500 computer system. This paper discusses the development and implementation of this emulator. A demonstration of its compatibility with Starbase is also provided along with a users' manual and a programmers' reference.

The purpose of this thesis is the design of the software necessary for teleoperation of a fluid handling laboratory. It does not include the implementation of this software. The laboratory for which it is designed is being developed at the University of Arizona, and is a model of the fluid handling laboratory aboard Space Station. The software includes man/machine, machine/machine, and machine/instrument interfaces. The man/machine interface is menu driven and consists of high level commands which are independent of the devices in the laboratory. The machine/machine interface is also device independent. It consists of intermediary commands and maps the commands of the man/machine interface into the low level, device dependent, commands and programs of the machine/instrument interface. Although the software is primarily designed for the model laboratory, the needs of a remotely operated fluid handling laboratory aboard Space Station have been considered.

This thesis describes the process of writing a software application geared toward developing computer graphics in the Windows environment. The code is written using Visual C++ and the Microsoft Foundation Classes (MFC). As an illustration of this process we will walk through the development of a software application. This application will allow a user to create and edit an image composed of simple line graphics and geometric shapes. The user can select drawing colors, select drawing styles, and do area filling. This application also illustrates the use of menus and dialog boxes. / Department of Computer Science

Experimental plans identify the treatment allocated to each unit and they are necessary for the supervision of most comparative experiments. Few computer programs have been written for constructing experimental plans but many for analysing data arising from designed experiments. In this thesis the construction of experimental plans is reviewed so as to determine requirements for a computer program. One program, DSIGNX, is described. Four main steps in the construction are identified: declaration, formation of the unrandomized plan (the design), randomization and output. The formation of the design is given most attention. The designs considered are those found to be important in agricultural experimentation and a basic objective is set that the 'proposed' program should construct most designs presented in standard texts (e.g. Cochran and Cox (1957)) together with important designs which have been developed recently. Topics discussed include block designs, factorial designs, orthogonal Latin squares and designs for experiments with non-independent observations. Some topics are discussed in extra detail; these include forming standard designs and selecting defining contrasts in symmetric factorial experiments, general procedures for orthogonal Latin squares and constructing serially balanced designs. Emphasis is placed on design generators, especially the design key and generalized cyclic generators, because of their versatility. These generators are shown to provide solutions to most balanced and partially balanced incomplete block designs and to provide efficient block designs and row and column designs. They are seen to be of fundamental importance in constructing factorial designs. Other versatile generators are described but no attempt is made to include all construction techniques. Methods for deriving one design from another or for combining two or more designs are shown to extend the usefulness of the generators. Optimal design procedures and the evaluation of designs are briefly discussed. Methods of randomization are described including automatic procedures based on defined block structures and some forms of restricted randomization for the levels of specified factors. Many procedures presented in the thesis have been included in a computer program DSIGNX. The facilities provided by the program and the language are described and illustrated by practical examples. Finally, the structure of the program and its method of working are described and simplified versions of the principal algorithms presented.

This thesis provides a powerful general-purpose proof technique for the verification of systems, whether finite or infinite. It extends the idea of finite local model-checking, which was introduced by Stirling and Walker: rather than traversing the entire state space of a model, as is done for model-checking in the sense of Emerson, Clarke et al. (checking whether a (finite) model satisfies a formula), local model-checking asks whether a particular state satisfies a formula, and only explores the nearby states far enough to answer that question. The technique used was a tableau method, constructing a tableau according to the formula and the local structure of the model. This tableau technique is here generalized to the infinite case by considering sets of states, rather than single states; because the logic used, the propositional modal mu-calculus, separates simple modal and boolean connectives from powerful fix-point operators (which make the logic more expressive than many other temporal logics), it is possible to give a relatively straightforward set of rules for constructing a tableau. Much of the subtlety is removed from the tableau itself, and put into a relation on the state space defined by the tableau-the success of the tableau then depends on the well-foundedness of this relation. This development occupies the second and third chapters: the second considers the modal mu-calculus, and explains its power, while the third develops the tableau technique itself The generalized tableau technique is exhibited on Petri nets, and various standard notions from net theory are shown to play a part in the use of the technique on nets-in particular, the invariant calculus has a major role. The requirement for a finite presentation of tableaux for infinite systems raises the question of the expressive power of the mu-calculus. This is studied in some detail, and it is shown that on reasonably powerful models of computation, such as Petri nets, the mu-calculus can express properties that are not merely undecidable, but not even arithmetical. The concluding chapter discusses some of the many questions still to be answered, such as the incorporation of formal reasoning within the tableau system, and the power required of such reasoning.

Approved for public release; distribution is unlimited / The use of the HF radar to measure and map surface currents has proliferated along the coastlines of many countries for purposes of Search and Rescue, Oil Spill Management, Oceanographic and Fishery Science studies. In the US Navy, these surface current maps are being evaluated for operational use in real-time data assimilating coastal circulation models, and direct monitoring tools in environmentally sensitive operating areas. The SeaSonde HF radar, a DF system, was considered in this study. It uses the MUSIC algorithm to recover bearings from the Doppler backscatter spectrum of the sea surface. By varying the radial and antenna patterns, the simulated backscatter spectra were passed through the SeaSonde software suite for radial pattern recovery. This unprecedented approach directly evaluated SeaSondeâ s MUSIC, and the associated uncertainties were examined against the simulated inputs of (1) fixed amplitude and phase deviations from the ideal antenna pattern, (2) measured antenna patterns and (3) decreasing SNR. It was found that using the measured antenna pattern to recover radials yielded least uncertainty, but a definitive prediction of MUSICâ s radial-recovery capability in relation to the patternâ s complex amplitude and phase structure remained illusive. The results highlighted the need to calibrate the militaryâ s DF-systems for accurate azimuth recovery. / Outstanding Thesis

The success of formal specifications and reactive systems is highly dependant on the formal specification language being used. To date, the most common approach to this problem involves two activities: (i) the specification activity, where correctness properties are specified, and (ii) verification activity, where the system under review is proven to satisfy those properties. Typically, some form of temporal logic or regular expression language is used to specify the correctness properties; properties that are specified for given states of the system under review. This means that specification is partial and is done after system design, prototyping, or coding. Temporal logics have been found to be unsuitable for early specification. This thesis investigates the suitability of TLCharts, a specification language that combines statecharts and temporal logic, for the early specification of the dynamic characteristics of a homing torpedo. In order to achieve the task, a fictitious homing torpedo example, called KTorp, is used. Using a systematic approach, we developed deterministic statecharts and non-deterministic TLCharts for the KTorp control software. Our case study shows that using TLCharts as the early specification language for weapon systems software provides efficient, visual and intuitive specifications.

Wireless Local Area Networks (WLANs) extend the usage of wired LANs from specific places within a building to the many mobile users whether in the building or outside. The wireless data is not only used by authorized users but also might be intercepted and altered by other unauthorized users. Therefore, the power of the transmitter is kept as low as possible to make it difficult for the others to intercept the signal. In the absence of interception, adversaries might attempt to jam the signal so that the network cannot operate properly. The purpose of present study is to investigate the effects of noise jamming against a WLAN in a high-rise building. The building model was created by Rhino, a well known Windows-based computer drawing software. The jamming effects are simulated using Urbana. The LAN transmitter operates with an omni-directional antenna and 100 mW of power. The noise jammer has variable power levels of 10 W and 100 W. It uses a directional antenna. The signal-to jam-ratio (SJR) is computed for several floors in the building to determine if the jammer will disrupt the WLAN.

Modern network technologies were not designed for high assurance applications. As the DOD moves towards implementing the Global Information Grid (GIG), hardened networks architectures will be required. The Monterey Security Architecture (MYSEA) is one such project. This work addresses the issue of object reuse as it pertains to volatile memory spaces in untrusted MYSEA clients. When a MYSEA client changes confidentiality levels, it is possible that classified material remains in volatile system memory. If the system is not power cycled before the next the login, an attacker could retrieve sensitive information from the previous session. This thesis presents a conceptual design to protect against such an attack. A processor may undergo a hard or soft reboot. The proposed design uses a secure coprocessor to sense the reboot type of the host platform. In addition, a count is kept of the number of hard reboots the host platform has undergone. Using services provided by the secure coprocessor, the host platform can trustfully attest to a remote entity that it has undergone a hard reboot. This addresses the MYSEA object reuse problem. The design was tested using the CPU simulator software SimpleScalar.