PACC Publications

Predictable Assembly

Objective Confidence

Component Technology

Reasoning Frameworks

Performance Reasoning Frameworks

Model Checking Reasoning Frameworks

Case Studies

Languages for Predictable Assemblies

Predictable Assembly

Ivers, James & Moreno, Gabriel A. "Model-driven Development with Predictable Quality." Conference on Object Oriented Programming Systems Languages and Applications, Montreal, Quebec, Canada, 2007.

The PACC Starter Kit is an eclipse-based development environment that combines a model-driven development approach with reasoning frameworks that apply performance, safety, and security analyses. These analyses predict runtime behavior based on specifications of component behavior and are accompanied by some measure of confidence.

Merson, Paulo & Hissam, Scott. "Predictability by Construction." Conference on Object Oriented Programming Systems Languages and Applications, San Diego, CA, 2005.

This two page paper was presented along with a poster in the poster sessions at OOPSLA 2005. It gives an overview of how PACC uses reasoning frameworks to achieve predictability.

Larsson, Magnus; Wall, Anders; & Wallnau, Kurt. “Predictable Assembly: The Crystal Ball to Software.” ABB Review (2/2005). [PDF]

The sheer complexity of software means that errors often slip unnoticed through test phases – traditional testing methods are no longer in a position to evaluate all situations that can occur. Mathematically based approaches to development and verification greatly reduce risks and contribute to quality management.

Merson, Paulo. A Template for Documenting Prediction-Enabled Component Technologies. (CMU/SEI-2003-TN-030).

This report outlines the PACC team's initial thinking on how reasoning frameworks can be documented as off-the-shelf products in their own right.

Stafford, Judith & Hissam, Scott. The Software Engineering Institute's Second Workshop on Predictable Assembly: Landscape of Compositional Predictability. (CMU/SEI-2003-TN-029)

Six leading researchers in component-based software engineering were invited to discuss topics related to compositional reasoning with members of the SEI technical staff. During the workshop, participants articulated the current state of research, identified gaps in the available technology, and set the direction for future efforts.

Hissam, Scott & Ivers, James. PECT Infrastructure: A Rough Sketch. (CMU/SEI-2002-TN-033).

This paper describes initial thinking on the what is required of a tool infrastructure for developers and users of prediction-enabled component technology, including roles and infrastructure change scenarios.

Hissam, Scott; Moreno, Gabriel.; Stafford, Judith; & Wallnau, Kurt. Packaging Predictable Assembly with Prediction-Enabled Component Technology. (CMU/SEI-2001-TR-024).

This report describes the use of prediction-enabled component technology (PECT) as a means of packaging predictable assembly as a deployable product.

Stafford, Judith & Wolf, Alexander. Annotating Components to Support Component-Based Static Analysis of Software Systems. Proceedings of Grace Hopper Conference 2000, Hyannis, Massachusetts, September, 2000.

This paper describes the improvement in precision of path-based analysis results that can be achieved when input-output pathways of components have been identified and are used to refine assembly-level path analysis.

Objective Confidence

Chaki , Sagar; Ivers, James; Lee, Peter; Wallnau, Kurt; Zeilberger, Noam. Model-Driven Construction of Certified Binaries.

This paper presents a model-driven approach for generating certified binaries (executables) from component specifications.

Chaki , Sagar; Ivers, James; Lee, Peter; Wallnau, Kurt; Zeilberger, Noam. Certified Binaries for Software Components (CMU/SEI-2007-TR-001).

This report presents an approach to automatically certify that binary code satisfies user specifiable behavioral requirements. The approach builds on proof-carrying code and certifying model checking research and generates a proof certificate that can be independently verified, allowing developers to trust the code that is produced without having to trust the tools that produced it.

Chaki , Sagar; Schallhart, Christian; Veith, Helmut. Verification Across Intellectual Property Boundaries.

This paper presents a cryptographic approach for software certification.

