Faculty Research Projects

Title:

Deductive Synthesis for Verifiable, Scalable software generation

Investigators:

Jeffrey Van Baalen, Michael Lowry (Automated Software Engineering Group, NASA Ames Research Center)

Abstract:

This project, called Amphion, is a joint activity with NASA Ames Research center. The goal of the Amphion project is to make Knowledge-Based Software Engineering (KBSE) a reality for NASA. KBSE uses techniques from artificial intelligence and formal methods to raise the level at which users program to the specification level (which describes the problem to be solved) from the code level (which describes how to solve the problem).

The Amphion approach to implementing KBSE for NASA is to automate software reuse. The construction of reuse libraries of software components is the standard software engineering solution for improving software development productivity and quality. By encapsulating usable functionality in software components (e.g. subroutines, object classes), and then reusing those components, software of greater functionality can be developed in less time, with some assurance that the overall system is correct because it is built up from trusted components.

Current activities at the University of Wyoming on this project include

• The development of a technique that explains how a program generated by Amphion was synthesized in a manner easily understandable to domain experts. For example, a user can ask why some portion of a synthesized program has been included and an explanation in terms of the program specification will be generated.
• Work on the automatic generation of decision procedures to accelerate deductive synthesis.

Title:

Specifying and Verifying Fault-tolerant Agent-based Protocols

Investigators:

Jeffrey Van Baalen, James Caldwell, Shivakant Mishra

Abstract:

Fault tolerance is an important issue in mobile, agent-based computing systems. However, most research in this area has focused on security and mobility issues. The DaAgent (Dependable Agent) system is similar to several other agent-based computing systems. However, unlike these systems DaAgent is being designed to address fault tolerance issues. Within the DaAgent system several fault tolerant protocols are being investigated. These protocols have been specified in natural language, English prose, and a Java implementation within the DaAgent system is being tested. This approach has proved to be extremely time-consuming and inflexible, for example, it is difficult to rapidly change test conditions and fault injection is extremely primitive involving physically halting or resetting a machine, pulling network connections, or sending a kill message to the agent process. Testing the implementation of course serves as a weak form of evidence of correctness, but offers little real assurance of the correctness of the system.

In order to address these problems we are taking the approach of formalizing the protocol specifications and debugging them at the specification level. We are using the Maude executable specification language for this purpose. We are taking this approach knowing that a majority of defects in systems can be traced back to specification errors. Also, much data supports the fact that errors identified early in the development process are dramatically less expensive to correct.

Support:

University of Wyoming: Faculty Grant-in-Aid award $5000 (1999-2000).

Title:

Meeting Some of Knuth's Machine Verification Challenges

Investigators:

Thomas Bailey, John Cowles

Abstract:

In the paper ``Textbook Examples of Recursion'', Donald E. Knuth of Stanford University generalizes McCarthy's 91 function and Takeuchi's triple recursion. Quoting from Knuth: ``Several theorems are proposed as interesting candidates for machine verification, and some intriguing open questions are raised.'' The machine verification is done with the theorem prover ACL2.

The generalization of the 91 function involves real numbers which are dealt with by mechanically verifying results that are true, not only about the field of all real numbers, but also about every subfield of that field. See the ACL2 Case Studies book.

Knuth generalizes Takeuchi's function to higher dimensions. Knuth's original formulation of a theorem about the generalization was incorrect, but a correction was suggested in May 2000. As of June 2000, ACL2 has verified the corrected version of the theorem for dimensions 2 through 7. See the presentation at the ACL2 Workshop 2000.

Title:

CAREER: A formal programming methodology with applications to developing automated verifiers.

Investigators:

James Caldwell

Abstract:

The goals of this research are twofold. Firstly, the work is directed at establishing a new methodology of formal program development. This will be done within the type-theoretic framework provided by the Nuprl system. Secondly, this methodology will be tested and refined in the context of efforts to synthesize automated verifiers: decision procedures, model-checkers, and satisfiability procedures.

The new methodology is based on a combination of complementary modes of formal program development: extraction in which a formal proof (typically a constructive proof of a forall\exists statement) is interactively constructed and a ``correct-by-construction'' program term is extracted directly from the proof; and, verification in which a program term is shown to be correct by explicitly proving it inhabits a type corresponding to its specification. In practice, it is sometimes easier to verify a program term while at other times it is easier to extract it. Although the Nuprl system provides a framework which supports both modes, a methodology truly integrating the two is not well established. The new methodology offers the possibility of gaining leverage on difficult problems because it uniformly supports the application of the two techniques within the same environment.

