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:
Post a Comment