## User Studies of Principled Model Finder Output

Tags: Verification, User Studies

*Posted on 01 July 2017.*

For decades, formal-methods tools have largely been evaluated on their
correctness, completeness, and mathematical foundations while
side-stepping or hand-waving questions of *usability*.
As a result, tools like model checkers,
model finders, and proof assistants can require years of expertise to
negotiate, leaving knowledgeable but uninitiated potential users at a loss.
This state of affairs must change!

One class of formal tool, model finders, provides concrete instances
of a specification, which can guide a user’s intuition or witness the
failure of desired properties. But are the examples produced actually
helpful? Which examples ought to be shown first? How should they be
presented, and what supplementary information can aid comprehension?
Indeed, *could they even hinder understanding*?

We’ve set out to answer these questions via disciplined user-studies. Where can we find participants for these studies? Ideally, we would survey experts. Unfortunately, it has been challenging to do so in the quantities needed for statistical power. As an alternative, we have begun to use formal methods students in Brown’s upper-level Logic for Systems class. The course begins with Alloy, a popular model-finding tool, so students are well suited to participate in basic studies. With this population, we have found some surprising results that call into question some intuitively appealing answers to (e.g.) the example-selection question.

For more information, see our paper.

Okay, that’s student populations. But there are only so many students in a class, and they take the class only so often, and it’s hard to “rewind” them to an earlier point in a course. Are there audiences we can use that don’t have these problems? Stay tuned for our next post.