Actual large-scale formal programming efforts provide the most effective driver for the development, testing and refinement of a new methodology. In this research, integrated verification and extraction methods will be applied to synthesizing programs that implement algorithms supporting automated verification: model-checkers, satisfiability procedures, and decision procedures. Automated verifiers have gained acceptance within industry: however, presently they may only credibly be used to discover errors. Until the correctness of a tool has been formally established, that tool cannot in turn be used to certify the correctness of its results. Thus, formal program development has an important role to play in the development of automated verification tools.

This research will result in a new methodology for formally generating efficient and readable programs in a type-theoretic framework by using a combination of existing verification and extraction techniques. It will result in a number of formally developed artifacts including programs and mathematical theories which are of significant interest in their own right. Additionally, there are plans to adapt the formalized mathematical theories supporting these program developments for use in an undergraduate discrete mathematics course.

Support:

NSF CCR-9985239, $231,195, (2000-2004) this project is funded by NSF as part of the CAREER program.

Title:

Building Interactive Digital Libraries of Formal Algorithmic Knowledge

Investigators:

University of Wyoming: James Caldwell (Co-PI), John Cowles
Cornell: Robert Constable (PI), Stuart Allen (Co-PI)
California Institute of Technology: Jason Hickey (Co-PI)

Abstract:

The world is engaged in a grand scientific and technological enterprise to build a global information resource. It will include vast digital collections of scientific information. Creating this global resource will be one of the great achievements of information technology. The research of our group at Cornell, Cal Tech and Wyoming on applied logic, formal methods and automated reasoning will make the emerging information resource more capable -- first by providing a basis for semantic processing of information and for a logical accounting of its structure, essential to creating knowledge, and second by including among the resources an interactive digital library of formal computational mathematics. Such a library will bring into being a ``formal forum'' that will connect experts and practitioners together in building reliable software systems, educating the information technology work force, empowering the lay scientist, and in nucleating the creation of a broader library of formally grounded knowledge.

We propose contributions to this enterprise that will impact all uses and will make the global information resource especially valuable in designing reliable software systems. We are well qualified to solve the research problems identified in the call for proposals. The ten research concentration areas listed in the call naturally fall into two groups. One is concerned with the issues that arise in trying to automate a logically sound information management service (topics 4-10). The other group is concerned with providing formal content, namely formal algorithmic knowledge supported by constructive reasoning (topics 1, 2, 3, and part of 6 and the preamble). It is essential to pursue topics in both groups simultaneously. We have worked on the content and application issues for twenty five years. We thought about foundational ``library issues'' for the past eight years, and have implemented novel ideas that we are now testing. In the course of this work we identified several critical technical challenges that we propose to investigate in this project on progressively larger scales.

We remain leaders in demonstrating the value of constructive methods, both in foundational theory and in significant applications. We have built highly usable systems that we and others have used to create large amounts of formal content and support the design and verification of software. Currently we develop and use two different systems which interact; to connect them we have been led to create advanced formal information management tools as part of our logical library. We know the problems involved in scaling these tools to support the emerging global digital library of formal content and to support collaborative theory building and reliable software construction. One of the most critical challenges is finding methods to track dependencies among library objects in an environment that allows justifications of inference steps to include programs (called tactics). Another key challenge is devising accounting mechanisms that allow different theorem provers to share results consistently and allow users to merge results developed independently. A further issue is implementing operations that soundly transform entire algorithmic~theories~and~translate among~them.

Creating formal algorithmic content requires systems that are very expressive, open and very fast. We explore all three aspects which leads us to problems that have been unsolved for many years, such as how to implement a practical general reflection mechanism in an open system and how to reason about computational complexity in formal theories. For speed we are led to building concurrent interactive provers. For more expressiveness, we are led to concepts and tools for proving and programming ``in the large.'' Our research agenda on these topics is critical to building digital libraries of formal algorithmic knowledge which in turn will significantly enhance the nation's ability to design, build and maintain reliable software systems.

Support:

ONR N00014-01-1-0765 (2001-2004): $152,596 (UW part), option(2004-2006): $114,751 (UW part)

Title:

A Secure Internet-Based Data Transfer System for Space Life Sciences

Investigators:

Rex E. Gantenbein, Thomas L. James, Garrace DeGroot, Sung Y. Shin (South Dakota State University)

Abstract:

Researchers from NASA and its partners in the International Space Station have collected many years worth of data on living and working in space. This project involves creating a secure, Internet-accessible data management system to make that data available to scientists all over the world, as well as to support collection of new results from research in the years to come. Access to the data will be limited to researchers who have entered into an agreement with NASA for access to the data, but within this group there will be varying levels of access that must be supported.

