Current research on this
topic includes exploring mechanisms for proving properties of
specifications interactive behaviour using model checkers [Campos &
Harrison, 2001, 2003]. This work focuses on the IVY tool developed by Jose Campos at
University of Minho
which
supports the instantiation of standard property templates to a
particular model. These templates can be applied systematically to
analyse
interactive devices [Campos & Harrison, 2008, 2009] and the use of
information resources to restrict analysis to cognitively plausible
paths [Doherty, Campos & Harrison, 2008, Dittmar & Harrison,
2010].