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.