Defense Notices

Property-directed verification of functional programs tends to take one of two paths. 
First, is the traditional testing approach, where properties are expressed in the original programming language and checked with a collection of test data. 
Tools following this technique have the advantage of a direct integration with the host system, but their resultant statement about a program's correctness is anything but a guarantee. 
Alternatively, for those desiring a more rigorous approach, properties can be written and checked with a formal tool; typically, an external proof system. 
This process delivers a well reasoned argument for a program's correctness, however, it comes at the cost of a more complex system integration requiring additional expertise. 

We propose a hybrid approach that captures the best of both worlds: the formality of a proof system paired with the native integration of an embedded, domain specific language for testing. 
Presented in this document is a description of the hybridization, a theorem prover as a library, as well as a classification of our target properties for case study. 
As we attempt to verify these properties, our goal is to document and formalize the logical connection between language and tool. 
The resultant process will be evaluated both for the strength of its reasoning power and its viability for real world application.

A multichannel sense-and-avoid radar system targeted for small unmanned aerial vehicles (UAVs), such as the 40% Yak-54 RC aircraft, is being developed to assist the integration of UAVs into the national air space. This frequency-modulated continuous-wave (FMCW) radar system utilizes a two-dimensional fast-Fourier transform process to detect targets in range and Doppler. Interferometry using a 5-element receiver array allows the radar to calculate the azimuth/elevation angles of the target relative to itself. These tasks are being performed in real time with a targeted update rate of 10 Hz utilizing highly-integrated radar-ready components and an FPGA based processor. The focus of the research is on analysis and enhancement of the radar performance by implementing various detection and predictive algorithms such as extended Kalman filtering and constant false alarm rate detection. By tracking targets and predicting their future location, false alarms caused by anomalies can be minimized. Furthermore, targets located at the same range and Doppler will corrupt each other’s signals during interferometic processing thus giving the autopilot corrupted angle information. Using a predictive algorithm these occurrences can be avoided with some level of confidence.

The path geo-diversity routing protocol described in this report takes advantage of geographical diversity of physical network topology, and quickens the routing selection. By importing this mechanism, a more accurate path could be provided instead of multiple useless attempts when area-based challenges occur in the network. A k-shortest path algorithm is introduced, followed by a modified algorithm. These two algorithms are implemented in ns-3, and tested in both grid network and real network. Simulation results show that they provide better performance compared to OSPF, as multiple geo-diverse paths are calculated to provide reliable performance.

In a multi-agent system, an idle agent may be available to assist other agents in the system. An agent architecture called intent recognition is proposed to accomplish this with minimal communication. 
In order to assist other agents in the system, an agent performing recognition observes the tasks other agents are performing. Unlike the much studied field of plan recognition, the overall intent of an agent is recognized instead of a specific plan. The observing agent may use capabilities that it has not observed. This study focuses on the key research questions of: (1) What are intent recognition systems? (2) How can these be used in order to have agents autonomously assist each other effectively and efficiently? A conceptual framework is proposed for intent recognition systems. An implementation of the conceptual framework is tested and evaluated. We hypothesize that using intent recognition in a multi-agent system increases utility (where utility is domain specific) and decreases the amount of communication. We test our hypotheses using two experimental series in the domains of Box Pushing, where agents attempt to push boxes to specified locations; and Cow Herding, where agents attempt to herd cow agents into team corrals. A set of metrics, including task time and number of communications, is used to compare the performance of plan recognition and intent recognition. In both sets of experimental series, intent recognition agents communicate fewer times than plan recognition agents. In addition, unlike plan recognition, when agents use the novel approach of intent recognition, they select unobserved actions to perform, which was seen in both experimental series. Intent recognition agents were also able to outperform plan recognition agents by sometimes reducing task completion time in the Box Pushing domain and consistently scoring more points in the Cow Herding domain.

We examine the problem of determining a decision threshold for the binary hypothesis test that naturally arises when a radar system must decide if there is a target present in a range cell under test. Modern radar systems require predictable, low, constant rates of false alarm (i.e. when unwanted noise and clutter returns are mistaken for a target). Measured clutter returns have often been fitted to heavy tailed, non-Gaussian distributions. The heavy tails on these distributions cause an unacceptable rise in the number of false alarms. We use the class of spherically invariant random vectors (SIRVs) to model clutter returns. SIRVs arise from a phenomenological consideration of the radar sensing problem, and include both the Gaussian distribution and most commonly reported non-Gaussian clutter distributions (e.g. K distribution, Weibull distribution). We propose an extension of a prior technique called the Ozturk algorithm. The Ozturk algorithm generates a graphical library of points corresponding to known SIRV distributions. These points are generated from linked vectors whose magnitude is derived from the order statistics of the SIRV distributions. Measured data is then compared to the library and a distribution is chosen that best approximates the measured data. Our extension introduces a framework of weighting functions and adaptively scaling of the measured data. Further, we extend the Ozturk algorithm to both a distribution classi fication technique as well as a method of determining an adaptive threshold in data that may not belong to a known distribution. Special attention is paid to producing a robust, adaptive estimation of the detection threshold.

