CodeHawk: an analyzer generator

KT has developed a static analyzer generator called CodeHawk&trade. CodeHawk enables the following:

  • the ability to synthesize families of static analyzers with high performance AND 100% code coverage on industrial-sized code sets. This is made possible by using Specware (www.specware.org) to specify the desired properties and to synthesize the resulting analyzers.
  • customizability to an application, i.e., the ability to define application-specific properties for analysis. (Contrast this with analyzers that are restricted to programming language semantics.) Initially, this will require tool mediation by KT experts.
  • support for software development by providing in-context ranges to the parameters of a function. This is made possible by using Specware to specify the desired properties and to synthesize the resulting analyzers.
  • support for software development support. Providing in-context ranges to the parameters of a function supports informed (by constraint recognition) unit testing. The capability could be used for MCDC support.

  • support for integration testing and reverse engineering. Determining the complete impact set of a statement or function exceeds capabilities provided by conventional data flow analysis, since CodeHawk can narrow potential data flows, e.g., through elicited variable constraints.

  • support for certification. CodeHawk can be used to support best practices. One goal is formal support for proofs for CodeHawk's results. Another goal is differential static analysis, to reduce time and costs of re-certification for upgrades.

The initial code for analysis is C, but we will extend this to include Java. We are open to analysis of C++ applications.

All the capabilities above will not happen at once. We will phase-in CodeHawk functionality and work at the start with a few organizations to get feedback before we make the system more widely available. If you would like more details, please contact us.

NASA taps Kestrel team

NASA's Exploration Mission Systems Directorate selected the team of Kestrel Institute (prime), Kestrel Technology, Sun Microsystems, Jet Propulsion Laboratory (JPL), and The Open Group in its 2004 competition for R&D projects to support upcoming exploration missions. Kestrel's project, "Model-centric safety-critical Java for Exploration", was among 70 projects chosen from an initial field of 3750. Press release

Code-named MXJ, Kestrel's project's goal is to build an environment in which application requirements can be written in a domain specific language, and specfications can be analyzed for properties related to functionality, runtime behavior, and satisfaction of mission- and safety-critical constraints. Policies can be woven into specifications to create runtime monitors to support fault protection. Finally, the specifications can be transformed into Java for deployment.

To address mission- and safety-critical requirements that impose constraints on the programming language itself, Kestrel Technology and Sun Microsystems will work with The Open Group within the Java Community Process to create a standard for Safety Criitical Java, which is then available as a target language. The applications selected for MXJ's focus are resource management (e.g., power for landers and rovers), and Guidance, Navigation, and Control (GNC). Kestrel Institute will work with JPL to create the appropriate models and specification languages for these applications.

Safe net-centric systems

KT has been awarded another Phase I SBIR, this one to develop a Model Development Environment (MoDE) that supports the creation of net-centric systems with guarantees of safety and information assurance. The main technical objective of MoDE is to develop a comprehensive net-centric system development environment that supports:

  • development and composition of high-level models of a target system
  • safety constraints and other cross-cutting constraints that can be enforced by automated tools
  • analysis of models for safety and generation of certifications
  • generation of efficient code from the models
  • certification of the code generation process itself, so that the executable code has assurance guarantees.