Program Transformation

My primary research is in the area of rewrite-based program transformation. This type of program transformation is essentially based on symbol substitution in the context of a correctness-preserving relation such as strong equivalence or refinement. A traditional goal in this area (and the goal of my research) is to "structure and restrict the software development process in such a manner that the resulting software can be formally verified to satisfy the specification from which it is derived".

In order to explore these types of transformation-based software development techniques, I have developed (and am continuing to develop) a transformation system called HATS. The acronym HATS stands for High Assurance Transformation System and the name serves as a reminder as to the goal of its development. HATS is being developed with the help and input from several people including Gary Fuehrer, Steve Roach, Frank Wunderlin, Anthony Vestal, and Deepak Kapur. HATS currently only runs on an NT or Windows 2000 platform, but an effort is underway to develop a platform independent version of HATS, and we hope to make something available early next year.

To find out more about my research in program transformation see: HATS and publications.

Virtual Reality

One of the fundamental problems when developing (ultra) high assurance systems is to provide sufficient evidence that an informally stated problem existing in the physical world has been correctly specified in (mapped to) a formal framework. Numerous studies have shown that a significant percentage of system errors can be traced back to this step. Unfortunately, since this mapping crosses an informal/formal boundary it lies beyond the reach of formal verification. While it is true that certain "well-formedness" checks can be performed (e.g., consistency and completeness), formal calculation cannot be used to demonstrate "with mathematical certainty" that a formal specification correctly captures a physical system. This leaves validation techniques as the remaining option for providing evidence in the correctness of a specification.

My research in virtual reality (VR) focuses on leveraging "human calculation" in the validation process. The assumption on which this research is based is that humans have extraordinary spacial reasoning capabilities. The goal is to construct a mapping from a physical system to a formal framework in such a manner that VR can be effectively used to provide an environment maximizing human spacial reasoning capabilities.

Example: The Production Cell

The production cell is a well known case study involving a robotic system. Below is our 3D image representing the physical system. Given the physical model a wire-frame model can be developed in which distinguishable component states map to cells in the wire-frame. Typically component states in a system will intersect with as well as be adjacent to other component states. In this context a control function serves the purpose of orchestrating the behavior of each of the system components in order to achieve some larger objective. Typical errors in the specification stage involve missed system constraints or incomplete or erroneous specification of relationships between system components (e.g., incorrect state intersections).

Constraints are typically formalized as first order logic formulas which are oftentimes difficult to conceptualize. However, when mapped onto a 3D wire-frame these formulas become quite intuitive and are subject to validation by domain experts.

Above is a visual representation describing the non-intersecting region of two components in the production cell.

To find out more about my research in virtual reality see the publications section or to see a more detailed animation click here.

SSP Project

The main project I am currently involved with is funded by Sandia National Laboratories and is called the Sandia Secure Processor (SSP) Project. This project is driven by Sandia's need to develop a processor for small high consequence embedded applications. Any processor considered for these applications must satisfy numerous requirements. Perhaps first and foremost among these is the need to analyze the resulting hardware. This analysis proceeds all the way to the gate level, and for that reason the use of large commercial processors (e.g., Pentium processors) is unattractive. The purpose of such an analysis is to provide "sufficiently convincing" evidence that the processor faithfully carries out the computations it has been instructed to perform. More specifically, to the extent that is possible, Sandia is interested in quantifying and qualifying the behavior of the processor in (1) normal, (2) abnormal, and (3) malevolent environments. The goal of the SSP Project is to build such a processor in-house at Sandia Labs.

For a number of reasons, the choice has been made to leverage off of the extensive research and development that is underway for Java. Thus the processor being developed is essentially a Java Virtual Machine (JVM). The SSP supports most of Java with the exception of: (1) floating point, (2) threads, and (3) strings. The SSP is built directly from the JVM specification and therefore executes byte codes directly (i.e., the byte codes are not interpreted in terms of some other instruction set such as SPARC assembly).

Because of its ability to execute byte codes directly there is a close connection between Java class files and SSP Programs, which are also known as ROM images. This means that the object structure present in class files is largely preserved in ROM images, which makes them easier to analyze.

In general, my role in the SSP project is to bring rigor to its design and implementation. Presently, a major area that I am focusing on is the classloading function for the SSP. Because the SSP is intended for embedded applications, it can not and should not be able to download classfiles during execution time. This constraint enables a significant portion of classloading to be performed statically with the benefit of simplifying the SSP as well as increasing its performance. To date, I have developed a prototype transformation sequence capable of transforming Java applications consisting of a hierarchy of classfiles into corresponding ROM images. My current research is to redesign this transformation sequence using transformations that are more suitable to formal verification. In order to achieve this, HATS will be extended with new types of transformational capabilities.