Predictable Assembly from Certifiable Code (PACC) Initiative
The Predictable Assembly from Certifiable Code (PACC) Initiative is the name of the sponsored project under which the PACC work described on these web pages is carried out at the SEI.
|
|
In Brief
Community Problem:
Mission critical systems are increasingly
developed from software components that have opaque and un-trusted behavior,
yielding systems that have unpredictable behavior.
PACC Goal:
Enable the development of component-based systems
whose critical runtime qualities (performance, security, safety, ...) are
reliably predicted from the trusted properties of software components.
Axioms Guiding Our Work
- Smart architectural design constraints lead to predictable behavior.
- Component technology is a carrier for design constraints.
- The enforcement of design constraints needs to be automated where possible .
Where the PACC Initiative is going
Purpose
The purpose of the Predictable Assembly from
Certifiable Code Initiative is to mature the technical concepts of
predictable assembly from certifiable code (PACC). PACC will
enable software engineers to predict the runtime behavior (or quality
attributes) of assemblies of software components, and to select software
components on the basis of their certified component properties and predicted
contribution to assembly behavior. We are developing prediction-enabled
component technology (PECT) and its associated engineering methods to realize
PACC concepts in a practical, sound, and repeatable way. PECT combines
component technology with existing but under-exploited, and emerging
state-of-the-art, analysis and prediction techniques. We are working to
validate PECT in increasingly challenging defense and industry problem
settings, with an emphasis on scaling to larger systems, improving the accuracy
and generality of the current-generation of PECT performance and safety
prediction technologies, and developing prediction technologies for other
runtime qualities, for example, security. We are enabling the cost-effective
adoption of PECT through an initial PACC Starter Kit that will provide
an out-of-the-box PECT for developing predictable (prototypical) real-time,
safety-critical systems, and support customization of the PECT to new classes
of system and new or problem-specific analysis and prediction techniques.
Finally, we are conditioning the software community to use the Starter Kit and
to recognize the value PACC brings to the software engineering
disciplinethe economic and societal benefits that accrue from achieving
predictable runtime behavior by construction.
Vision
Our vision is that PACC is the preeminent strategy for
using software component technology to build, deploy, and sustain predictably
reliable, timely, safe, and secure software systems. PACC delivers on the
earlier promises of software components that were not fulfilled simply by
interface standards. Critical defense and industry segments (e.g., fire
control, aerospace, automotive, power generation and transmission) use PECT to
establish-and enforce-design and implementation standards that deliver
predictable system behavior by construction. A competitive market exists for
commercial-grade PECTs and for certified software components usable in these
PECTs. PECT provides a conduit for incorporating state of the art quality
attribute analysis techniques into mainstream software development practice.
Acquirers insist on the use of PECT for mission- and business-critical software
systems. PECT use increases the quality of software systems while decreasing
the costs for their development, test and validation. PACC and PECT is a
conventional topic of discourse in software engineering literature and
education, and in the software technology marketplace.
Tasks
The work of the initiative is carried out through two
primary tasks:
- Mature PACC and PECT Technology: Provide organizations with the necessary technology for predictable assembly from certifiable code through prediction-enabled component technology (PECT), state-of-the-art reasoning frameworks for real-time performance, safety, and security; a way to characterize desired component assembly properties, augment component technologies with analysis capability, certify critical component properties with respect to specific systems, and predict the runtime behavior of component assemblies. Harness existing but under-exploited and emerging technologies to enhance PECTs. Validate PECTs in the laboratory and in increasingly demanding industry and DoD settings.
- Establish PACC Transition Basis: Build the necessary mechanisms to effectively guide PACC maturation and transition; establish PACC research credentials; channel other researchers and developers to focus on PACC; educate the developer and the DoD communities about PACC and its results through reports, case studies, tutorials, and a handbook; develop a Starter Kit that includes a complete PECT and is suitable for out-of-the-box use or customization.
Where the PACC Initiative has been
The Predictable Assembly from Certifiable Components (PACC) Initiative was launched in 2003 to address the known deficiencies in component technology. Component technology delivered on the promise of efficiently building systems from components that are easily "hooked" together. It fell short in guaranteeing behavioral properties such as those for safety and performance. At the same time, advances in software architecture showed that architectural designs could be successfully analyzed and designed vis-à-vis quality attribute requirements; the structure of underlying quality attribute models informing the structure of the architecture (see SAT Initiative).
The PACC Initiative was born out of the idea that component technology can be the carrier of these advances in software architecture thereby enabling the creation of predictable architectural designs from a collection of components with certifiable properties and the automatic generation of implementations conforming to those designs.
The PACC Initiative in its two years of activity has proven the viability of this concept. The major architectural elements of prediction-enabled component technology (PECT) were defined, developed, and trial tested in industry for building predictable real time, safety critical software systems. In particular
- A component technology (Pin) was developed that exhibits the minimum required (canonical) features of a predictable component technology. An adaptable kernel runtime was developed for Pin that provides direct support for UML statechart semantics (to reduce the abstraction gap between design specifications and implementations), and supports alternative scheduling disciplines (to support alternative performance theories). The Pin component model supports closed world, fixed topology, reactive (embedded, real time) systems, with parameterized ("plug-in") intercomponent communication protocols. Pin and its runtime execute on Microsoft Win32 on both Windows2K and WindowsCE platforms, and can be rehosted to "bare" hardware.
- A specification language (CCL) was developed that mirrors the Pin component model (and base design concepts) to capture the static structure of components and their assemblies, uses a profile of UML Statecharts to capture the behavioral aspects of components, their assemblies, and their interaction protocols. Code generators have been developed that produce executable implementations from CCL design-level specifications of components and assemblies. Automated translation ("interpretation") have been developed that produce analyzable models for predicting timing-related and safety-related behavior. These translations have been formally defined, increasing confidence that the implemented system is consistent with the analysis models and thereby yielding "predictability by construction."
- A family of reasoning frameworks was developed (lambda-star) for predicting average latency and other timing-related behavior of component assemblies. It uses generalized rate monotonic theory (RMA) as a foundation, and adds queuing extensions coupled with a "sporadic server" design pattern to extend the reach of RMA to systems that exhibit a mix of periodic and aperiodic behavior. In its current form, lambda-star is applicable to a significant and important class of systems, comprising (at least) two domains where lambda-star has been applied: real time control systems in electric power grid (substation automation), and industrial automation (industrial robotic control). Analytic and simulative solutions for significant portions of lambda-star have been validated, and generalization of the theory to a broader class of systems is currently underway.
- Early prototypes of a reasoning framework (ComFoRT) for predicting the satisfaction of safety-critical behavioral constraints have been developed. ComFoRT builds on prior work performed at the SEI to demonstrate the feasibility of model checking that uncovered implementation flaws in industrial robot control code where the state space of the analyzed code exceeded 10200 states, even when abstracted. ComFoRT uses sate-of-the-art software model checking technology, developed by Carnegie Mellon University and optimized specifically for use in component-based systems and for the style of interactive behavior exhibited by such systems. It also employs cutting-edge concepts such as predicate abstraction and automated counter-example guided abstraction refinement to construct conservative finite models of software systems that may exhibit infinite behavior, and promises to provide a robust solution to the principle obstacle for more widespread use of model checking, namely, state space explosion.
- A validation framework was developed for assigning objective statistical confidence intervals to reasoning framework predictions, with particular focus on performance predictions. The framework implements a form of stratified sampling by using a set of topological (e.g., connectivity) and other constraints (e.g, execution ranges) as parameters to a constrained random assembly generation. The constraints bound the space of typical assemblies that are the subject matter of the reasoning framework, while random generation ensures a statistically valid sample within these bounds. The statistical analysis techniques used in conjunction with constrained random assembly generation have been successfully applied in an industrial case study, and the techniques have resulted in one PhD dissertation.
PECT has been applied to model problems in the domains of substation automation and industrial robot control as part of an industrial collaboration with ABB. For substation automation the SEI used PECT to predict the average latency of operations to control primary equipment (e.g., transformers, switches), and for round-trip operations from human operator to primary controllers. ABB provided funding to generalize the concepts for use in an industrial product that allows introduction of third-party controllers. Openness to third-party extension is also a key motivator for the SEI application of PECT to industrial robot control. In this case, the queuing/sporadic server extensions to lambda-star permits accurate analysis of "bounded intrusion" of plug-ins on the timing behavior of critical control functions. This work with ABB can be generalized to a broad class of defense and industry control systems. The impact of this research include
- one senior ABB engineer noting that a "bug" in the inter-process communication code was discovered quickly through model checking; using other methods, it had taken eight years to uncover.
- the demonstration of a performance prediction capability for an industrial controller that ABB previously thought was intractable. This demonstration was possible only because of the reasoning framework developed by the SEI.
The PACC Initiative has also been active in developing academic and industrial research collaborations. During 2003-2004, the PACC team organized six workshops attended by the international leaders in component technology, model checking, and compositional reasoning, published 13 reports and papers, and gave 17 external presentations on PACC technology. A special issue of Journal of Systems and Software 3/2003 on "Component-Based Software Engineering-Component Certification and System Prediction" was co-edited by two members of the PACC team. The workshop Component-Based Software Engineering (CBSE), which the SEI has co-organized as part of the International Conference on Software Engineering (ICSE) for the past six years, is now an adjunct part of the ICSE conference and has its own proceedings published by Springer-Verlag.
Though it is only in its initial stages, the potential of PACC and PECT have been recognized by the DoD: PACC was mentioned explicitly in a congressional testimony made by David McCurdy; the SEI gave a PACC presentation at the Systems & Software Technology Conference (SSTC) program; and an article describing PACC and PECT appeared in Crosstalk.



