Abstract
Mode confusion situations or more general automation surprises can arise in the context of sophisticated control systems which require the interaction with human operators as for example flight monitoring systems in airplanes. A “mode” is defined by a subset of system variables the values of which determine distinguishable forms of system behaviour. Critical situations can arise if the operator interacts with the system assuming a wrong mode. The identification and analysis of such situations needs to take into account both the system design and the operators mental model of the system. Recent research showed that model-checking techniques are useful for identifying mode-confusion situations. Two different approaches can be found: the first tries to identify mode confusion potential in system design, the second analyses actual mode confusion situations to identify the discrepancies between the mental model of operators and the system design. This paper reports an experiment in using the model-checker FDR2 for comparing system and mental models based on CSP refinement. In contrast to earlier attempts using model-checkers for this task, this approach allows a direct comparison of the two models which can be easily derived from a rule-based description.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Sarter, N., Woods, D., Billings, C.: Automation surprises. In: Salvendy, G. (ed.) Handbook of Human Factors and Ergonomics, 2nd edn. John Wiley and Sons, Chichester (1997)
Levevson, N.G., Pinnel, L.D., Sandys, S.D., Koga, S., Rees, J.D.: Analyzing software specifications for mode confusion potential. In: Johnson, C.W. (ed.) Proceedings of a Workshop on Human Error and System Development, Glasgow, Scotland. Glasgow Accident Analysis Group, Technical Report GAAG-TR-97-2, March 1997, pp. 132–146 (1997)
Miller, S., Potts, J.: Detecting mode confusion through formal modeling and analysis. Technical Report NASA/CR-1999-208971, NASA Langley Research Center (January 1999), available at: http://shemesh.larc.nasa.gov/fm/fm-pubs-larc.html
Lüttgen, G., Carreño, V.: Analyzing mode confusion via model checking. Technical Report NASA/CR-1999-209332, ICASE Report No. 99-18, ICASE - NASA Langley Research Center (May 1999), available at: http://shemesh.larc.nasa.gov/fm/fm-pubs-icase.html
Rushby, J.: Using model checking to help discover mode confusions and other automation surprises. In: Javaux, D. (ed.) Proceedings of the 3rd Workshop on Human Error, Safety, and System Development (HESSD 1999). University of Liege, Belgium (1999)
Rushby, J.: Using model checking to help discover mode confusions and other automation surprises. Reliability Engineering and System Safety 75, 167–177 (2002), available at: http://www.csl.sri.com/users/rushby/abstracts/ress02
Dill, D.: The Murφ verification system. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102. Springer, Heidelberg (1996)
Rushby, J., Crow, J., Palmer, E.: An automated method to detect potential mode confusions. In: 18th AIAA/IEEE Digital Avionics Systems Conference, St Louis, MO (1999)
Palmer, E.: “Oops, it didn’t arm.” A case study of two automation surprises. In: Jensen, R.S., Rakovan, L.A. (eds.) Proceedings of the Eightth International Symposium on Aviation Psychology, Columbus, OH. The Aviation Psychology Department of Aerospace Engineering, Ohio State University, April 1995, pp. 227–232 (1995), available at: http://human-factors.arc.nasa.gov/IHpersonnel/ev
Leveson, N.G., Palmer, E.: Designing automation to reduce operator errors. In: Proceedings of the IEEE Systems, Man, and Cybernetics Conference (1997)
Formal Systems (Europe) Lts: FDR2 User Manual (1997), Available under: http://www.formal.demon.co.uk/fdr2manual/index.html
Buth, B.: Formal and Semi-Formal Methods for the Analysis of Industrial Control Systems. BISS Monographs, vol. 15 (2002) (Habilitationsschrift submitted May 2001)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall International, Englewood Cliffs (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Buth, B. (2004). Analysing Mode Confusion: An Approach Using FDR2. In: Heisel, M., Liggesmeyer, P., Wittmann, S. (eds) Computer Safety, Reliability, and Security. SAFECOMP 2004. Lecture Notes in Computer Science, vol 3219. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30138-7_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-30138-7_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23176-9
Online ISBN: 978-3-540-30138-7
eBook Packages: Springer Book Archive