José C. Campos

Citation:

Campos JC, Harrison M.  1999.  From Interactors to SMV: A Case Study in the Automated Analysis of Interactive Systems, copy at www.tinyurl.com/okzoz7t

Abstract:

Recent accounts of accidents have drawn attention to problems that arise in safety critical systems through “automation surprises”. A particular class of such surprises, interface mode changes, may have significant impact on the safety of a dynamic interactive system and may take place implicitly as a result of other system action. Formal specifications of interactive systems may provide an opportunity to analyse problems that arise in such systems. In this paper we consider the role that an interactor based specification may have as a partial model of an interactive system, so that mode consequences might 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 case. Our final aim is to develop a general purpose methodology for the automated analysis of interactive systems, and, in this context, we show how the verification process can be useful by raising questions that have to be addressed in a broader context of analysis.

Citation Key: