Software Engineering Institute Carnegie Mellon

Product Line Systems Program
Predictable Assembly from
Certifiable Code
PACC Technologies
Collaborations
Downloads
Publications
Glossary
Workshops and Conferences
Software Product Lines
Software Architecture

PACC Technologies

 

Achieving predictability by construction requires the integration of several distinct technologies. We call the aggregate of these a prediction-enabled component technology (PECT)glossary icon, 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 qualties as performance and behavioral correctness. Some of the technologies found in the PACC Starter Kit include:

  • The Pinglossary icon component technologyglossary icon is the basic fabrication mechanism for components and their assemblies.
  • The Construction and Composition Language (CCL)glossary icon is an architecture description language that has been specialized to Pin-style component technologies, from which we define reasoning framework interpretationsglossary icon and generate Pin implementations.
  • The Lambda-star performance reasoning frameworksglossary icon 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.

Current Areas of Investigation

We are also actively investigating these technologies:

  • The ArchE architecture design assistant provides expert guidance on how to apply design tactics to transform architectural (assembly) specifications to optimize the behavior of a system according to specific runtime qualities.