Support:

Funding for this project has come from the NASA Life Sciences Research Laboratory, the NASA Graduate Student Researchers Program, and the Wyoming Space Grant Consortium, NASA Grant #NGT-40008.

Title:

The Wyoming Cancer Control Network

Investigators:

Rex E. Gantenbein, Yong Edward Qiu, Suranga Hettiarchchi

Abstract:

Health-care professionals in Wyoming recognize the value of the World-Wide Web in providing information about various diseases and their cures, but many do not have the time or expertise to search through the thousands of pages that most search engines return in response to a simple query such as "cancer." The Wyoming Cancer Control Network involves the creation of a searchable Web page that provides "quick links" to pre-screened Web pages offering valid information about cancer. The project will eventually provide a way for health-care professionals to quickly and easily view cancer information and communicate among themselves about issues related to cancer and its treatments.

Title:

Translation tools for Web-Based Translators

Investigator:

Jeffrey Van Baalen

Abstract:

We are developing a tool set that enables a non-computer science expert to quickly build translators for semi-structured documents. For example, one can easily build HTML to XML translators. Of course, this idea only makes sense on sets of HTML pages that have the same format. An example is a phone directory. Here all the relevant information for each HTML page is in the same format, so we can write a set of rules that translates any of these pages to some desired XML.

The translation process begins with a more or less standard LALR (1) parser for an HTML grammar. An input HTML page is parsed into an internal representation called an Abstract Syntax Tree. The user specifies transformations on this tree to produce the desired XML. The transformations can take any of the text of a page into account, not just the HTML tags. We are also working on an error recovery mechanism to address the fact that many documents (like HTML pages) are not well-formed, causing problems for the parser. So far, we have built translators for the faculty, staff and student directories at the University of Wyoming. It is now possible to hit a web page that returns information from these directories in XML. Also we have written translators for a couple of the standard stock information pages on the web (e.g. Yahoo). This enables one to get the stock information back in XML.

Title:

Integrating Spatial Access Methods into real DBMS Environments

Investigator:

Byunggu Yu

Abstract:

The complexity of deploying high-performance spatial structures in transactional DBMS environments has motivated us to experiment with the idea of reusing the effort invested in developing a traditional indexing scheme.

The development of efficient methods and techniques for spatial retrieval is an important and timely issue in the area of database management. Since spatial access methods (SAMs) preserve the proximity of objects in a multi-dimensional space better than the indexing schemes for exact-match retrieval, e.g. B+-trees, they tend to be used to support spatial selections. In contrast to point access methods (PAMs), SAMs must accommodate both points and extended spatial objects (regions in space). However, since spatial structures employ more complex operations than traditional indexing techniques, supporting fine-grain concurrency and dynamic recovery becomes a serious obstacle to the deployment of SAMs in transactional DBMSs. The idea of reusing the effort, which invested in developing an existing indexing scheme, would enable rapid deployment of a spatial access method by reusing a traditional indexing technique, e.g. a B+-tree, along with the accompanying concurrency and recovery mechanisms.

Although some flexible PAMs (e.g., UB-trees and pyramid techniques), which index point objects with traditional access methods, have been proposed, except UB-trees, few of them have been actually integrated into real DBMS environments. In this project, we implement and test these PAMs in well-known commercial DBMS (Informix). On these PAMs, we implement and test transformation schemes (SAMs that can reuse any PAM to index extended spatial objects). Furthermore, we implement our recent three-layer QSF-trees (3lQSF-trees), which is the most flexible variant of the original QSF-tree, and conduct a set of comprehensive experiments in real DBMS environments.

Support:

This project is supported by a $222,250 software grant from Informix Software Inc.

Title:

Towards Processing Complex Spatial Queries

Investigator:

Byunggu Yu

Abstract:

Our research objectives are to design, implement, and test the core techniques that are required to develop an efficient processor for complex spatial queries. Spatial databases are required for storage and retrieval of geographical information, multimedia data, documents, and medical images. Since spatial data are very complex and large relative to conventional one-dimensional data, the primitive operations are expensive. Moreover, a spatial query frequently consists of multiple primitive operations. Therefore, efficient processing techniques are even more important than in conventional databases. Unfortunately, there is a marked lack of adequate query processor for complex spatial queries. In this project, we investigate the problems of developing efficient spatial query processor, and provide appropriate solutions. The solutions will enable us to develop an efficient and effective spatial query processor that can be easily integrated into existing systems.

Support:

NSF EPSCoR (Starter Grant) $30,000, 2001-2002