kevin bierhoff

Kevin Bierhoff, Darpan Saini, Matthew Kehrt, Majid Al-Meshari, Sangjin Han, and Jonathan Aldrich.  A Language-based Approach to Specification and Enforcement of Architectural Protocols.  Technical Report CMU-ISR-10-110, Carnegie Mellon University, March 2010.
Supersedes CMU-ISRI-07-121.

Abstract.  Software architecture research has proposed using protocols for specifying the interactions between components through ports. Enforcing these protocols in an implementation is difficult. This paper proposes an approach to statically reason about protocol conformance of an implementation. It leverages the architectural guarantees of the ArchJava programming language. The approach allows modular reasoning about implementations with callbacks, recursive calls, and multiple instances of component types. It uses a dataflow analysis to check method implementations and uses model checking techniques to reason modularly about component composition. The approach is limited to static architectures but can handle multiple instances for component types and arbitrary nesting of components.

Kevin Bierhoff.  API Protocol Compliance in Object-Oriented Software.  PhD thesis.  Technical Report CMU-ISR-09-108, Carnegie Mellon University, April 2009.

Abstract.  Modern software development is highly reliant on reusable APIs.  APIs often define usage protocols that API clients must follow in order for code implementing the API to work correctly.  Loosely speaking, API protocols define legal sequences of method calls on objects.  In this work, protocols are defined based on typestates.  Typestates leverage the familiar intuition of abstract state machines to define usage protocols.
The goal of this work is to give developers comprehensive help in defining and following API protocols in object-oriented software. Two key technical contributions enable the proposed approach: (1) Object state spaces are defined with hierarchical state refinements. Hierarchical state spaces make specifications more succinct, elegantly deal with subtyping, express uncertainty, and enable more precise reasoning about aliasing. (2) A novel abstraction, called access permissions, combines typestate and aliasing information. Access permissions capture developers' design intent regarding API protocols and enable sound modular verification of API protocol compliance while allowing a great deal of flexibility in aliasing objects.
This dissertation demonstrates that typestate-based protocols with state refinement and access permissions can be used for automated, static, modular enforcement of API protocols in practical object-oriented software. Formal and empirical results show that the presented approach captures common API protocols succinctly, allows sound modular checking of protocol compliance in object-oriented code, can be automated in tools for mainstream programming languages that impose low annotation burden on developers, and can check API protocols in off-the-shelf software with higher precision than previous approaches.
This work puts automatic API protocol compliance checking within reach of being used in practice. It will enable rapid and correct use of APIs during initial construction and ensure that API clients and implementations remain consistent with the specified protocol during maintenance tasks.

Kevin Bierhoff, Nels E. Beckman, and Jonathan Aldrich.  Practical API Protocol Checking with Access Permissions.  Technical Report CMU-ISR-09-101, Carnegie Mellon University, January 2009.

Abstract.  Reusable APIs often define usage protocols. We previously developed a sound modular type system that checks compliance with typestate-based protocols while affording a great deal of aliasing flexibility. We also developed Plural, a prototype tool that embodies our approach as an automated static analysis and includes several extensions we found useful in practice. This paper evaluates our approach along the following dimensions: (1) We report on experience in specifying relevant usage rules for a large Java standard API with our approach. We also specify several other Java APIs and identify recurring patterns. (2) We summarize two case studies in verifying third-party open-source code bases with few false positives using our tool. We discuss how tool shortcomings can be addressed either with code refactorings or extensions to the tool itself. These results indicate that our approach can be used to specify and enforce real API protocols in practice.

Kevin Bierhoff and Jonathan Aldrich.  Modular Typestate Verification of Aliased Objects.  Technical Report CMU-ISRI-07-121, Carnegie Mellon University, March 2007.
Superseded by CMU-ISR-10-110.  A draft of this report has been available on this website since April 2006.

Abstract.  Software architecture research has proposed using protocols for specifying the interactions between components through ports. Enforcing these protocols in an implementation is difficult. This paper proposes an approach to statically reason about protocol conformance of an implementation. It leverages the architectural guarantees of the ArchJava programming language. The approach allows modular reasoning about implementations with callbacks, recursive calls, and multiple instances of component types. It uses a dataflow analysis to check method implementations and uses model checking techniques to reason modularly about component composition. The approach is limited to static architectures but can handle multiple instances for component types and arbitrary nesting of components.

Kevin Bierhoff and Jonathan Aldrich.  Modular Typestate Verification of Aliased Objects.  Technical Report CMU-ISRI-07-105, Carnegie Mellon University, March 2007.

Abstract.  A number of type systems have used typestates to specify and statically verify protocol compliance. Aliasing is a major challenge for these systems. This paper proposes a modular type system for a core object-oriented language that leverages linear logic for verifying compliance to more expressive protocol specifications than previously supported. The system improves reasoning about aliased objects by associating references with access permissions that systematically capture what aliases know about and can do to objects. Permissions grant full, shared, or read-only access to a certain part of object state and allow aliasing both on the stack and in the heap. The system supports dynamic state tests, arbitrary callbacks, and open recursion. The system's expressiveness is illustrated with examples from the Java I/O library.

Andi Bejleri, Jonathan Aldrich, and Kevin Bierhoff.  A Type Checked Prototype-based Model with Linearity.  Technical Report CMU-ISRI-04-142, Carnegie Mellon University, December 2004.

Abstract.  Dynamic inheritance, originating in the Self programming language, is the ability of an object to change the code that it inherits at run time. This ability is useful for modeling objects that behave in different ways at different points in the object's lifecycle. Unstructured dynamic inheritance, however, allows arbitrary changes to the interface of the object, and thus is incompatible with statically typechecked languages such as C++, C# and Java.
This paper provides a more structured facility for dynamic inheritance, where a type system tracks the changes in an object's interface that occur as the inheritance hierarchy is changed. We define a formal model of a language and type system with dynamic inheritance, and prove that the type system is sound in that it prevents run-time type errors. The type system tracks the linearity of objects and methods in order to ensure that objects whose interfaces change are not aliased.