Case Study in Alloy Modeling: A Common Profile for Presence

Using Alloy as a software modeling tool, I conducted a case study of a presence protocol by the Instant Messaging and Presence Protocol working group. I questioned major design choices and uncovered inconsistencies in the Common Profile for Presence protocol – a protocol that enables a client to subscribe to other clients and subsequently receive notifications regarding changes in the presence information of those clients. In this paper, I present the results of my modeling experience. Both the formal analysis of the final model and the rigorous thinking that accompanied the construction of the model evoked a reconsideration of areas of interest; these areas of interest included protocol operations, subscription management, multi-located clients, privacy concerns, and asynchronous notifications. My purpose in conducting this case study is to aid the working group in its development of the instant messaging and presence protocols and to demonstrate the utility of abstract modeling in the early stages of software design. In the absence of this modeling, the issues described in this paper might have propagated into the implementation phase of the protocol, thereby wasting future time and effort investments. Software modeling thus serves as an invaluable thinking aid during design