Using model checking to help discover mode confusions and other automation surprises

Bowman, 1999, Analysing cognitive behavior using LOTOS and Mexitl, Form Asp Comput, 11, 132, 10.1007/s001650050045 Butler RW, Miller SP, Potts JN, Carreño VA. A formal methods approach to the analysis of mode confusion. In 17th AIAA/IEEE Digital Avionics Systems Conference, Bellevue, WA, October 1998. Clarke, 1986, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Trans Program Lang Syst, 8, 244, 10.1145/5397.5399 Clarke, 1999 Crow, 1998, Formalizing space shuttle software requirements: four case studies, ACM Trans Software Engng Method, 7, 296, 10.1145/287000.287023 Degani, 2000, Pilot–autopilot interaction: a formal perspective, 157 Dill, 1996, The Murø verification system, vol. 1102 Duke, 1999, The formalization of a cognitive architecture and its application to reasoning about human–computer interaction, Form Asp Comput, 11, 665, 10.1007/s001659970004 The interfaces between flightcrews and modern flight deck systems. Report of the FAA human factors team, Federal Aviation Administration, 1995. http://www.faa.gov/avr/afs/interfac.pdf. Halpern, 1991 Javaux, 1999, A method for predicting errors when interacting with finite state machines Johnson-Laird, 1989 Leveson NG, Palmer E. Designing automation to reduce operator errors. In Proceedings of the IEEE Systems, Man, and Cybernetics Conference, October 1997. http://www.cs.washington.edu/research/projects/safety/www/papers/smc.ps. Leveson NG, Pinnel LD, Sandys SD, Koga S, Rees JD. Analyzing software specifications for mode confusion potential. In Johnson CW. editor. Proceedings of a Workshop on Human Error and System Development, p. 132–46, Glasgow Accident Analysis Group, technical report GAAG-TR-97-2, Glasgow, Scotland, March 1997. http://www.cs.washington.edu/research/projects/safety/www/papers/glascow.ps (sic). Norman, 1988 Palmer E. ‘Oops, it didn't arm.’ A case study of two automation surprises. In Jensen RS, Rakovan LA. editors. Proceedings of the Eighth International Symposium on Aviation Psychology, p. 227–32, The Aviation Psychology Laboratory, Department of Aerospace Engineering, Ohio State University, Columbus, OH, April 1995. http://olias.arc.nasa.gov/ev/OSU95_Oops/PalmerOops.html. Roscoe, 1994 Rushby J. Combining system properties: a cautionary example and formal examination. Computer Science Laboratory, SRI International, Menlo Park, CA, June 1995. Unpublished project report; included in the Murø distribution, http://www.csl.sri.com/~rushby/combined.html. Sage, 1999, Formally verified, rapid prototyping for air traffic control Sarter, 1995, How in the world did we ever get into that mode? Mode error and awareness in supervisory control, Human Factors, 37, 5, 10.1518/001872095779049516 Sarter, 1997, Automation surprises Vakil, 1999, Approaches to mitigating complexity-driven issues in commercial autoflight systems