{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,6,26]],"date-time":"2023-06-26T04:05:14Z","timestamp":1687752314827},"reference-count":62,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2012,8,21]],"date-time":"2012-08-21T00:00:00Z","timestamp":1345507200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Comput Math Organ Theory"],"published-print":{"date-parts":[[2013,9]]},"DOI":"10.1007\/s10588-012-9138-6","type":"journal-article","created":{"date-parts":[[2012,8,20]],"date-time":"2012-08-20T13:52:18Z","timestamp":1345470738000},"page":"288-312","source":"Crossref","is-referenced-by-count":13,"title":["Automatic validation and failure diagnosis of human-device interfaces using task analytic models and model checking"],"prefix":"10.1007","volume":"19","author":[{"given":"Matthew L.","family":"Bolton","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2012,8,21]]},"reference":[{"key":"9138_CR1","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1145\/225434.225459","volume-title":"Proceedings of the 1st conference on designing interactive systems","author":"GD Abowd","year":"1995","unstructured":"Abowd GD, Wang H, Monk AF (1995) A formal technique for automated dialogue development. In: Proceedings of the 1st conference on designing interactive systems. ACM Press, New York, pp\u00a0219\u2013226"},{"issue":"6","key":"9138_CR2","doi-asserted-by":"crossref","first-page":"547","DOI":"10.1007\/s10009-006-0008-8","volume":"8","author":"Y A\u00eft-Ameur","year":"2006","unstructured":"A\u00eft-Ameur Y, Baron M (2006) Formal and experimental validation approaches in HCI systems design based on a shared event B model. Int J Softw Tools Technol Transf 8(6):547\u2013563","journal-title":"Int J Softw Tools Technol Transf"},{"key":"9138_CR3","first-page":"732","volume-title":"Proceedings of the international conference on software engineering research and practice","author":"Y A\u00eft-Ameur","year":"2003","unstructured":"A\u00eft-Ameur Y, Baron M, Girard P (2003) Formal validation of HCI user tasks. In: Proceedings of the international conference on software engineering research and practice. CSREA Press, Las Vegas, pp\u00a0732\u2013738"},{"issue":"1","key":"9138_CR4","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1016\/j.cogsys.2004.09.008","volume":"6","author":"R Amant","year":"2005","unstructured":"Amant R, Freed A, Ritter F (2005) Specifying act-r models of user interaction with a goms language. Cogn Syst Res 6(1):71\u201388","journal-title":"Cogn Syst Res"},{"issue":"5","key":"9138_CR5","doi-asserted-by":"crossref","first-page":"545","DOI":"10.1016\/j.ssci.2007.01.001","volume":"45","author":"S Basnyat","year":"2007","unstructured":"Basnyat S, Palanque P, Schupp B, Wright P (2007) Formal socio-technical barrier modelling for safety-critical interactive systems design. Saf Sci 45(5):545\u2013565","journal-title":"Saf Sci"},{"key":"9138_CR6","volume-title":"Proceedings of the joint ESREL 2008 and 17th SRA-Europe conference","author":"S Basnyat","year":"2008","unstructured":"Basnyat S, Palanque PA, Bernhaupt R, Poupart E (2008) Formal modelling of incidents and accidents as a means for enriching training material for satellite control operations. In: Proceedings of the joint ESREL 2008 and 17th SRA-Europe conference. Taylor and Francis, London, CD\u2013ROM"},{"key":"9138_CR7","first-page":"1817","volume-title":"Proceedings of the IEEE international conference on systems, man, and cybernetics","author":"EJ Bass","year":"2011","unstructured":"Bass EJ, Bolton ML, Feigh K, Griffith D, Gunter E, Mansky W, Rushby J (2011) Toward a multi-method approach to formalizing human-automation interaction and human-human communications. In: Proceedings of the IEEE international conference on systems, man, and cybernetics. IEEE, Piscataway, pp 1817\u20131824"},{"issue":"6","key":"9138_CR8","doi-asserted-by":"crossref","first-page":"571","DOI":"10.1007\/s00165-008-0101-8","volume":"21","author":"TA Basuki","year":"2009","unstructured":"Basuki TA, Cerone A, Griesmayer A, Schlatte R (2009) Model-checking user behaviour using interacting components. Form Asp Comput 21(6):571\u2013588","journal-title":"Form Asp Comput"},{"key":"9138_CR9","unstructured":"Bolton ML (2010) Using task analytic behavior modeling, erroneous human behavior generation, and formal methods to evaluate the role of human-automation interaction in system failure. PhD thesis, University of Virginia, Charlottesville"},{"key":"9138_CR10","first-page":"764","volume-title":"Proceedings of the 53rd annual meeting of the human factors and ergonomics society","author":"ML Bolton","year":"2009","unstructured":"Bolton ML, Bass EJ (2009) A method for the formal verification of human interactive systems. In: Proceedings of the 53rd annual meeting of the human factors and ergonomics society. HFES, Santa Monica, pp\u00a0764\u2013768"},{"issue":"3","key":"9138_CR11","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/s11334-010-0129-9","volume":"6","author":"ML Bolton","year":"2010","unstructured":"Bolton ML, Bass EJ (2010a) Formally verifying human-automation interaction as part of a system model: limitations and tradeoffs. Innov Syst Softw Eng 6(3):219\u2013231","journal-title":"Innov Syst Softw Eng"},{"key":"9138_CR12","doi-asserted-by":"crossref","first-page":"2069","DOI":"10.1109\/ICSMC.2010.5641711","volume-title":"Proceedings of the 2010 IEEE international conference on systems, man, and cybernetics","author":"ML Bolton","year":"2010","unstructured":"Bolton ML, Bass EJ (2010b) Using task analytic models to visualize model checker counterexamples. In: Proceedings of the 2010 IEEE international conference on systems, man, and cybernetics. IEEE, Piscataway, pp 2069\u20132074"},{"key":"9138_CR13","doi-asserted-by":"crossref","unstructured":"Bolton ML, Bass EJ, Siminiceanu RI (2012) Using formal verification to evaluate human-automation interaction in safety critical systems, a review. IEEE Trans Syst Man Cybern, Part A, Syst Hum (accepted)","DOI":"10.1109\/TSMCA.2012.2210406"},{"issue":"5","key":"9138_CR14","doi-asserted-by":"crossref","first-page":"961","DOI":"10.1109\/TSMCA.2011.2109709","volume":"41","author":"ML Bolton","year":"2011","unstructured":"Bolton ML, Siminiceanu RI, Bass EJ (2011) A systematic approach to model checking human-automation interaction using task-analytic models. IEEE Trans Syst Man Cybern, Part A, Syst Hum 41(5):961\u2013976","journal-title":"IEEE Trans Syst Man Cybern, Part A, Syst Hum"},{"key":"9138_CR15","doi-asserted-by":"crossref","first-page":"663","DOI":"10.1002\/0471721174","volume-title":"Handbook of human systems integration","author":"H Booher","year":"2003","unstructured":"Booher H, Minninger J (2003) Human systems integration in army systems acquisition. In: Booher HR (ed) Handbook of human systems integration. Wiley, Hoboken, pp 663\u2013698"},{"issue":"3","key":"9138_CR16","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1016\/j.ress.2004.07.020","volume":"88","author":"J Bredereke","year":"2005","unstructured":"Bredereke J, Lankenau A (2005) Safety-relevant mode confusions\u2013modelling and reducing them. Reliab Eng Syst Saf 88(3):229\u2013245","journal-title":"Reliab Eng Syst Saf"},{"key":"9138_CR17","unstructured":"Brito R (2009) The algorithms bundle. http:\/\/carroll.aset.psu.edu\/pub\/CTAN\/macros\/latex\/contrib\/algorithms\/algorithms.pdf"},{"issue":"2","key":"9138_CR18","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch JR, Clarke EM, Dill DL, Hwang J, McMillan KL (1992) Symbolic model checking: 1020 states and beyond. Inf Comput 98(2):142\u2013171","journal-title":"Inf Comput"},{"issue":"2","key":"9138_CR19","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1207\/s15327108ijap1502_2","volume":"15","author":"M Byrne","year":"2005","unstructured":"Byrne M, Kirlik A (2005) Using computational cognitive modeling to diagnose possible sources of aviation error. Int J Aviat Psychol 15(2):135\u2013155","journal-title":"Int J Aviat Psychol"},{"key":"9138_CR20","first-page":"109","volume-title":"Proceedings of the fourth international Eurographics workshop on the design, specification, and verification of interactive systems","author":"JC Campos","year":"1997","unstructured":"Campos JC, Harrison M (1997) Formally verifying interactive systems: a review. In: Proceedings of the fourth international Eurographics workshop on the design, specification, and verification of interactive systems. Springer, Berlin, pp 109\u2013124"},{"key":"9138_CR21","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/978-3-540-70569-7_6","volume-title":"Proceedings of the 15th international workshop on the design, verification and specification of interactive systems","author":"JC Campos","year":"2008","unstructured":"Campos JC, Harrison MD (2008) Systematic analysis of control panel interfaces using formal tools. In: Proceedings of the 15th international workshop on the design, verification and specification of interactive systems. Springer, Berlin, pp 72\u201385"},{"key":"9138_CR22","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1145\/1570433.1570442","volume-title":"Proceedings of the 1st ACM SIGCHI symposium on engineering interactive computing systems","author":"JC Campos","year":"2009","unstructured":"Campos JC, Harrison MD (2009) Interaction engineering using the ivy tool. In: Proceedings of the 1st ACM SIGCHI symposium on engineering interactive computing systems. ACM Press, New York, pp 35\u201344"},{"key":"9138_CR23","doi-asserted-by":"crossref","first-page":"352","DOI":"10.1109\/SEFM.2005.19","volume-title":"Proceedings of the 3rd IEEE international conference on software engineering and formal methods","author":"A Cerone","year":"2005","unstructured":"Cerone A, PA Lindsay, Connelly S (2005) Formal analysis of human-computer interaction using model-checking. In: Proceedings of the 3rd IEEE international conference on software engineering and formal methods. IEEE Computer Society, Los Alamitos, pp 352\u2013362"},{"issue":"7","key":"9138_CR24","doi-asserted-by":"crossref","first-page":"1054","DOI":"10.1109\/21.391287","volume":"25","author":"RW Chu","year":"1995","unstructured":"Chu RW, Mitchell CM, Jones PM (1995) Using the operator function model and OFMspert as the basis for an intelligent tutoring system: towards a tutor\/aid paradigm for operators of supervisory control systems. IEEE Trans Syst Man Cybern, Part A, Syst Hum 25(7):1054\u20131075","journal-title":"IEEE Trans Syst Man Cybern, Part A, Syst Hum"},{"issue":"5","key":"9138_CR25","doi-asserted-by":"crossref","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E Clarke","year":"2003","unstructured":"Clarke E, Grumberg O, Jha S, Lu Y, Veith H (2003) Counterexample-guided abstraction refinement for symbolic model checking. J ACM 50(5):752\u2013794","journal-title":"J ACM"},{"issue":"1","key":"9138_CR26","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/BF00625969","volume":"9","author":"EM Clarke","year":"1996","unstructured":"Clarke EM, Enders R, Filkorn T, Jha S (1996) Exploiting symmetry in temporal logic model checking. Form Methods Syst Des 9(1):77\u2013104","journal-title":"Form Methods Syst Des"},{"key":"9138_CR27","volume-title":"Model checking","author":"EM Clarke","year":"1999","unstructured":"Clarke EM, Grumberg O, Peled DA (1999) Model checking. MIT Press, Cambridge"},{"key":"9138_CR28","doi-asserted-by":"crossref","first-page":"331","DOI":"10.1007\/3-540-36577-X_24","volume-title":"Proceedings of the 9th international conference on tools and algorithms for the construction and analysis of systems","author":"J Cobleigh","year":"2003","unstructured":"Cobleigh J, Giannakopoulou D, P\u0103s\u0103reanu C (2003) In: Proceedings of the 9th international conference on tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp.\u00a0331\u2013346"},{"key":"9138_CR29","unstructured":"De Moura L, Owre S, Shankar N (2003) The SAL language manual. Tech. Rep. CSL-01-01, Computer Science Laboratory, SRI International, Menlo Park"},{"key":"9138_CR30","first-page":"244","volume-title":"Proceedings of the sixth European software engineering conference","author":"MB Dwyer","year":"1997","unstructured":"Dwyer MB, Carr V, Hines L (1997) Model checking graphical user interfaces using abstractions. In: Proceedings of the sixth European software engineering conference. Springer, New York, pp 244\u2013261"},{"key":"9138_CR31","first-page":"154","volume-title":"Proceedings of the 19th IEEE international conference on automated software engineering","author":"MB Dwyer","year":"2004","unstructured":"Dwyer MB, Tkachuk O, Robby, Visser W (2004) Analyzing interaction orderings with model checking. In: Proceedings of the 19th IEEE international conference on automated software engineering. IEEE Computer Society, Los Alamitos, pp 154\u2013163"},{"key":"9138_CR32","first-page":"995","volume-title":"Handbook of theoretical computer science","author":"EA Emerson","year":"1990","unstructured":"Emerson EA (1990) Temporal and modal logic. In: van Leeuwen J, Meyer AR, Nivat M, Paterson M, Perrin D (eds) Handbook of theoretical computer science. MIT Press, Cambridge, Chap\u00a016, pp 995\u20131072"},{"key":"9138_CR33","doi-asserted-by":"crossref","first-page":"487","DOI":"10.1007\/978-3-540-73331-7_53","volume-title":"Proceedings of the 7th international conference on engineering psychology and cognitive ergonomics","author":"M Feary","year":"2007","unstructured":"Feary M (2007) Automatic detection of interaction vulnerabilities in an executable specification. In: Proceedings of the 7th international conference on engineering psychology and cognitive ergonomics. Springer, Berlin, pp 487\u2013496"},{"key":"9138_CR34","unstructured":"Fields RE (2001) Analysis of erroneous actions in the design of critical systems. PhD thesis, University of York, York"},{"key":"9138_CR35","first-page":"886","volume-title":"Proceedings of the IEEE international conference and systems, man, and cybernetics","author":"S G\u00f6knur","year":"2004","unstructured":"G\u00f6knur S, Bolton ML, Bass EJ (2004) Adding a motor control component to the operator function model expert system to investigate air traffic management concepts using simulation. In: Proceedings of the IEEE international conference and systems, man, and cybernetics. IEEE, Piscataway, pp 886\u2013892"},{"key":"9138_CR36","unstructured":"Hamon G, De Moura L, Rushby J (2005) Automated test generation with SAL. Tech. rep., Menlo Park. http:\/\/www.csl.sri.com\/users\/rushby\/papers\/salatg.pdf"},{"issue":"3","key":"9138_CR37","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1145\/98188.98191","volume":"8","author":"HR Hartson","year":"1990","unstructured":"Hartson HR, Siochi AC, Hix D (1990) The UAN: a user-oriented representation for direct manipulation interface designs. ACM Trans Inf Syst 8(3):181\u2013203","journal-title":"ACM Trans Inf Syst"},{"key":"9138_CR38","first-page":"197","volume-title":"Proceedings of the 7th international conference on formal description techniques","author":"G Holzmann","year":"1994","unstructured":"Holzmann G, Peled D (1994) An improvement in formal verification. In: Proceedings of the 7th international conference on formal description techniques. Chapman and Hall, London, pp 197\u2013211"},{"issue":"4","key":"9138_CR39","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1145\/235833.236050","volume":"3","author":"BE John","year":"1996","unstructured":"John BE, Kieras DE (1996) Using GOMS for user interface design and evaluation: which technique? ACM Trans Comput-Hum Interact 3(4):287\u2013319","journal-title":"ACM Trans Comput-Hum Interact"},{"issue":"3","key":"9138_CR40","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1007\/s10588-006-9001-8","volume":"13","author":"CM Jonker","year":"2007","unstructured":"Jonker CM, Schut MC, Treur J, Yolum P (2007) Analysis of meeting protocols by formalisation, simulation, and verification. Comput Math Organ Theory 13(3):283\u2013314","journal-title":"Comput Math Organ Theory"},{"key":"9138_CR41","first-page":"2.D.1-1","volume-title":"Proceedings of the 22nd digital avionics systems conference","author":"A Joshi","year":"2003","unstructured":"Joshi A, Miller SP, Heimdahl MP (2003) Mode confusion analysis of a flight guidance system using formal methods. In: Proceedings of the 22nd digital avionics systems conference. IEEE, Piscataway, pp 2.D.1-1\u20132.D.1-12"},{"key":"9138_CR42","first-page":"83","volume-title":"Goms models for task analysis","author":"D Kieras","year":"2003","unstructured":"Kieras D (2003) Goms models for task analysis. Lawrence Erlbaum Associates, Mahwah, pp 83\u2013116"},{"key":"9138_CR43","doi-asserted-by":"crossref","DOI":"10.1201\/b16826","volume-title":"A guide to task analysis","author":"B Kirwan","year":"1992","unstructured":"Kirwan B, Ainsworth LK (1992) A guide to task analysis. Taylor and Francis, London"},{"issue":"10","key":"9138_CR44","doi-asserted-by":"crossref","first-page":"863","DOI":"10.1109\/32.729686","volume":"24","author":"A Lecerof","year":"1998","unstructured":"Lecerof A, Patern\u00f2 F (1998) Automatic support for usability evaluation. IEEE Trans Softw Eng 24(10):863\u2013888","journal-title":"IEEE Trans Softw Eng"},{"key":"9138_CR45","first-page":"135","volume-title":"The handbook of task analysis for human-computer interaction","author":"Q Limbourg","year":"2003","unstructured":"Limbourg Q, Vanderdonckt J (2003) Comparing task models for user interface design. In: Diaper D, Stanton N (eds) The handbook of task analysis for human-computer interaction. Lawrence Erlbaum Associates, Mahwah, pp 135\u2013154"},{"issue":"4","key":"9138_CR46","doi-asserted-by":"crossref","first-page":"469","DOI":"10.1007\/s10515-006-7999-y","volume":"13","author":"K Loer","year":"2006","unstructured":"Loer K, Harrison MD (2006) An integrated framework for the analysis of dependable interactive systems (IFADIS): its tool support and evaluation. Autom Softw Eng 13(4):469\u2013496","journal-title":"Autom Softw Eng"},{"key":"9138_CR47","unstructured":"Mansouri-Samani M, Pasareanu CS, Penix JJ, Mehlitz PC, O\u2019Malley O, Visser WC, Brat GP, Markosian LZ, Pressburger TT (2007) Program model checking: a practitioner\u2019s guide. Tech. rep., Intelligent Systems Division, NASA Ames Research Center, Moffett Field"},{"issue":"3","key":"9138_CR48","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1109\/TSMC.1986.4308966","volume":"16","author":"CM Mitchell","year":"1986","unstructured":"Mitchell CM, Miller RA (1986) A discrete control model of operator function: a methodology for information display design. IEEE Trans Syst Man Cybern, Part A, Syst Hum 16(3):343\u2013357","journal-title":"IEEE Trans Syst Man Cybern, Part A, Syst Hum"},{"key":"9138_CR49","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/s10588-011-9093-7","volume":"17","author":"S Mueller","year":"2011","unstructured":"Mueller S, Simpkins B, Anno G, Fallon C, Price O, McClellan G (2011) Adapting the task-taxon-task methodology to model the impact of chemical protective gear. Comput Math Organ Theory 17:251\u2013271","journal-title":"Comput Math Organ Theory"},{"key":"9138_CR50","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/978-0-387-34907-7_11","volume-title":"Proceedings of the IFIP TC2\/WG2.7 working conference on engineering for human-computer interaction","author":"PA Palanque","year":"1996","unstructured":"Palanque PA, Bastide R, Senges V (1996) Validating interactive system design through the verification of formal task and system models. In: Proceedings of the IFIP TC2\/WG2.7 working conference on engineering for human-computer interaction. Chapman and Hall, London, pp\u00a0189\u2013212"},{"key":"9138_CR51","first-page":"379","volume-title":"Proceedings of the 24th national ACM conference","author":"DL Parnas","year":"1969","unstructured":"Parnas DL (1969) On the use of transition diagrams in the design of a user interface for an interactive computer system. In: Proceedings of the 24th national ACM conference. ACM Press, New York, pp\u00a0379\u2013385"},{"issue":"2","key":"9138_CR52","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1016\/S0953-5438(97)00015-5","volume":"9","author":"F Patern\u00f2","year":"1997","unstructured":"Patern\u00f2 F (1997) Formal reasoning about dialogue properties with automatic support. Interact Comput 9(2):173\u2013196","journal-title":"Interact Comput"},{"key":"9138_CR53","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/3-540-44675-3_9","volume-title":"Proceedings of the 7th international workshop on the design, specification, and verification of interactive systems","author":"F Patern\u00f2","year":"2001","unstructured":"Patern\u00f2 F, Santoro C (2001) Integrating model checking and HCI tools to help designers verify user interface properties. In: Proceedings of the 7th international workshop on the design, specification, and verification of interactive systems. Springer, Berlin, pp 135\u2013150"},{"key":"9138_CR54","first-page":"362","volume-title":"Proceedings of the IFIP TC13 international conference on human-computer interaction","author":"F Patern\u00f2","year":"1997","unstructured":"Patern\u00f2 F, Mancini C, Meniconi S (1997) Concurtasktrees: a diagrammatic notation for specifying task models. In: Proceedings of the IFIP TC13 international conference on human-computer interaction. Chapman and Hall, London, pp 362\u2013369"},{"key":"9138_CR55","first-page":"71","volume-title":"Proceedings of the 5th international conference on the design, specification, and verification of interactive systems","author":"F Patern\u00f2","year":"1998","unstructured":"Patern\u00f2 F, Santoro C, Tahmassebi S (1998) Formal model for cooperative tasks: concepts and an application for en-route air traffic control. In: Proceedings of the 5th international conference on the design, specification, and verification of interactive systems. Springer, Vienna, pp 71\u201386"},{"key":"9138_CR56","volume-title":"Human-system integration in the system development process: a new look","author":"R Pew","year":"2007","unstructured":"Pew R, Mavor A (2007) Human-system integration in the system development process: a new look. National Academies Press, Washington"},{"issue":"2","key":"9138_CR57","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1518\/155534307X232811","volume":"1","author":"F Ritter","year":"2007","unstructured":"Ritter F, Kukreja U, Amant R (2007) Including a model of visual processing with a cognitive architecture to model a simple teleoperation task. J Cogn Eng Decis Mak 1(2):121","journal-title":"J Cogn Eng Decis Mak"},{"issue":"3","key":"9138_CR58","doi-asserted-by":"crossref","first-page":"592","DOI":"10.1109\/TSMCA.2005.853482","volume":"36","author":"FE Ritter","year":"2006","unstructured":"Ritter FE, Van Rooy D, Amant RS, Simpson K (2006) Providing user models direct access to interfaces: an exploratory study of a simple interface with implications for HRI and HCI. IEEE Trans Syst Man Cybern, Part A, Syst Hum 36(3):592\u2013601","journal-title":"IEEE Trans Syst Man Cybern, Part A, Syst Hum"},{"issue":"6","key":"9138_CR59","doi-asserted-by":"crossref","first-page":"541","DOI":"10.1007\/s00165-008-0102-7","volume":"21","author":"R Ruk\u0161enas","year":"2009","unstructured":"Ruk\u0161enas R, Back J, Curzon P, Blandford A (2009) Verification-guided modelling of salience and cognitive load. Form Asp Comput 21(6):541\u2013569","journal-title":"Form Asp Comput"},{"issue":"2","key":"9138_CR60","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1016\/S0951-8320(01)00092-8","volume":"75","author":"J Rushby","year":"2002","unstructured":"Rushby J (2002) Using model checking to help discover mode confusions and other automation surprises. Reliab Eng Syst Saf 75(2):167\u2013177","journal-title":"Reliab Eng Syst Saf"},{"key":"9138_CR61","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/3-540-44518-8_16","volume-title":"Proceedings of the international workshop on abstract state machines, theory and applications","author":"N Shankar","year":"2000","unstructured":"Shankar N (2000) Symbolic analysis of transition systems. In: Proceedings of the international workshop on abstract state machines, theory and applications. Springer, London, pp 287\u2013302"},{"issue":"9","key":"9138_CR62","first-page":"10","volume":"23","author":"JM Wing","year":"1990","unstructured":"Wing JM (1990) A specifier\u2019s introduction to formal methods. Computer 23(9):8, 10\u201322, 24","journal-title":"Computer"}],"container-title":["Computational and Mathematical Organization Theory"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10588-012-9138-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10588-012-9138-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10588-012-9138-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,25]],"date-time":"2023-06-25T10:46:10Z","timestamp":1687689970000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10588-012-9138-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,8,21]]},"references-count":62,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2013,9]]}},"alternative-id":["9138"],"URL":"https:\/\/doi.org\/10.1007\/s10588-012-9138-6","relation":{},"ISSN":["1381-298X","1572-9346"],"issn-type":[{"value":"1381-298X","type":"print"},{"value":"1572-9346","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,8,21]]}}}