Communication networks, in particular the Internet, face a variety of challenges that can disrupt our daily lives resulting in the loss of human lives and significant financial costs in the worst cases. We define challenges as external events that trigger faults that eventually result in service failures. Understanding these challenges accordingly is essential for improvement of the current networks and for designing Future Internet architectures. This dissertation presents a taxonomy of challenges that can help evaluate design choices for the current and Future Internet. Graph models to analyse critical infrastructures are examined and a multilevel graph model is developed to study interdependencies between different networks. Furthermore, graph-theoretic heuristic optimisation algorithms are developed. These heuristic algorithms add links to increase the resilience of networks in the least costly manner and they are computationally less expensive than an exhaustive search algorithm. The performance of networks under random failures, targeted attacks, and correlated area-based challenges are evaluated by the challenge simulation module that we developed. The GpENI Future Internet testbed is used to conduct experiments to evaluate the performance of the heuristic algorithms developed.

The surface-elevation of ice sheets and sea ice is currently measured using both satellite and airborne radar altimeters. These measurements are used for generating mass balance estimates of ice sheets and thickness estimates of sea ice. However, due to the penetration of the altimeter signal into the snow there is ambiguity between the surface tracking point and the actual surface location which produces errors in the surface elevation measurement. Until now there is no comprehensive study done to address how the penetration of the Ku-band signal affects the shape of the return signal over various snow zones and sea ice. Therefore, it is important to study the effect sub-surface scattering and seasonal variations in the properties of snow pack have on the return waveform to correctly interpret the satellite radar altimeter data. To address this problem, an ultra-wide bandwidth Ku-band radar altimeter was developed at the Center for Remote Sensing of Ice Sheets (CReSIS). The CReSIS Ku-band Altimeter (CKA) operates over the frequency range of 12 to 18 GHz providing very fine resolution to resolve the sub-surface features of the snow. The CKA is design to encompass the frequency band of SIRAL, a satellite radar altimeter on board CryoSat-2, operating from 13.4 to 13.75 GHz. The data from CKA can be used to simulate SIRAL data, and the simulated SIRAL waveforms can help us understand the effect of signal penetration and sub-surface scattering on the low bandwidth satellite altimeter. The extensive CKA data collected as a part of the Operation Ice Bridge (OIB) campaign can be used to interpret SIRAL data over surfaces with varying snow conditions. The goal of this research is to use modeling and data inter-comparisons from CKA and satellite measurements to investigate the effect of signal penetration into snow and geophysical snow conditions on the retrieval of surface elevation from satellite radar altimeters, such as SIRAL. Based on the results of this investigation, the plan is to improve the tracking algorithms used by SIRAL to effectively track the actual surface location accurately.

As well recognized, healthcare information is growing exponentially and is made more available to public. Frequent users such as medical professionals and patients are highly dependent on the web sources to get the appropriate information promptly. However, the trustworthiness of the web information can be hardly discriminated due to the fast and augmentative properties of the Internet. Most search engines provide relevant pages to given keywords, but the results might contain unreliable or biased information. 

In this dissertation, I proposed a new system named HealthTrust, which automatically assesses the trustworthiness of healthcare information over the Internet. First, in the first phase, a new ranking algorithm for structure-based analysis is adopted. The basic hypothesis is that trustworthy pages are more likely to link to trustworthy pages. In this way, the original set of positive and negative seeds will propagate over the Web graph. Next, in the second phase, the content-consistency between general healthcare-related webpages and trusted sites is evaluated using information retrieval techniques to evaluate the context of the webpage. In addition, sentence modeling is employed to generate contents-based ranking for each page. Finally, an iterative algorithm is developed to integrate the two components.

Existing RF path loss models are useful for prediction but do not necessarily exploit additional knowledge such as differing terrain features. This research will examine the relationship between terrain type (determined by public GIS data sets) and empirical path loss model parameters through the use of a large scale data collection platform. A large scale measurement campaign will be undertaken to sample the UHF DTV bands from a variety of environments using a set of portable software defined radio sensors. Machine learning and geostatistical algorithms will then be used to learn path loss parameters for generalized terrain types.

"Assistive robotics for the elderly has become a significant area of research, driven primarily by a rapidly aging global population. Between 2011 and 2050, the number of people aged 60 and over is expected to climb from 893 million to 2.4 billion. In addition to a rapidly aging global population, a growing shortage of caretakers has placed additional urgency on the search for alternative solutions. 

Despite the potential benefits of assistive robotics, one significant hurdle that remains is designing robots that the elderly are willing to use. Not only must assistive robots be effective at monitoring and caring for the elderly, but they must also be acceptable to a wide range of elderly individuals. While a variety of factors can influence the acceptability of a robot, past research has focused primarily on the physical embodiment of the robot. 

Social robotics, however, uses human-robot interactions to study the many social factors that can influence the acceptability of a robot, including affective behaviors, or behaviors that simulate personality and emotion. While the majority of research in affective behaviors has focused on facial expressions, these methods require sophisticated anthropomorphic representations, which are not generally preferred by the elderly. 

However, in addition to facial expressions, body language can also be an effective communicator of emotions and personalities. This research will demonstrate the effectiveness of using non-verbal behaviors to simulate a variety of personalities and emotions on the Aldebaran Nao, as well as the impact these behaviors have on the elderly’s trust and acceptance of the assistive robot. By adapting the personalities and emotions of an assistive robot both to the task it is performing, as well as to individual elderly users, this research will ultimately enable assistive robots to perform as more effective caretakers for the elderly."