Personal tools
You are here: Home
Document Actions

Welcome to Fluid

by admin last modified 2007-05-17 12:48 PM

Building a Programmer-Oriented Approach to Software Assurance and Evolution

If you're looking for SureLogic, click here

Information about our project is below, but here are some quick links:

img

The Fluid Project is focused on creating practicable tools for programmers to assure and evolve real programs. We focus on "mechanical" program properties that tend to defy traditional testing and inspection regimes. These are properties with a non-local character, in that there may be no single place in the code where they are manifest, and they may involve non-determinism.

We have explored properties including:

  • race conditions and locking policies,
  • unique references and other programmer-significant aliasing properties,
  • effects,
  • appropriate typing,
  • realtime threading policies, and
  • single-threading policies.

These properties bear significantly on code safety, security, API compliance, and other attributes of dependability.

Composable static semantic program analyses are used to assure consistency of code and programmer expressed "low-level" models of design intent. Thus a failure to achieve assurance can indicate an error in the model, an error in the code, or an insufficiently precise analysis.

In order to facilitate experimentation, our prototype tool is presented as a seemingly benign plug-in in the widely adopted Eclipse IDE for Java. Case studies have identified numerous concurrency and other anomalies in production code drawn from a variety of sources, including government, industry, and open source.

We are guided in our design by a set of principles related to practicability. Specifically:

  • Incrementality and early gratification. Any increment of effort we ask programmers to undertake should yield a generally immediate reward in the form of bug finding, assurance creation, guidance in evolution, or model expression.
  • Familiar expression. Properties should be expressed tersely and using terminology already familiar to programmers.
  • Cut points and composability. Components can be assured separately, and the assurances linked into chains of evidence.

The principle of incrementality suggests that partial chains are valuable in that they can assist in localizing attention when there are problems.

img

The Fluid Project team acknowledges primary support through the High Dependability Computing Program (HDCP) from NASA cooperative agreement NCC-2-1298. Work on the Fluid Tool has been funded entirely through NASA and previous contracts with DARPA and NSF. The team appreciates a grant from IBM Corporation specifically for work involving the Eclipse open source IDE. The team also appreciates support from Carnegie Mellon CyLab specifically for work on open source software quality and empirical work on case studies.

 

Powered by Plone, the Open Source Content Management System

This site conforms to the following standards: