A Basis for Composition Language CL

A Basis for Composition Language CL

A Model Problem for an Open Robotics Controller

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.

A Template for Documenting Prediction-Enabled Component Technologies

This report suggests a template for documenting a PECT, and provides guidelines and a few
examples to help PECT developers consolidate the broad range of information produced into the PECT development process in a single, organized volume.

Adaptive System Infrastructure for Ultra-Large-Scale Systems

presentation made at the 2008 SMART Ultra-Large-Scale System Forum, Carnegie Mellon University
Pittsburgh, PA, 2008

Applied Computational Mechanism Design

presentation made at the 2008 SMART Ultra-Large-Scale System Forum, Carnegie Mellon University
Pittsburgh, PA, 2008

Assume-Guarantee Reasoning for Deadlock

Assume-Guarantee Reasoning for Deadlock

Building Systems from Commercial Components

This book describes specific engineering practices needed to integrate preexisting components with preexisting specifications successfully, illustrating the techniques described with case studies and examples.

CCL in Pictures

Presented: June 2005

Certified Binaries for Software Components

Certified Binaries for Software Components

Certifying the Absence of Buffer Overflows

Certifying the Absence of Buffer Overflows

Computational Emergence Research Area

Presentation by Richard P Gabriel, IBM Resear

Copper Manual, Tutorial, and Specification Grammar

Copper is a software model checker for concurrent message-passing C programs.

Creating Custom Containers with Generative Techniques

Creating Custom Containers with Generative Techniques

Enabling Future Technology Ultra-Large-Scale Systems in the Army

presentation made at the SMART Ultra-Large-Scale
System Forum, Carnegie Mellon University
Pittsburgh, PA, 2008

Introducing Predictable Assembly from Certifiable Components (PACC)

Introducing Predictable Assembly from Certifiable Components (PACC)

Is Third Party Certification Necessary?

Is Third Party Certification Necessary?

Issues in Predicting the Reliability of Components

Issues in Predicting the Reliability of Components

Issues of Scale: A Community Perspective

Discussion topics:

* What types of ultra-large-scale systems will there be in your organization/industry?

* What do you see as the major scale challenges and issues in your organization/industry?

* How do you cope with them today? Will those same solutions work in the future?

K-BACEE: A Knowledge-Based Automated Component Ensemble Evaluation Tool

K-BACEE: A Knowledge-Based Automated Component Ensemble Evaluation Tool

Lessons Learned Model Checking an Industrial Communications Library

Lessons Learned Model Checking an Industrial Communications Library

Meeting the Challenge of Ultra-Large-Scale (ULS) Systems

Meeting the Challenge of Ultra-Large-Scale (ULS) Systems

Meeting the Challenges of Ultra-Large- Scale Systems via Model-Driven Engineering

Presented: February 2, 2007

Meeting the Challenges of Ultra-Large-Scale Distributed Real-time & Embedded (DRE) Systems

Presented: Wednesday, May 30, 2007, WPDRTS, Long Beach, CA

Meeting the Challenges of Ultra-Large-Scale Distributed Real-time & Embedded Systems with QoS-enabled Middleware & Model-Driven Engineering

Presented: December 10, 2007, Middleware 2007

Model-Driven Construction of Certified Binaries

October 2007 presentation in which Sagar Chaki and others describe an implementation of the approach that targets the Pin component technology, and present experimental results on a collection of benchmarks

Model-Driven Performance Analysis

Model-Driven Performance Analysis

Obtaining the Benefits of Predictable Assembly from Certifiable Components (PACC)

Obtaining the Benefits of Predictable Assembly from Certifiable Components (PACC)

Optimized L*-Based Assume-Guarantee Reasoning

white paper from the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2007

Overview of ComFoRT: A Model Checking Reasoning Framework

Overview of ComFoRT: A Model Checking Reasoning Framework

Overview of the Lambda-* Performance Reasoning Frameworks

This report provides an overview of the Lambda-* performance reasoning frameworks, their current capabilities, and ongoing research. Lambda-* is a suite of performance reasoning frameworks for predicting the average and worst-case latency of tasks in real-time systems.

PACC Starter Kit

The PACC Starter Kit is an integrated set of tools that
demonstrates how technologies can be combined to deliver objective confidence in predictions of system behavior.

PACC Starter Kit Provides Tools for Developing Systems that Exhibit Predictable Behavior

PACC Starter Kit Provides Tools for Developing Systems that Exhibit Predictable Behavior

PECT Infrastructure: A Rough Sketch

PECT Infrastructure: A Rough Sketch

Packaging Predictable Assembly with Prediction-Enabled Component Technology

Packaging Predictable Assembly with Prediction-Enabled Component Technology

Panel: Promising Research Areas

SMART Event, March 6, 2008

Performance Analysis of Real-Time Component

Performance Analysis of Real-Time Component

Performance Property Theories for Predictable Assembly from Certifiable Components (PACC)

Performance Property Theories for Predictable Assembly from Certifiable Components (PACC)

Pin Component Technology (V1.0) and Its C Interface

Pin Component Technology (V1.0) and Its C Interface

Precise Buffer Overflow Detection via Model Checking

Precise Buffer Overflow Detection via Model Checking

Predicate Abstraction with Minimum Predicates

Predicate Abstraction with Minimum Predicates

