{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T04:21:18Z","timestamp":1775881278397,"version":"3.50.1"},"reference-count":47,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2014,11,13]],"date-time":"2014-11-13T00:00:00Z","timestamp":1415836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Autom Softw Eng"],"published-print":{"date-parts":[[2015,6]]},"DOI":"10.1007\/s10515-014-0157-z","type":"journal-article","created":{"date-parts":[[2014,11,14]],"date-time":"2014-11-14T20:19:56Z","timestamp":1415996396000},"page":"159-197","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Building high assurance human-centric decision systems"],"prefix":"10.1007","volume":"22","author":[{"given":"Constance L.","family":"Heitmeyer","sequence":"first","affiliation":[]},{"given":"Marc","family":"Pickett","sequence":"additional","affiliation":[]},{"given":"Elizabeth I.","family":"Leonard","sequence":"additional","affiliation":[]},{"given":"Myla M.","family":"Archer","sequence":"additional","affiliation":[]},{"given":"Indrakshi","family":"Ray","sequence":"additional","affiliation":[]},{"given":"David W.","family":"Aha","sequence":"additional","affiliation":[]},{"given":"J. Gregory","family":"Trafton","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,11,13]]},"reference":[{"key":"157_CR1","unstructured":"Alspaugh, T.A., Faulk, S.R., Britton, K.H., Parker, R.A., Parnas, D.L., Shore, J.E.: Software requirements for the A-7E aircraft. Tech. Rep. NRL-9194, Naval Research Laboratory, Washington, DC (1992)"},{"key":"157_CR2","first-page":"114","volume-title":"Proceedings of the 10th International Conference on Concurrency Theory (CONCUR)","author":"R Alur","year":"1999","unstructured":"Alur, R., Yannakakis, M.: Model checking of Message Sequence Charts. Proceedings of the 10th International Conference on Concurrency Theory (CONCUR), pp. 114\u2013129. Eindhoven, The Netherlands (1999)"},{"issue":"1\u20134","key":"157_CR3","first-page":"131","volume":"29","author":"M Archer","year":"2001","unstructured":"Archer, M.: TAME: Using PVS strategies for special-purpose theorem proving. Ann Math Artif Intell 29(1\u20134), 131\u2013189 (2001)","journal-title":"Ann Math Artif Intell"},{"key":"157_CR4","doi-asserted-by":"crossref","unstructured":"Bharadwaj, R., Heitmeyer, C.: Developing high assurance avionics systems with the SCR requirements method. In: Proceedings of the 19th Digital Avionics Systems Conference (DASC), Philadelphia, Pennsylvania (2000)","DOI":"10.1109\/DASC.2000.886888"},{"key":"157_CR5","unstructured":"Boussemart, Y., Cummings, M.: Behavioral recognition and prediction of an operator supervising multiple heterogeneous unmanned vehicles. In: Proceedings of the 1st International Conference on Humans Operating Unmanned Systems (HUMOUS), Brest, France (2008)"},{"issue":"1","key":"157_CR6","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1109\/TSMC.2013.2293317","volume":"44","author":"LA Breslow","year":"2014","unstructured":"Breslow, L.A., Gartenberg, D., McCurry, J.M., Trafton, J.G.: Dynamic operator overload: A model for predicting workload during supervisory control. IEEE Trans Hum Mach Syst 44(1), 30\u201340 (2014)","journal-title":"IEEE Trans Hum Mach Syst"},{"key":"157_CR7","unstructured":"Bumiller, E., Shanker, T.: War evolves with drones, some tiny as bugs. New York Times, (2011)"},{"key":"157_CR8","doi-asserted-by":"crossref","unstructured":"Crandall, J.W., Goodrich, M.A., D R Olsen, J., Nielsen, C.W.: Validating human-robot systems in multi-tasking environments. IEEE Transactions on Systems, Man, and Cybernetics 35(4), 438\u2013449 (2005)","DOI":"10.1109\/TSMCA.2005.850587"},{"issue":"2","key":"157_CR9","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1109\/TSMCA.2007.914757","volume":"38","author":"ML Cummings","year":"2008","unstructured":"Cummings, M.L., Mitchell, P.J.: Predicting controller capacity in supervisory control of multiple UAVs. IEEE Trans Syst Man Cybern 38(2), 451\u2013460 (2008)","journal-title":"IEEE Trans Syst Man Cybern"},{"issue":"12","key":"157_CR10","doi-asserted-by":"crossref","first-page":"1056","DOI":"10.1109\/TSE.2005.138","volume":"31","author":"C Damas","year":"2005","unstructured":"Damas, C., Lambeau, B., Dupont, P., van Lamsweerde, A.: Generating annotated behavior models from end-user scenarios. IEEE Trans Softw Eng 31(12), 1056\u20131073 (2005)","journal-title":"IEEE Trans Softw Eng"},{"key":"157_CR11","doi-asserted-by":"crossref","unstructured":"Damas, C., Lambeau, B., Roucoux, F., van Lamsweerde, A.: Analyzing critical process models through behavior model synthesis. In: Proceedings of the 31st International Conference on Software Engineering (ICSE), pp. 241\u2013251. Vancouver, Canada (2009)","DOI":"10.1109\/ICSE.2009.5070543"},{"key":"157_CR12","unstructured":"DSB: The role of autonomy in DoD systems. Tech. rep., Defense Science Board, Office of the Under Secretary of Defense for Acquisition, Technology and Logistics, Washington, DC (2012)"},{"issue":"8","key":"157_CR13","doi-asserted-by":"crossref","first-page":"861","DOI":"10.1016\/j.patrec.2005.10.010","volume":"27","author":"T Fawcett","year":"2006","unstructured":"Fawcett, T.: An introduction to ROC analysis. Pattern Recognit Lett 27(8), 861\u2013874 (2006)","journal-title":"Pattern Recognit Lett"},{"key":"157_CR14","doi-asserted-by":"crossref","unstructured":"Gargantini, A., Heitmeyer, C.: Using model checking to generate tests from requirements specifications. In: Proceedings of the 7th European Software Engineering Conference and 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC\/FSE), pp. 146\u2013162. Toulouse, France (1999)","DOI":"10.1007\/3-540-48166-4_10"},{"key":"157_CR15","doi-asserted-by":"crossref","unstructured":"Gartenberg, D., Breslow, L., Park, J., McCurry, J., Trafton, J.: Adaptive automation and cue invocation: The effect of cue timing on operator error. In: Proceedings of the ACM SIGCHI Conference on Human Factors in Computing Systems (CHI), pp. 3121\u20133130. France, Paris (2013)","DOI":"10.1145\/2470654.2466426"},{"key":"157_CR16","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1145\/949952.940106","volume":"28","author":"D Giannakopoulou","year":"2003","unstructured":"Giannakopoulou, D., Magee, J.: Fluent model checking for event-based systems. ACM SIGSOFT Softw Eng Notes 28, 257\u2013266 (2003)","journal-title":"ACM SIGSOFT Softw Eng Notes"},{"issue":"4","key":"157_CR17","first-page":"322","volume":"6","author":"WD Gray","year":"2000","unstructured":"Gray, W.D., Boehm-Davis, D.A.: Milliseconds matter: An introduction to microstrategies and to their use in describing and predicting interactive behavior. J Exp Psychol 6(4), 322 (2000)","journal-title":"J Exp Psychol"},{"issue":"1","key":"157_CR18","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1007\/s12021-008-9041-y","volume":"7","author":"M Hanke","year":"2009","unstructured":"Hanke, M., Halchenko, Y.O., Sederberg, P.B., Olivetti, E., Fr\u00fcnd, I., Rieger, J.W., Herrmann, C.S., Haxby, J.V., Hanson, S.J., Pollmann, S.: PyMVPA: a Python toolbox for multivariate pattern analysis of fMRI data. Neuroinformatics 7(1), 37\u201353 (2009)","journal-title":"Neuroinformatics"},{"key":"157_CR19","doi-asserted-by":"crossref","unstructured":"Heitmeyer, C., Jeffords, R.: Applying a formal requirements method to three NASA systems: Lessons learned. In: Proceedings of the IEEE Aerospace Conference, Big Sky, Montana, p 84 (2007)","DOI":"10.1109\/AERO.2007.352764"},{"issue":"11","key":"157_CR20","doi-asserted-by":"crossref","first-page":"927","DOI":"10.1109\/32.730543","volume":"24","author":"C Heitmeyer","year":"1998","unstructured":"Heitmeyer, C., Kirby, J., Labaw, B., Archer, M., Bharadwaj, R.: Using abstraction and model checking to detect safety violations in requirements specifications. IEEE Trans Softw Eng 24(11), 927\u2013948 (1998)","journal-title":"IEEE Trans Softw Eng"},{"issue":"1","key":"157_CR21","first-page":"19","volume":"20","author":"C Heitmeyer","year":"2005","unstructured":"Heitmeyer, C., Archer, M., Bharadwaj, R., Jeffords, R.: Tools for constructing requirements specifications: The SCR toolset at the age of ten. Comput Syst Sci Eng 20(1), 19\u201335 (2005)","journal-title":"Comput Syst Sci Eng"},{"key":"157_CR22","doi-asserted-by":"crossref","unstructured":"Heitmeyer, C., Pickett, M., Breslow, L., Aha, D., Trafton, J.G., Leonard, E.: High assurance human-centric decision systems. In: Proc of the 2nd International NSF-Sponsored Workshop on Realizing Artificial Intelligence Synergies in Software Engineering (RAISE) (2013a)","DOI":"10.1109\/RAISE.2013.6615202"},{"issue":"3","key":"157_CR23","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1145\/234426.234431","volume":"5","author":"CL Heitmeyer","year":"1996","unstructured":"Heitmeyer, C.L., Jeffords, R.D., Labaw, B.G.: Automated consistency checking of requirements specifications. ACM Trans Softw Eng Methodol 5(3), 231\u2013261 (1996)","journal-title":"ACM Trans Softw Eng Methodol"},{"issue":"1","key":"157_CR24","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1109\/TSE.2007.70772","volume":"34","author":"CL Heitmeyer","year":"2008","unstructured":"Heitmeyer, C.L., Archer, M.M., Leonard, E.I., McLean, J.D.: Applying formal methods to a certifiably secure software system. IEEE Trans Softw Eng 34(1), 82\u201398 (2008)","journal-title":"IEEE Trans Softw Eng"},{"key":"157_CR25","doi-asserted-by":"crossref","unstructured":"Heitmeyer, C.L., Shukla, S., Archer, M.M., Leonard, E.I.: On model-based software development. In: Munch, J., Schmid, K. (eds) Perspectives on the Future of Software Engineering, Springer, Berlin, Germany, pp 49\u201360 (2013b)","DOI":"10.1007\/978-3-642-37395-4_4"},{"issue":"1","key":"157_CR26","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1109\/TSE.1980.230208","volume":"6","author":"KL Heninger","year":"1980","unstructured":"Heninger, K.L.: Specifying software requirements for complex systems: New techniques and their application. IEEE Trans Softw Eng 6(1), 2\u201313 (1980)","journal-title":"IEEE Trans Softw Eng"},{"key":"157_CR27","unstructured":"ITU: Message Sequence Charts. Recommendation Z.120, Intern. Telecomm. Union, Telecomm. Standardization Sector (1999)"},{"key":"157_CR28","doi-asserted-by":"crossref","unstructured":"Jeffords, R., Heitmeyer, C.: Automatic generation of state invariants from requirements specifications. In: Proceedings of the 6th ACM SIGSOFT Symposium on Foundations of Software Engineering (FSE), pp. 56\u201369. Lake Buena Vista, Florida (1998)","DOI":"10.1145\/291252.288218"},{"key":"157_CR29","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1145\/949952.940077","volume":"28","author":"RD Jeffords","year":"2003","unstructured":"Jeffords, R.D., Heitmeyer, C.L.: A strategy for efficiently verifying requirements. ACM SIGSOFT Softw Eng Notes 28, 28\u201337 (2003)","journal-title":"ACM SIGSOFT Softw Eng Notes"},{"issue":"4","key":"157_CR30","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1016\/0010-0285(76)90015-3","volume":"8","author":"MA Just","year":"1976","unstructured":"Just, M.A., Carpenter, P.A.: Eye fixations and cognitive processes. Cogn Psychol 8(4), 441\u2013480 (1976)","journal-title":"Cogn Psychol"},{"key":"157_CR31","doi-asserted-by":"crossref","unstructured":"Kira, K., Rendell, L.A.: A practical approach to feature selection. In: Proceedings of the 9th International Workshop on Machine Learning (ML), pp. 249\u2013256. Aberdeen, Scotland (1992)","DOI":"10.1016\/B978-1-55860-247-2.50037-1"},{"issue":"1\u20132","key":"157_CR32","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1023\/A:1023072104553","volume":"16","author":"EI Leonard","year":"2003","unstructured":"Leonard, E.I., Heitmeyer, C.L.: Program synthesis from formal requirements specifications using APTS. High Order Symb Comput 16(1\u20132), 63\u201392 (2003)","journal-title":"High Order Symb Comput"},{"key":"157_CR33","doi-asserted-by":"crossref","unstructured":"Leonard, E.I., Archer, M., Heitmeyer, C.L., Jeffords, R.D.: Direct generation of invariants for reactive models. In: Proc. 10th ACM\/IEEE Conference on Formal Methods and Models for Co-Design (MEMOCODE), pp 119\u2013130 (2012)","DOI":"10.1109\/MEMCOD.2012.6292308"},{"key":"157_CR34","unstructured":"Pickett, M., Aha, D.W., Trafton, J.G.: Acquiring user models to test automated assistants. In: Proceedings of the 26th International Florida Artificial Intelligence Research Society Conference (FLAIRS), pp 112\u2013117 (2013)"},{"issue":"3","key":"157_CR35","first-page":"205","volume":"26","author":"R Ratwani","year":"2011","unstructured":"Ratwani, R., Trafton, J.G.: A real-time eye tracking system for predicting postcompletion errors. Hum Comput Interact 26(3), 205\u2013245 (2011)","journal-title":"Hum Comput Interact"},{"issue":"3","key":"157_CR36","doi-asserted-by":"crossref","first-page":"372","DOI":"10.1037\/0033-2909.124.3.372","volume":"124","author":"K Rayner","year":"1998","unstructured":"Rayner, K.: Eye movements in reading and information processing: 20 years of research. Psychol Bull 124(3), 372 (1998)","journal-title":"Psychol Bull"},{"key":"157_CR37","unstructured":"Rayner, K., Morris, R.K.: Do eye movements reflect higher order processes in reading? In: From Eye to Mind. Information Acquisition in Perception, Search, and Reading, North-Holland, pp 191\u2013204 (1990)"},{"key":"157_CR38","doi-asserted-by":"crossref","unstructured":"Rothamel, T., Heitmeyer, C., Leonard, E., Liu, A.: Generating optimized code from SCR specifications. In: Proceedings of the ACM SIGPLAN\/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2006) (2006)","DOI":"10.1145\/1134650.1134670"},{"key":"157_CR39","first-page":"385","volume-title":"Proceedings of the 9th International Workshop on Machine Learning (ML)","author":"C Sammut","year":"1992","unstructured":"Sammut, C., Hurst, S., Kedzier, D., Michie, D.: Learning to fly. In: Sleeman, D.H., Edwards, P. (eds.) Proceedings of the 9th International Workshop on Machine Learning (ML), pp. 385\u2013393. Morgan Kaufmann, Aberdeen, Scotland (1992)"},{"issue":"5","key":"157_CR40","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1109\/MS.2003.1231146","volume":"20","author":"B Selic","year":"2003","unstructured":"Selic, B.: The pragmatics of model-driven development. IEEE Softw 20(5), 19\u201325 (2003)","journal-title":"IEEE Softw"},{"key":"157_CR41","unstructured":"Sengupta, S.: U.S. border agency allows others to use its drones. New York Times, (2013)"},{"key":"157_CR42","doi-asserted-by":"crossref","unstructured":"\u0160uc, D., Bratko, I., Sammut, C.: Learning to fly simple and robust. In: Proceedings of the 15th European Conference on Machine Learning (ECML), pp. 407\u2013418. Pisa, Italy (2004)","DOI":"10.1007\/978-3-540-30115-8_38"},{"key":"157_CR43","volume-title":"Signal detection theory and ROC analysis in psychology and diagnostics: Collected Papers","author":"JA Swets","year":"1996","unstructured":"Swets, J.A.: Signal detection theory and ROC analysis in psychology and diagnostics: Collected Papers. Lawrence Erlbaum Associates, Mahawa (1996)"},{"issue":"2","key":"157_CR44","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1109\/TSE.2003.1178048","volume":"29","author":"S Uchitel","year":"2003","unstructured":"Uchitel, S., Kramer, J., Magee, J.: Synthesis of behavioral models from scenarios. IEEE Trans Softw Eng 29(2), 99\u2013115 (2003)","journal-title":"IEEE Trans Softw Eng"},{"issue":"3","key":"157_CR45","doi-asserted-by":"crossref","first-page":"384","DOI":"10.1109\/TSE.2008.107","volume":"35","author":"S Uchitel","year":"2009","unstructured":"Uchitel, S., Brunet, G., Chechik, M.: Synthesis of partial behaviour model synthesis from properties and scenarios. IEEE Trans Softw Eng 35(3), 384\u2013406 (2009)","journal-title":"IEEE Trans Softw Eng"},{"key":"157_CR46","unstructured":"US Senate: The future of drones in America: law enforcement and privacy considerations, hearing before the Committee on the Judiciary. Tech. Rep. J-113-10, Washington, DC (2013)"},{"key":"157_CR47","doi-asserted-by":"crossref","unstructured":"Whittle, J., Schumann, J.: Generating statechart designs from scenarios. In: Proceedings of the 22nd International Conference on Software Engineering (ICSE), pp. 314\u2013323. Limerick, Ireland (2000)","DOI":"10.1145\/337180.337217"}],"container-title":["Automated Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-014-0157-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10515-014-0157-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-014-0157-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,17]],"date-time":"2019-08-17T11:25:12Z","timestamp":1566041112000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10515-014-0157-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,13]]},"references-count":47,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,6]]}},"alternative-id":["157"],"URL":"https:\/\/doi.org\/10.1007\/s10515-014-0157-z","relation":{},"ISSN":["0928-8910","1573-7535"],"issn-type":[{"value":"0928-8910","type":"print"},{"value":"1573-7535","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,11,13]]}}}