Tuesday, June 20, 2006

reading papers: Exploring the Design of an Intentional Naming Scheme with an Automatic Constraint Analyzer

Notes to self on http://sdg.csail.mit.edu/pubs/2000/INS_ASE00.pdf. I'm revising this as I read more.

Shallow summary: the authors use Alloy, a model checker, to validate the design of the Intentional Naming System (INS); along the way, they show that INS has flaws in it. They use Alloy as a counterexample generator and as a tool to explore INS's design.

What questions does the paper ask?

* When does INS break?
* When does it work?
* Can we use the model to describe general properties for any intentional naming system?

Why is this novel?

* It's another data point showing that model checking can be used effectively in real world applications.
* It shows, in particular, that Alloy can handle the modeling of complex data structures. This is a new application of Alloy to a recursive algorithm (Lookup-Name) that has not been done before.

No comments: