SAGE to help programmers see their software

KT has been awarded a Phase II SBIR award by the Army Research Labs for SAGE, a programmer's static analysis assistant. The SAGE goal is to provide information derived as a by-product of sound static analysis in support of the production of high assurance software. Users will be able to specify input conditions, e.g., variable ranges and usage scenarios, and see the corresponding envelope of variable outputs at intermediate function points. Users will also be able to check automatically derived program invariants within a development version and compare it with regression-like support with corresponding invariants from previous versions.

SAGE will not require modification of the source, unlike annotation-based verification, nor a changed development process. The technology will also provide a rear-view mirror for Informed Testing&trade. Among other uses, Informed Testing enables us to compute input variable ranges that could cause buffer overflow or other causes for failure of desired application properties.

KT's Metro project to create the Software Hub

KT has been awarded a Phase II SBIR contract by the Office of Naval Research for Metro, a project with the goal to create a Software Hub. Metro will take steps towards creating standards for model driven embedded system development. In our initial work, models defined using Simulink, Matlab and Stateflow will be translated into an object-oriented interchange framework that we will standardize with help from an appropriate standards organization.

The framework will be constructed from a composable set of meta-models. For example, data models (the data types and operations) are defined independently from control models (such as for data flow or state machine). Similarly, object inheritance will be used to capture more analyzable or feature restricted subsets of language like Stateflow.

As part of this project KT will work within selected standards groups to produce language standards, and work in collaboration with prominent tool providers and users to bring about the integration vision.

Failsafe extends IVHM into software

KT has won a Phase II SBIR to build Failsafe, a system that extends Integrated Vehicle Health Management (IVHM) into the software realm.

With embedded software becoming increasingly complex, assuming that it behaves perfectly is not realistic. The adaptation of fault protection concepts to embedded software is attractive, particularly in the context of the fault containment and health management capabilities provided by ARINC 653.

In this project, KT will develop a framework containing tools to:

  • define verifiable models that characterize the software with respect to its interface behavior, resource usage, and data reasonableness
  • instrument and monitor the software for execution in both test and operational environments

Failsafe tools will be integrated into ARINC 653 for fault detection and recovery in an operational context, and available as plug-in's into the Eclipse software development environment for application in a test and verification context such as DSIL and engineering analysis context such as CEAL.

To reduce costs as well as improve safety, the project will also yield a methodology to assist in certification of instantiations from Failsafe.

Robust complex systems

KT has won a Phase II SBIR from the Air Force to build a prototype of the Interface Explorer (IFEx), an automated software verification toolset for assessing the robustness of large complex systems. The analysis of these systems exceeds the capacity of even the most powerful existing static analysis techniques. This owes to the sheer size of the whole application (tens of millions of lines), its heterogeneity (the system's components can be written in multiple programming languages), and its highly dynamic execution modes

IFEx is based on a compositional approach for to robustness analysis. Each component (assumed to be written in a single programming language) is analyzed separately, for its robustness properties, and then also in its context, i.e., using a model of its interaction with the larger system. The user is provided automated support for analysis of the components and their interaction. IFEx automatically checks for basic properties implicitly defined by the programming language (no buffer overflow, no division by zero, etc.), as well as robustness requirements explicitly defined by the user (ranges of the input parameters of a component functionality, invariant properties of the module, communication latencies, etc.).

Based on abstract interpretation techniques, IFEx conservatively discovers all possible property violations, and tuned modeling keeps false positives low. Using the underlying CodeHawk technology, IFEx can scale to handle DoD-sized applications, including those with mixed language modules.