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.

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

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

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

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

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

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

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

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 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.

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

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