Search

We have performed research on approaches for integrating the personnel who interact with software systems more directly in a collaborative effort of developing, deploying, validating and maintaining the various components of the systems, with the primary objective of enhancing their dependability. We have created techniques that capture and encode user expertise, verification and other dependability-enhancing techniques that use this expertise to function cost-effectively both collaboratively and across system lifetimes, and mechanisms for better coordinating the development and maintenance processes for these systems., The original document contains color images.

This paper presents CraneTracker, a novel sensor platform for monitoring migratory birds. The platform is designed to monitor Whooping Cranes, an endangered species that conducts an annual migration of 4, 000 km between southern Texas and north-central Canada. CraneTracker includes a rich set of sensors, a multi-modal radio, and power control circuitry for sustainable, continental-scale information delivery during migration. The need for large-scale connectivity motivates the use of cellular technology in low-cost sensor platforms augmented by a low-power transceiver for ad-hoc connectivity. This platform leads to a new class of cellular sensor networks (CSNs) for time-critical and mobile sensing applications. The CraneTracker is evaluated via field tests on Wild Turkeys, Siberian Cranes, and an on-going alpha deployment with wild Sandhill Cranes. Experimental evaluations demonstrate the potential of energy-harvesting CSNs for wildlife monitoring in large geographical areas, and reveal important insights into the movements and behaviors of migratory animals. In addition to benefiting ecological research, the developed platform is expected to extend the application domain of sensor networks and enable future research applications.

Load tests aim to validate whether system performance is acceptable under peak conditions. Existing test generation techniques induce load by increasing the size or rate of the input. Ignoring the particular input values, however, may lead to test suites that grossly mischaracterize a system’s performance. To address this limitation we introduce a mixed symbolic execution based approach that is unique in how it 1) favors program paths associated with a performance measure of interest, 2) operates in an iterative-deepening beam-search fashion to discard paths that are unlikely to lead to high-load tests, and 3) generates a test suite of a given size and level of diversity. An assessment of the approach shows it generates test suites that induce program response times and memory consumption several times worse than the compared alternatives, it scales to large and complex inputs, and it exposes a diversity of resource consuming program behavior.

The past decades have produced a wide-variety of automated techniques for assessing the correctness of software systems. In practice, when applied to large modern software systems all existing automated program analysis and verification techniques come up short. They might produce false error reports, exhaust available human or computational resources, or be incapable of reasoning about some set of important properties. Whatever their shortcoming, the goal of proving a system correct remains elusive. Many people believe that, after an initial period of development, software systems are "mostly" correct — systems have much more correct behavior than incorrect behavior. Following this line of thinking, we explore what it means to re-orient program analysis and verification techniques away from focusing on proving properties. Rather, we explore how to develop and leverage techniques that characterize the subset of system behaviors that can be shown to be consistent with property specifications. We describe the challenges in producing a rich suite of evidence-producing automated verification and validation techniques and suggest one approach to overcoming those challenges. We then describe the promise that combining such techniques offers — the weaknesses of one technique can be masked by the strengths of another, the results of one technique can be used to target the application of another, and evidence from multiple techniques can be combined to produce an explicit characterization of what is known about system correctness. BIOGRAPHY Matthew B. Dwyer is the Henson Professor of Software Engineering in the Department of Computer Science and Engineering at the University of Nebraska – Lincoln. He received the BS in Electrical Engineering in 1985 from the University of Rochester and worked for six years as a Senior Engineer with Intermetrics Inc. developing compilers and software for safety-critical embedded systems. His interests in verification and validation of embedde

Model checking is a promising technique for verifying program behavior and is increasingly finding usage in industry. To date, however, researchers have primarily considered model checking of single versions of programs. It is well understood that model checking can be very expensive for large, complex programs. Thus, simply reapplying model checking techniques on subsequent versions of programs as they evolve, in the limited time that is typically available for validating new releases, presents challenges. To address these challenges, we have developed a new technique for regression model checking (RMC), that applies model checking incrementally to new versions of systems. We report results of an empirical study examining the effectiveness of our technique; our results show that it is significantly faster than traditional model checking.

Dynamic analysis is an increasingly important means of supporting software validation and maintenance. To date, developers of dynamic analyses have used low-level instrumentation and debug interfaces to realize their analyses. Many dynamic analyses, however, share multiple common high-level requirements, e.g., capture of program data state as well as events, and efficient and accurate event capture in the presence of threading. We present SOFYA – an infra-structure designed to provide high-level, efficient, concurrency-aware support for building analyses that reason about rich observations of program data and events. It provides a layered, modular architecture, which has been successfully used to rapidly develop and evaluate a variety of demanding dynamic program analyses. In this paper, we describe the SOFYA framework, the challenges it addresses, and survey several such analyses.