CERT-SEI

Research

Work on predictability by construction (PBC) began at the SEI 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 informs the structure of the architecture.

The PBC work 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 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 translations ("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.
  • A reasoning framework (ComFoRT) for predicting   the satisfaction of safety-critical behavioral constraints has 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 measurement and validation test bench was developed for assigning objective   statistical confidence intervals to reasoning framework predictions, with   particular focus on performance predictions. That test bench 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.

SEI Blog