Predictability by Construction

This brochure summarizes our area of work about Predictability by Construction: building high-stakes systems from certified software components.

Predictable Assembly of Substation Automation Systems: An Experiment Report, Second Edition

Predictable Assembly of Substation Automation Systems: An Experiment Report, Second Edition

Prediction-Enabled Component Technology Presentation

Prediction-Enabled Component Technology Presentation

Preserving Real Concurrency

white paper presented at Correctness of Model-Based Software Composition (CMC), 2003

Product Line Systems Program Talk SEPG 2008

SEPG 2008 presentation, March 2008

SAT-Based Predicate Abstraction of Programs

SAT-Based Predicate Abstraction of Programs

SAT-Based Software Certification

SAT-Based Software Certification

SMART ULSS Forum: Electricity

SMART ULSS Forum: Electricity

SMART Ultra-Large-Scale Systems Forum: “Scale Changes Everything”

SMART Ultra-Large-Scale Systems Forum: “Scale Changes Everything”

SMART Ultra-Large-Scale Systems Forum: Scale Changes Everything

presentations made on March 6, 2008, as part of the forum, "Scale Changes Everything," on ultra-large-scale (ULS) systems

Scale Changes Everything

A presentation to the 2006 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications held in Portland Oregon.

Scale Changes Everything, ICGSE 2006

International Conference on Global Software Engineering, Costão do Santinho, Florianópolis, Brazil, October 16-19, 2006.

Snapshot of CCL: A Language for Predictable Assembly

Snapshot of CCL: A Language for Predictable Assembly

Software Component Certification: 10 Useful Distinctions

Software Component Certification: 10 Useful Distinctions

System of Systems Common Operating Environment (SOSCOE) Support to Net Centricity

Presented: March 2007

System of Systems Security

SOSSEC is a broadly based industry consortium dedicated to improving by an order of magnitude the nation’s ability to detect, intervene, respond and recover to any and all threats on the Homeland. It is founded upon three principles:

* A wide spectrum of capabilities. Basic research to major program management.

* Innovative business practices that removes the barriers of normal practices.

* Unique ability to respond to government requirements.

The ComFoRT Reasoning Framework

Presented: August 2005

The ComFoRT Reasoning Framework

Model checking is a promising technology for verifying critical behavior of software.
However, software model checking is hamstrung by scalability issues and
is difficult for software engineers to use directly. The second challenge arises
from the gap between model checking concepts and notations, and those used
by engineers to develop large-scale systems. ComFoRT [15] addresses both of
these challenges. It provides a model checker, Copper, that implements a suite
of complementary complexity management techniques to address state space
explosion. But ComFoRT is more than a model checker. The ComFoRT reasoning
framework includes additional support for building systems in a particular
component-based idiom. This addresses transition issues.

The Impact of Scale

The Impact of Scale

The Potential for Synergy Between Certification and Insurance

The Potential for Synergy Between Certification and Insurance

The Software Engineering Institute's Second Workshop on Predictable Assembly: Landscape of Compositional Predictability

To further its work in predictable assembly focusing on compositional reasoning techniques, the Software Engineering Institute (SEI) held its second Predictable Assembly from Certifiable Components (PACC) Workshop on January 10-11, 2003.

ULS Ecosystem Design

The most critical property of a ULS system is its capacity to adapt to the change dynamics of (including the resolution of risk/uncertainty in) its environment. To be able to assure that given ULS systems have adequate adaptive capacity we need a new discipline of ecosystem architecture. Such a discipline will build on but transcend the discipline of software architecture. Economic considerations will play an important role in such a discipline

ULS Systems Research Roadmap 2008

presentation made at the 2008 SMART Ultra-Large-Scale System Forum, Carnegie Mellon University
Pittsburgh, PA, 2008

Ultra-Large-Scale (ULS) Systems Roundtable

Ultra-Large-Scale (ULS) Systems Roundtable

Ultra-Large-Scale Systems: Scale Changes Everything

presentation made at the 2008 SMART Ultra-Large-Scale System Forum, Carnegie Mellon University
Pittsburgh, PA, 2008

Ultra-Large-Scale Systems: The Software Challenge of the Future

Ultra-Large-Scale Systems: The Software Challenge of the Future is the product of a 12-month study of ultra-large-scale (ULS) systems software.

Ultra-Large-Scale-Systems Development Challenges at Siemens

presentation made at the 2008 SMART Ultra-Large-Scale System Forum, Carnegie Mellon University
Pittsburgh, PA, 2008

Using Containers to Enforce Smart Constraints for Performance in Industrial Systems

Using Containers to Enforce Smart Constraints for Performance in Industrial Systems

Verification of Evolving Software via Component Substitutability Analysis

Verification of Evolving Software via Component Substitutability Analysis

Virtua Health

Presented: August 2007

Volume I: Market Assessment of Component-Based Software Engineering Assessments

Volume I: Market Assessment of Component-Based Software Engineering Assessments

Volume II: Technical Concepts of Component-Based Software Engineering, 2nd Edition

Volume II: Technical Concepts of Component-Based Software Engineering, 2nd Edition

Volume III: A Technology for Predictable Assembly from Certifiable Components

Volume III: A Technology for Predictable Assembly from Certifiable Components

Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog

Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog