PLURAL: checking protocol compliance under aliasing

Enforcing compliance to API usage protocols is notoriously hard due to possible aliasing of objects through multiple references. In previous work we proposed a sound, modular approach to checking protocol compliance based on typestates that offers a great deal of flexibility in aliasing [1]. In our approach, API protocols are defined based on typestates. Every reference is associated with a permission, and reasoning about permissions is appropriately conservative for the "degree" of possible aliasing admitted by a permission. This paper describes Plural, a tool to automatically enforce typestate-based protocols using permissions in Java. API developers can specify protocols with simple annotations on methods and method parameters. A static flow analysis tracks permissions in code that uses specified APIs and issues warnings for possible protocol violations. Categories and Subject Descriptors D.2.2 [Software Engineering]: Design Tools and Techniques--Object-oriented programmi...

• Type: Conference
• Year: 2008
• Where: ICSE
• Authors: Kevin Bierhoff, Jonathan Aldrich
• Keywords: Analysis Tracks Permissions, API Protocols, ICSE 2008, Possible Aliasing, Software Engineering