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.

Find Us Here

Share This Page

Share on Facebook  Send to your Twitter page  Save to del.ico.us  Save to LinkedIn  Digg this  Stumble this page.  Add to Technorati favorites  Save this page on your Google Home Page 

For more information

Contact Us

info@sei.cmu.edu

412-268-5800