Chaki, Sagar & Hissam, Scott. Certifying the Absence of Buffer Overflows. (CMU/SEI-2006-TN-030).

This report presents a technique for certifying the safety of buffer manipulations in C programs. The approach is based on two key ideas: (1) using a certifying model checker to automatically verify that a buffer manipulation is safe and (2) validating the resulting invariant and proving it with a decision procedure based on Boolean satisfiability.

Chaki, Sagar. "SAT-Based Software Certification". pp. 151 - 166. Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2006). Vienna, Austria, March 25 - April 2, 2006. Notes in Computer Science, Volume 3920, 2006.

This paper presents an automated technique for certifying a program's adherence to safety and liveness criteria. The technique consists of two broad stages. In the first stage, a certifying model checker is used to generate a verification condition (VC). In the second stage, a decision procedure based on Boolean satisfiability (SAT) is used to prove the VC. The use of SAT enables us to construct extremely compact proofs.

Chaki, Sagar. SAT-Based Software Certification. (CMU/SEI-2006-TN-004).

This technical note presents a framework for constructing extremely compact proofs of the satisfaction of safety and liveness specifications by source code. The approach is based on a combination of certifying model checking and Boolean satisfiability (SAT) technology.

Wallnau, Kurt C. Software Component Certification: 10 Useful Distinctions. (CMU/SEI-2004-TN-031).

Certification is a practical, proven means of establishing trust in various sorts of things in other disciplines and is, therefore, a natural contender for developing trust in software components. This technical note introduces a series of 10 distinctions that can help in understanding different aspects of certification in the context of software components.

Hissam, Scott; Hudak, John; Ivers, James; Klein, Mark; Larsson, Magnus; Moreno, Gabriel; Northrop, Linda; Plakosh, Daniel; Stafford, Judith; Wallnau, Kurt; & Wood, William. Predictable Assembly of Substation Automation Systems: An Experiment Report, 2nd ed. (CMU/SEI-2002-TR-031).

This reports the results of a PECT feasibility study the PACC team performed for ABB in the domain of power substation automation. It is representative of our approach and documents a number of important concepts, especially the notions of co-refinement and empirical validation.

Moreno, Gabriel.; Hissam, Scott; & Wallnau, Kurt. “Statistical Models for Empirical Component Properties and Assembly-Level Property Predictions: Toward Standard Labeling.” Proceedings of the 5th ICSE Workshop on Component-Based Software Engineering, Orlando, Florida, May 2002. [PDF]

The paper provides a short tutorial on various types of statistical analyses used to describe measurable properties of components and assembly predictions, leading to a position statement regarding a form of standard component label.

Li, Paul Luo; Shaw, Mary; Stolarick, Kevin; & Wallnau, Kurt. “The Potential for Synergy between Certification and Insurance.” First International Workshop on Software Reuse Economics, held in conjunction with the Seventh International Conference on Software Reuse, Austin, Texas, April 2002. [PDF]

Written with the help of an expert in actuarial models and insurance, this paper argues that predictability of assembly behavior is a useful prerequisite for for-profit insurance of component quality and behavior.

Stafford, Judith & Wallnau, Kurt. “Is Third Party Certification Necessary?” Proceedings of the 4th ICSE Workshop on Component-Based Software Engineering, Toronto, Canada, May, 2001. [PDF]

The paper offers speculations on the roles and interactions among these roles for various stakeholders in certifying properties of software components.

Component Technology

