kevin bierhoff

Taekgoo Kim, Kevin Bierhoff, Jonathan Aldrich, and Sungwon Kang.  Typestate Protocol Specification in JML.  In Proceedings of the 8th International Workshop on Specification and Verification of Component-Based Systems (SAVCBS '09) at ESEC/FSE 2009, Amsterdam, The Netherlands, August 25, 2009, pages 11-18.  ACM Press, New York, August 2009.

Abstract.  The Java Modeling Language (JML) is a language for specifying the behavior of Java source code.  However, it can describe the protocols of Java classes and interfaces only implicitly.  Typestate protocol specification is a more direct, lightweight and abstract way of documenting usage protocols for object-oriented programs.  In this paper, we propose a technique for incorporating the typestate concept into JML for specifying protocols of Java classes and interfaces, based on our previous research on typestate protocol specifications.  This paper presents a set of formal translation rules for encoding typestate protocol specifications into pre/post-condition specifications.  It shows how typestate protocol specifications can be mixed with pre/post-condition specifications and how violations of code contracts in inheritance can be handled.  Finally, our proposed technique is demonstrated within the Java/JML environment to show its effectiveness.

Kevin Bierhoff and Jonathan Aldrich.  Permissions to Specify the Composite Design Pattern.  In 7th International Workshop on Specification and Verification of Component-Based Systems (SAVCBS '08) at FSE-16, Atlanta, GA, USA, November 9-10, 2008.

Abstract.  The Composite design pattern is a well-known implementation of whole-part relationships with trees of Composite objects.  This paper presents a permission-based specification of the Composite pattern that allows nodes in an object hierarchy to depend on invariants over their children while permitting clients to add new children to any node in the hierarchy at any time.  Permissions can capture the circular dependencies between nodes and their children that arise in this context.  The paper also discusses verifying a Composite implementation and known limitations of the presented specification.

Kevin Bierhoff and Chris Hawblitzel.  Checking the Hardware-Software Interface in Spec#.  In Proceedings of the 4th Workshop on Programming Languages and Operating Systems (PLOS '07) at SOSP '07, Stevenson, WA, USA, October 18, 2007.

Abstract.  Research operating systems are often written in type-safe, high-level languages. These languages perform automatic static and dynamic checks to give basic assurances about run-time behavior. Yet such operating systems still rely on unsafe, low-level code to communicate with hardware, with little or no automated checking of the correctness of the hardware-software interaction. This paper describes experience using the Spec# language and Boogie verifier to statically specify and statically verify the safety of a driver's interaction with a network interface, including the safety of DMA.

Kevin Bierhoff, Mark Grechanik, and Edy S. Liongosari.  Architectural Mismatch in Service-Oriented Architectures.  In Proceedings of the International Workshop on Systems Development in SOA Environments (SDSOA '07) at ICSE-29, Minneapolis, MN, USA, May 21, 2007, pp. 114-119.  IEEE Computer Society, Los Alamitos, CA, USA, May 2007.

Abstract.  Architectural mismatch results from implicit and conflicting assumptions that designers of components make about the environments in which these components should operate. While architectural mismatch was extensively studied in monolithic and distributed applications, it has not been applied to Service-Oriented Architectures (SOAs). A major contribution of this paper is the analysis of how architectural mismatch affects SOAs. We study how implicit and conflicting assumptions that designers make about web services and their compositions affect the quality of resulting SOA-based systems. We support our analysis with empirical data that we collected from a large-scale SOA-based project within Accenture and other smaller projects.

Kevin Bierhoff.  Iterator Specification with Typestates.  In Proceedings of the 5th International Workshop on Specification and Verification of Component-Based Systems (SAVCBS '06) at FSE-14, Portland, OR, USA, November 10-11, 2006, pages 79-82. ACM Press, New York, November 2006.

Abstract.  Java iterators are notoriously hard to specify.  This paper applies a general typestate specification technique that supports several forms of aliasing to the iterator problem. The presented specification conservatively captures iterator protocols and consistency rules. Two limitations of the specification are discussed.

Kevin Bierhoff, Edy S. Liongosari, and Kishore S. Swaminathan.  Incremental Development of a Domain-Specific Language That Supports Multiple Application Styles.  In 6th OOPSLA Workshop on Domain-Specific Modeling (DSM '06) at OOPSLA '06, Portland, OR, USA, October 22, 2006, pages 79-86.

Abstract.  Domain-Specific Languages (DSLs) are typically built top-down by domain experts for a class of applications (rather than a specific application) that are anticipated in a domain. This paper investigates taking the opposite route: Building a DSL incrementally based on a series of example applications in a domain. The investigated domain of CRUD applications (create, retrieve, update, delete) imposes challenges including independence from application styles and platforms. The major advantages of an incremental approach are that the language is available for use much sooner, there is less upfront cost and the language and domain boundaries are defined organically. Our initial experiments suggest that this could be a viable approach provided certain careful design decisions are made upfront.

Andi Bejleri, Jonathan Aldrich, and Kevin Bierhoff.  Ego: Controlling the Power of Simplicity. In 2006 International Workshop on Foundations and Developments of Object-Oriented Languages (FOOL/WOOD '06) at POPL '06, Charleston, SC, USA, January 14, 2006.
The proof of soundness and additional material can be found in the companion Technical Report CMU-ISRI-04-142.

Abstract.  The Self programming language provides powerful dynamic features, allowing programmers to add and remove methods from objects and to change the inheritance hierarchy at run time. These facilities are useful for modeling objects that behave in different ways at different points in the object’s lifecycle. Unstructured use of these techniques, however, can result in arbitrary changes to the interface of the object, and thus is incompatible with static type checking.
This paper proposes a structural type system for tracking changes to the interface of an object as methods are added and removed, and inheritance is changed at run time. The type system tracks the linearity of object and method references in order to ensure that objects whose interfaces change are not aliased. We show how our type system can express and enforce interesting protocol specifications. We then define a formal model of the language and type system, and prove that the type system is sound. Thus, our system is a foundation for languages that combine much of the power of dynamic languages like Self with the benefits of static typechecking.