Recent accounts of accidents draw attention to ''automation surprises'' that arise in safety critical systems. An automation surprise can occur w hen a system behaves differently from the expectations of the operator. Interface mode changes are one class of such surprises that have significant impact on the sa fety of a dynamic interactive system. They may take place implicitly as a result of other system action. Formal specifications of interactive systems provide an opportunity to analyse problems that arise in such systems. In this paper we consider the role that an interactor based specification has as a partial mode l of an interactive system so that mode consequences can be checked early in the design process. We show how interactor specifications can be translated into the SMV model checker input language and how we can use such specifications in conjunction with the model checker to analyse potential for mode confusion in a realistic cas e. Our final aim is to develop a general purpose methodology for the automated analysis of interactive systems. This verification process can be useful in raising qu estions that have to be addressed in a broader context of analysis.

download