Exploring the design of an intentional 
naming scheme using an automatic constraint analyzer






constraint satisfaction, model checking, formal specifications, software 
analysis, dynamic networks


Lightweight formal modeling and automatic analysis 
were used to explore the design of 
Intentional Naming (IN), a new scheme for 
resource discovery in a dynamic networked environment. 
We constructed a model of IN in 
Alloy, a lightweight relational notation, and analyzed 
it with Alcoa, a fully automatic simulation 
and checking tool. In doing so, we 
exposed several serious flaws in both the 
algorithm of IN and the underlying naming 
semantics. We were able to characterize the 
conditions under which the existing IN scheme 
works correctly, and evaluate proposed fixes.