Model Checking Interactor Specifications Export

@article{citeulike:4007515, abstract = {Recent accounts of accidents draw attention to ” automation surprises” that arise in safety critical systems. An automation surprise can occur when 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 safety 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 model 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 case. 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 questions that have to be addressed in a broader context of analysis.}, author = {Campos, Jos\'{e} C. and Harrison, Michael D.}, citeulike-article-id = {4007515}, citeulike-linkout-0 = {http://dx.doi.org/10.1023/A:1011265604021}, citeulike-linkout-1 = {http://www.springerlink.com/content/m67k51042wk27604}, day = {1}, doi = {10.1023/A:1011265604021}, journal = {Automated Software Engineering}, keywords = {2004, gui, modelchecking, specification, verification}, number = {3}, pages = {275--310}, posted-at = {2009-02-04 13:37:26}, priority = {5}, title = {Model Checking Interactor Specifications}, url = {http://dx.doi.org/10.1023/A:1011265604021}, volume = {8}, year = {2001} }

TY - JOUR ID - citeulike:4007515 L3 - citeulike-article-id:4007515 N2 - Recent accounts of accidents draw attention to “automation surprises” that arise in safety critical systems. An automation surprise can occur when 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 safety 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 model 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 case. 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 questions that have to be addressed in a broader context of analysis. IS - 3 JF - Automated Software Engineering EP - 310 TI - Model Checking Interactor Specifications VL - 8 SP - 275 KW - 2004 KW - gui KW - modelchecking KW - specification KW - verification AU - Campos, José AU - Harrison, Michael PY - 2001//01/ UR - http://dx.doi.org/10.1023/A:1011265604021 ER -