Moreno, Gabriel. "Creating Custom Containers with Generative Techniques". Proceedings of the 5th International Conference on Generative Programming and Component Engineering (GPCE'06). Portland, Oregon, USA, 2006.

This paper shows how generative programming techniques, using AspectC++ and metaprogramming, can be used to generate custom stubs and skeletons in component containers without the need for special compilers or interface description languages. It also describes an approach to create custom containers by composing different non-functional features.

Hissam, Scott A.; Moreno, Gabriel A.; & Wallnau Kurt C. Using Containers to Enforce Smart Constraints for Performance in Industrial Systems. (CMU/SEI-2005-TN-040).

This technical note shows how smart constraints can be embedded in software infrastructure by using containers, so that systems conforming to those constraints are predictable by construction. The use of containers is shown in the context of a model problem in the domain of industrial robotics.

Hissam, Scott; Ivers, James; Plakosh, Daniel; Wallnau, Kurt. Pin Component Technology (V1.0) and Its C Interface. (CMU/SEI-2005-TN-001).

Pin is a basic, simple component technology suitable for building embedded software applications. Pin is a component technology for pure assembly—systems are assembled by selecting components and connecting their interfaces. This report describes the main concepts of Pin and documents the C-language interface to Pin V1.0.

Wallnau, Kurt C. Volume III: A Technology for Predictable Assembly from Certifiable Components. (CMU/SEI-2003-TR-009).

This describes in some detail the theory of Prediction Enabled Component Technology (PECT). It is a bit more technical and theoretical than Volume II but still accessible to a technical audience. It is the foundation report on PECT.

Bass, Len; Buhman, Charles; Comella-Dorda, Santiago; Long, Fred; Robert, John; Seacord, Robert; & Wallnau, Kurt. Volume I: Market Assessment of Component-Based Software Engineering Assessments (CMU/SEI-2001-TN-007).

Reports on and abstracts what industry analysts were saying about the adoption of software component technology. Also includes survey results. Now somewhat dated, this was written by non marketing-types, so caveat emptor.

Wallnau, Kurt; Stafford, Judith; Hissam, Scott; & Klein, Mark. “On the Relationship of Software Architecture to Software Component Technology.” Proceedings of the 6th International Workshop on Component-Oriented Programming (WCOP6), Budapest, Hungary, June, 2001. [PDF]

This paper outlines our early thinking on how architectural design patterns could be incorporated into component models. The terminology is now dated but the ideas are still relevant, and the only illustrations of PACC concepts that explicitly address the question of predictability of properties related to information security.

Bachmann, Felix; Bass, Len; Buhman, Charles; Comella-Dorda, Santiago; Long, Fred; Robert, John; Seacord, Robert; Wallnau, Kurt. Volume II: Technical Concepts of Component-Based Software Engineering, 2nd ed. (CMU/SEI-2000-TR-008).

This is essential background reading on component technology. It isn't too deep or too technical, and, although we have since modified some of our terminology, it is still quite good as background on what we mean by “component technology” and its current limits.

Plakosh, Daniel; Smith, Dennis; & Wallnau, Kurt. Builder's Guide for WaterBeans Components (CMU/SEI-99-TR-024).

WaterBeans is a proof-of-feasibility system for building software applications through a process of assembling (composing) prefabricated software components. WaterBeans was originally developed as a proof of feasibility that software component technology could be used to develop software applications in the domain of water-quality modeling.

Reasoning Frameworks

Merson, Paulo & Hissam, Scott. "Predictability by Construction." Conference on Object Oriented Programming Systems Languages and Applications, San Diego, CA, 2005.

This two page paper was presented along with a poster in the poster sessions at OOPSLA 2005. It gives an overview of how PACC uses reasoning frameworks to achieve predictability.

Bass, Len; Ivers, James; Klein, Mark; Merson, Paulo. Reasoning Frameworks. (CMU/SEI-2005-TR-007).

This report describes a vehicle for encapsulating the quality attribute knowledge needed to understand a system's quality behavior as a reasoning framework that can be used by nonexperts. After defining the elements of a reasoning framework, the report goes on to describe several reasoning frameworks.

Chaki, Sagar; Ivers, James; Sharygina, Natasha; and Wallnau, Kurt. “The ComFoRT Reasoning Framework.” (2005). [PDF]

This paper provides a short description of the ComFoRT reasoning framework. It identifies the tools and techniques used to generate models from design specifications and to formally verify the models with temporal logic model checking. For a deeper look into ComFoRT, see [Overview of ComFoRT: A Model Checking Reasoning Framework].

Hissam, Scott; Klein, Mark; Lehoczky, John; Merson, Paulo; Moreno, Gabriel; & Wallnau, Kurt. Performance Property Theories for Predictable Assembly from Certifiable Components (PACC) (CMU/SEI-2004-TR-017).

This report develops a queueing-theoretic solution to predict, for a real-time system, the average-case latency of aperiodic tasks managed by a sporadic server. This theory is then applied to a model problem drawn in the domain of industrial robot control.

Ivers, James & Sharygina, Natasha. Overview of ComFoRT: A Model Checking Reasoning Framework (CMU/SEI-2004-TN-018).

ComFoRT is a reasoning framework that packages the effectiveness of state-of-the-art model checking in a form that enables users to perform formal verification without becoming a model checking expert. This report describes the techniques used to automate verification of design specifications and the model checking algorithms used within ComFoRT.

McGregor, John D.; Stafford, Judith A.; & Cho, Il-Hyung. “Measuring Component Reliability.” Proceedings of the 6th ICSE Workshop on Component-Based Software Engineering, Portland, Oregon, May 2003. [PDF]

A follow-on to Issues in Predicting the Reliability of Components, this also describes a technique for using Pin-like (see Volume III) constructs to aggregate reliability measures for several operations in a single component.

Stafford, Judith & McGregor, John D. “Issues in Predicting the Reliability of Components.” Proceedings of the 5th ICSE Workshop on Component-Based Software Engineering, Orlando, Florida, May 2002. [PDF]

Describes various definitions of, and (empirically-based) computational models of, software reliability, and outlines an experiment in compositional (empirical) reliability.

Performance Reasoning Frameworks

Hissam, Scott A.; Moreno, Gabriel A.; & Wallnau Kurt C. Using Containers to Enforce Smart Constraints for Performance in Industrial Systems. (CMU/SEI-2005-TN-040).

Hissam, Scott A. & Klein, Mark. A Model Problem for an Open Robotics Controller. (CMU/SEI-2004-TN-030).

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 here is an abstract representation of the parallel tasking and component configuration in an industrial robotics controller.

This report develops a queueing-theoretic solution to predict, for a real-time system, the average-case latency of aperiodic tasks managed by a sporadic server. The report applies this theory to a model problem drawn in the domain of industrial robot control.

This reports the results of a PECT feasibility study we 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.

Model Checking Reasoning Frameworks

Chaki, S. ; Datta, A. Automated Verification of Security Protocol Implementations. (CMU-CyLab-08-002).

This report presents a method that combines software model checking with a standard protocol security model (including a symbolic attacker) to provide analogous guarantees about protocol implementations as previous work does for protocol specifications.

Ghafari, N. ; Gurfinkel, A. ; Klarlund, N. ; Trefler, R. "Algorithmic Analysis of Piecewise FIFO Systems", in Proceedings of 7th International Conference on Formal Methods in Computer Aided Design (FMCAD'07), Austin, TX, USA, November 2007.

In this paper, we present two algorithms for computing the set of reachable states of a FIFO system composed of piecewise components. We consider arbitrary systems with a single communication channel, and multi-channel systems with acyclic communication structure.

Simmonds, J. ; Davies, J. ; Gurfinkel, A. & Chechik, M. "Exploiting Resolution Proofs to Speed Up LTL Vacuity Detection for BMC", in Proceedings of 7th International Conference on Formal Methods in Computer Aided Design (FMCAD'07), Austin, TX, USA, November 2007.

In this paper, we explore how resolution proofs from a run of a bounded model checker (BMC) can be mined for temporal vacuity. We present a vacuity detection tool, VaqTree, that uses these methods to detect vacuous variables, decreasing the total number of model-checking runs required to detect all sources of vacuity.

Chechik, M. & Gurfinkel, A. "A Framework for Counterexample Generation and Exploration", International Journal on Software Tools for Technology Transfer , Vol. 9, No. 5-6, pages 429-445, October 2007.

In this paper, we present a framework for generating, structuring, and exploring counterexamples produced by a model checker. The counterexamples are presented in a proof-like form that gives the user the navigational flexibility, but without sacrificing any of the intuitiveness and close relation to the model.

Gheorghiu, M.; Gurfinkel, A.; Chechik, M. "Finding State Solutions to Temporal Queries", in Proceedings of 6th International Conference on Integrated Formal Methods (IFM'07), Oxford, UK, July 2007.

In this paper, we propose a symbolic query-checking algorithm that finds "state" solutions to a temporal logic query. We argue that our approach generalizes previous specialized techniques, and this generality allows us to find new and interesting applications, such as finding stable states in a gene network. The approach has been implemented on top of the model checker NuSMV.

Chechik, M. ; Gheorghiu, M. ; Gurfinkel, A. "Finding Environment Guarantees", in Proceedings of 10th International Conference on Fundamental Approaches to Software Engineering (FASE'07), Braga, Portugal, March 2007.

In this paper, we identify and formalize a problem related to environment models -- environment guarantees. It captures those cases where the correctness of the component under analysis is due solely to the model of its environment. Environment guarantees provides a model-based analog to a property-based notion of vacuity by identifying cases when the component is irrelevant to satisfaction of a property.

Chaki, Sagar & Strichman, Ofer. Optimized L*-based Assume-Guarantee Reasoning, Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2007, LNCS 4424, page 276-291, March 26-30, 2007.

In this paper, we suggest three optimizations to the L*-based automated Assume-Guarantee reasoning algorithm for the compositional verification of concurrent systems.

Chaki, Sagar & Hissam, Scott. Certifying the Absence of Buffer Overflows. (CMU/SEI-2006-TN-030).

Chaki, Sagar & Sinha, Nishant. Assume-Guarantee Reasoning for Deadlock. (CMU/SEI-2006-TN-028)

In this report, the learning-based automated assume-guarantee paradigm is extended to perform compositional deadlock detection. A learning algorithm L^F is developed that constructs the minimal deterministic failure automaton accepting any unknown regular failure set using a minimally adequate teacher.

Chaki, Sagar & Sinha, Nishant. Assume-Guarantee Reasoning for Deadlock.

This is a conference version of CMU/SEI-2006-TN-028.

Chaki, Sagar; Ivers, James; Sharygina, Natasha; and Wallnau, Kurt. “The ComFoRT Reasoning Framework.” (2005). [PDF]

Ivers, James. Lessons Learned Model Checking an Industrial Communications Library. (CMU/SEI-2005-TN-039).

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.

Chaki, Sagar; Clarke, Edmund; Sharygina, Natasha; Sinha, Nishant. Verification of Evolving Software via Component Substitutability (CMU/SEI-2005-TR-008).

This report presents an automated and compositional procedure to solve the component substitutability problem. In particular, techniques are developed that exploit the results of previous verification efforts and focus only on the portions of the system that have changed (components). These new techniques incorporate model checking into development processes in a much less cumbersome manner than previous verification techniques.

Chaki, Sagar & Hissam, Scott. Precise Buffer Overflow Detection via Model Checking. (2005)

This white paper discusses an approach for precise detection of buffer overflows in C source code using model checking in combination with predicate abstraction and iterative counterexample driven refinement. It also compares and contrasts such an approach with existing buffer overflow detection techniques.

Chaki, Sagar; Clarke, Edmund; Sinha, Nishant; & Thati, Prasanna. “Automated Assume-Guarantee Reasoning for Simulation Conformance.” Proceedings of Computer Aided Verification (CAV), 2005. [PDF]

This paper addresses the issue of efficiently automating assume-guarantee reasoning for simulation conformance between finite state systems and specifications. The authors focus on a non-circular assume-guarantee proof rule. We have implemented this framework in the COMFORT toolkit and we report encouraging results (over an order of magnitude improvement in memory consumption) on non-trivial benchmarks.

Cook, Byron; Kroening, Daniel; & Sharygina, Natasha. “COGENT: Accurate Theorem Proving for Program Verification.” Proceedings of the Computer-Aided Verification (CAV) 2005 Conference. [PDF]

Many symbolic software verification engines such as Slam and ESC/Java rely on automatic theorem provers. This paper describes a theorem prover, Cogent, that accurately supports all ANSI-C expressions. When used by Slam during the model checking of over 300 benchmarks, Cogent’s improved accuracy reduced the number of Slam timeouts by half, increased the number of true errors found, and decreased the number of false errors.

Clarke, Ed; Jain, Himanshu; Kroening, Daniel; & Sharygina, Natasha. “Predicate Abstraction and Refinement Techniques for Verifying Verilog.” Proceedings of the DAC (Design and Automation) 2005 International Conference. [PDF]

Model checking techniques applied to large industrial circuits suffer from the state space explosion problem. A major technique to address this problem is abstraction. This paper proposes to use predicate abstraction for verifying RTL Verilog, a technique successfully used for software verification. We compare the performance of our technique with a modern model checker that implements localization reduction.

Chaki, Sagar; Clarke, Edmund; Sharygina, Natasha; & Sinha, Nishant. “Dynamic Component Substitutability Analysis.” Proceedings of Formal Methods (FM), 2005. [PDF]

This paper presents an automated and compositional procedure to solve the substitutability problem in the context of evolving software systems. The substitutability approach has been implemented and validated in the COMFORT model checking tool set and we report encouraging results on an industrial benchmark.

Ivers, James & Sharygina, Natasha. Overview of ComFoRT: A Model Checking Reasoning Framework (CMU/SEI-2004-TN-018).

Chaki, Sagar; Clarke, Edmund; Grumberg, Orna; Ouaknine, Joel; Sharygina, Natasha; Touili, Tayssir; & Veith, Helmut. An Expressive Verification Framework for State/Event Systems (CMU-CS-04-145). Pittsburgh, PA: Computer Science Department, School of Computer Science, Carnegie Mellon University, 2004 [PDF]

Specification languages for concurrent software systems need to combine practical algorithmic efficiency with high expressive power and the ability to reason about both states and events. We address this question by defining a new branching-time temporal logic SE-A which integrates both state-based and action-based properties. For experimental evaluation, we have integrated the presented algorithms in the software verification tool MAGIC.

Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; & Yorav, Karen. “Predicate Abstraction of ANSI-C Programs Using SAT.” Formal Methods in System Design 25, 2 (2004): 105 - 127. [PDF]

Predicate abstraction is a major method for verification of software. However, the generation of the abstract Boolean program from the set of predicates and the original program suffers from an exponential number of theorem prover calls as well as from soundness issues. This paper presents a novel technique that uses an efficient SAT solver for generating the abstract transition relations of ANSI-C programs.

Chaki, Sagar; Clarke, Edmund; Ouaknine, Joel; Sharygina, Natasha; & Sinha, Nishant. “State/Event-based Software Model Checking.” Fourth International Conference on Integrated Formal Methods (IFM) 2004 (Lecture Notes in Computer Science [LNCS] volume 2999). Kent, England, April 4-7, 2004. [PDF]

We present a framework for model checking concurrent software systems which incorporates both states and events. Contrary to other state/event approaches, our work also integrates two powerful verification techniques, counterexample-guided abstraction refinement and compositional reasoning.

Chaki, Sagar; Clarke, Edmund; Ouaknine, Joel; & Sharygina, Natasha. “Automated, Compositional and Iterative Deadlock Detection.” Proceedings of the Second ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE) 2004. San Diego, CA, June 22-25, 2004. [PDF]

We present an algorithm to detect deadlocks in concurrent message-passing programs. Even though deadlock is inherently non-compositional and its absence is not preserved by standard abstractions, our framework employs both abstraction and compositional reasoning to alleviate the state space explosion problem.

Chaki, Sagar; Clarke, Edmund; Groce, Alex; Ouaknine, Joel; Strichman, Ofer; & Yorav, Karen. “Efficient Verification of Sequential and Concurrent C Programs.” Formal Methods in System Design (FMSD) 25, 2-3 (September-November 2004): 129-166.

The state-space explosion problem in model checking remains the chief obstacle to the practical verification of real-world distributed systems. We attempt to address these issues in the context of verifying concurrent (message-passing) C programs against safety specifications. We describe our approach in detail, and report on some very encouraging experimental results obtained with our tool MAGIC.

Chaki, Sagar; Clarke, Edmund; Groce, Alex; & Strichman, Ofer. “Predicate Abstraction with Minimum Predicates.” Proceedings of the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME) 2003 (Lecture Notes in Computer Science [LNSC] volume 2860). L’Aquila, Italy, October 21-24, 2004. [PDF]

Predicate abstraction is a popular abstraction technique employed in formal software verification. Our experiments show that predicate minimization can result in a significant reduction of both verification time and memory usage compared to earlier methods.

Ivers, James & Wallnau, Kurt. “Preserving Real Concurrency.” Correctness of Model-Based Software Composition (CMC) Proceedings. Technical Report 2003-13 at Universitat Karlsruhe, July 2003. [PDF]

This paper sketches a method for modeling and composing component behavior (using CCL) in a manner that ensures that model concurrency matches implementation concurrency. This is a refinement of some of the ideas in A Basis for Composition Language (CMU/SEI-2002-TN-026), and is based on UML rather than CSP to promote transition.

Chaki, Sagar; Ouaknine, Joel; Yorav, Karen; Clarke, Edmund. “Automated Compositional Abstraction Refinement for Concurrent C Programs: A Two-Level Approach.”2nd Workshop on Software Model Checking (SoftMC) 2003, ENTCS 89(3). Boulder, Colorado, July 14, 2003. [PDF]

The state space explosion problem in model checking remains the chief obstacle to the practical verification of real-world distributed systems. We attempt to address this problem in the context of verifying concurrent (message-passing) C programs against safety specifications. To our knowledge, this is the first compositional use of CEGAR in the context of model checking concurrent C programs.

Chaki, Sagar; Ouaknine, Joel; Sharygina, Natasha; & Sinha, Nishant. “State/Event-based Software Model Checking.” To appear in the State-oriented vs. Event-oriented thinking in Requirements Analysis, Formal Specification and Software Engineering (ST.EVE) 2003 Workshop, Pisa, Sept. 13, 2003. [PDF]

This paper presents an LTL-like logic and associated formalism for expressing system properties that deal with both states and events. It also presents preliminary experimental evidence showing that such an approach is practically advantageous during verification of communication-based software (including component-based systems).

Case Studies

Ivers, James. Lessons Learned Model Checking an Industrial Communications Library. (CMU/SEI-2005-TN-039).

Hissam, Scott A. & Klein, Mark. A Model Problem for an Open Robotics Controller (CMU/SEI-2004-TN-030).

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.

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.

Languages for Predictable Assemblies

Wallnau, Kurt C. & Ivers, James. Snapshot of CCL: A Language for Predictable Assembly. (CMU/SEI-2003-TN-025).

This report illustrates in a simple example the basic syntax and semantics of CCL. CCL combines primitives for describing the structural aspects of an assembly of components with a syntax based on UML statecharts for describing detailed component behavior. This combination provides the information needed to predict assembly behavior with respect to several quality attributes (e.g., performance and safety) as well as to generate complete component implementations for the Pin component technology.

Ivers, James; Sinha, Nishant; & Wallnau, Kurt. A Basis for Composition Language CL. (CMU/SEI-2002-TN-026).

This paper provides a formal interpretation of an abstract component technology (see Volume III and Preserving Real Concurrency). We have since switched from the use of CSP to the more widely used (if less formal) UML statecharts. Nonetheless, the report is foundational, and we've built on it in many ways.