CERT-SEI

Tools & Methods

Achieving predictability by construction requires the integration of several distinct technologies. We call the aggregate of these a prediction-enabled component technology (PECT), although this term may overemphasize the component technology at the expense of other critical technologies.

The PACC Starter Kit is an implementation of a PECT that demonstrates the integration of a particular set of technologies that yield predictability by construction for such qualities as performance and behavioral correctness. Some of the technologies found in the PACC Starter Kit include:

  • The Pin component technology is the basic fabrication mechanism for components and their assemblies.
  • The Construction and Composition Language (CCL) is an architecture description language that has been specialized to Pin-style component technologies, from which we define reasoning framework interpretations and generate Pin implementations.
  • The Lambda-star performance reasoning frameworks support reasoning about average- and worst-case latency of systems in both periodic and stochastic settings.
  • The ComFoRT reasoning framework uses state-of-the-art software model checking technology for reasoning about the safety and liveness behavior of assemblies. It can also be used to generate proof certificates that will accompany the abstract models produced via predicate abstraction. This technology will provide a sound and strong form of certification for software components.
  • The Copper model checker uses advanced abstraction-refinement and compositional reasoning techniques to reason about concurrent C programs.
  • The Covert reasoning framework uses static analysis and software model checking technology to find buffer overflows in C programs.
  • A measurement and validation test bench supports the development of statistical confidence labels on performance predictions.