This paper discusses the results from an experiment that demonstrates the ability to predict deadline satisfaction of threads in a real-time system where the functionality performed is based on the configuration of the assembled software components. Presented is the method used to abstract the large, legacy code base of the system software and the application software components in the system, the model of those abstractions based on available architecture documentation and empirically-based, runtime observations, and the analysis of the predictions which yielded objective confidence in the observations and model created which formed the underlying basis for the predictions.
A Model Problem for an Open Robotics Controller
Scott A. Hissam & Mark Klein
This report describes the model problem created to support the continued enhancement and development of the prediction-enabled component technology (PECT) reasoning frameworks for an industrial trial in the domain of industrial robotics. The model problem is applicable to other domains typified by embedded control systems consisting of both periodic and stochastic behavior and using fixed-priority scheduling with real-time performance characteristics.
Predictable Assembly of Substation Automation Systems: An Experiment Report
Scott Hissam, John Hudak, James Ivers, Mark Klein, Magnus Larsson, Gabriel Moreno, Linda Northrop, Daniel Plakosh, Judith Stafford, Kurt Wallnau, & William Wood
This reports the results of a PECT feasibility study the PACC team performed for ABB in the domain of power substation automation. Some ideas and terminology were refined a bit between its publication and that of Volume III, but it is representative of our approach, and does document a number of important concepts, especially the notions of co-refinement and empirical validation.
Lessons Learned Model Checking an Industrial Communications Library
This report describes early experiments with packaging model checking as a reasoning framework. It describes the verification of an industrial communications library and the problems found with the library and the verification process.