Abstract. In this paper we argue that using verification in interactive systems development is more than just checking whether the specification of the system has all the required properties; and that changing the focus from a global specification into partial, property oriented, specifications can provide a number of advantages and make verification act as an aid to decision making. We also present a compiler that allows for the verification of interactor specifications to be done in SMV, as well as a simple case study where verification is used to inform a design decision.
José Creissac Campos, Michael D. Harrison