Publications

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

Citation indices can be found here.

Edited Volumes

Wu, C., Rothrock, L., & Bolton, M. L. (2020). Special issue on computational human performance modeling. IEEE Transactions on Human-Machine Systems, 49(6), 470- 578.

Bolton, M. L., Degani, A., & Palanque, P., eds. (2012). Proceeding of the Workshop on Formal Methods in Human-Machine Interaction (Formal H). London: Imperial College.

Book Chapters

Bolton, M. L. & Bass, E. J. (2017). Enhanced Operator Function Model (EOFM): A Task Analytic Modeling Formalism for Including Human Behavior in the Verification of Complex Systems. In Weyers, B., Bowen, J., Dix, A., & Palanque, P. (Eds.), The Handbook of Formal Methods in Human-Computer Interaction (pp. 343-377). Gewerbestrasse: Springer International.

Bolton, M. L., & Bass, E. J. (2011). Comparing perceptual judgment and subjective measures of spatial awareness. In E. Salas & A. S. Dietz (Eds.), Situational Awareness: Critical Essays on Human Factors in Aviation (pp. 211-221). Surrey: Ashgate. Reprint of Bolton, M. L. & Bass, E. J. (2009). Comparing perceptual judgment and subjective measures of spatial awareness. Applied Ergonomics, 40, 597-607.

Bolton, M. L., Klein, K. A., & Göknur, S. C. (2006). Navigation. In Strunk, E. A. & Knight, J. C. (Eds.), Digital Avionics: A Computing Perspective (pp. 15-26). Los Alamitos: IEEE Computer Society.

Göknur, S. C., Klein, K. A., & Bolton, M. L. (2006). Flight management systems. In Strunk, E. A. & Knight, J. C. (Eds.), Digital Avionics: A Computing Perspective (pp. 53-61). Los Alamitos: IEEE Computer Society.

Klein, K. A., Göknur, S. C., & Bolton, M. L. (2006). Autopilot flight director systems. In Strunk, E. A. & Knight, J. C. (Eds.),Digital Avionics: A Computing Perspective (pp. 45-52). Los Alamitos: IEEE Computer Society.

Peer-reviewed Journal Articles

Bolton, M. L., Edworthy, J., & Boyd, A. D. (N.D.). A systematic formal analysis of masking between the reserved sounds of the IEC 60601-1-8 international medical alarm standard. Human Factors, 17 pages. doi: 10.1177/0018720820967596

Zheng, X., Bolton, M. L., & Daly, C. (2020). Extended SAFPH℞ (Systems Analysis for Formal Pharmaceutical Human Reliability): Two Approaches Based on Extended CREAM and a Comparative Analysis. Safety Science, 132, 18 pages. doi: 10.1016/j.ssci.2020.104944

Wei, J., Bolton, M. L., & Humphry, L. (N.D.). The level of measurement of trust in automation. Theoretical Issues in Ergonomic Science, 22 pages. doi: 10.1080/1463922X.2020.1766596

Bolton, M. L., Zheng, X., Li, M., Edworthy, J. R., & Boyd, A. D. (2020). An experimental validation of masking in IEC 60601-1-8:2006-compliant alarm sounds. In Press in Human Factors, 20 pages. doi: 10.1177/0018720819862911

Zheng, X., Bolton, M. L., Daly, C., & Biltekoff, E. (2020). The development of a next-generation human reliability analysis: Systems analysis for formal pharmaceutical human reliability (SAFPH℞). Reliability Engineering & System Safety, 202, 15 pages. doi: 10.1016/j.ress.2020.106927

Wang, X., Bisantz, A. M., Bolton, M. L., Cavuoto, L., & Chandola, V. (2020). Explaining supervised learning models: A preliminary study on binary classifiers. Ergonomics in Design, 28(3), 20-26.

Wu, C., Rothrock, L., & Bolton, M. L. (2019). Editorial special issue on computational human performance modeling. IEEE Transactions on Human-Machine Systems, 49(6), 470-473.

Bolton, M. L., Houser, A., & Molinaro, K. (2019). A formal method for assessing the impact of task-based erroneous human behavior on system safety. Reliability Engineering and System Safety, 188, 168-180.

Edworthy, J. R., McNeer, R. R., Bennett, C. L., Dudaryk, R., McDougall, S. J. P., Schlesinger, J. J., Bolton, M. L., Edworthy, J. D., Vieira, E. O., Boyd, A. D., Reid, S. K. J., Rayo, M. F., Wright, M. C., & Osborn, D. (ND). Getting alarm sounds into a global standard. Ergonomics in Design, 26(2), 4-13.

Bolton, M. L., Edworthy, J., Boyd, A. D., Wei, J., & Zheng, X. (2018). A computationally efficient formal method for discovering masking in concurrently sounding medical alarms. Accepted to Applied Acoustics, 141, 403-415.

Molinaro, K., & Bolton, M. L. (2018). Evaluating the applicability of the double system lens model to the analysis of phishing email judgments. Accepted to Computers and Security, 77, 128-137.

Houser, A., Ma, L. M., Feigh, K., & Bolton, M. L.C (2018). Using formal methods to reason about taskload and resource conflicts in simulated air traffic scenarios. Innovations in Systems and Software Engineering, 14(1), 1-14.

Pan, D., & Bolton, M. L.C (2018). Properties for formally assessing the performance level of human-human collaborative procedures with miscommunications and erroneous human behavior. International Journal of Industrial Ergonomics, 63, 75-88.

Yoon, J. M., He, D. & Bolton, M. L.C (2017). A LAMSTAR network-based human judgment analysis. IEEE Transactions of Human Machine Systems, 47(6), 951-957.

Li, M., Wei, J., Zheng, X. & Bolton, M. L.C (2017). A formal machine learning approach to generating human-machine interfaces from task models. IEEE Transactions of Human Machine Systems, 47(6), 822-833.

Wei, J. & Bolton, M. L.C (2017). Compression Rates and Spatial Judgment Biases Made from Synthetic Vision Perspective Displays. The Journal of Aerospace Information Science, 14(10), 523-532.

Bolton, M. L.C (2017). A task-based taxonomy of erroneous human behavior. International Journal of Human-Computer Studies, 108, 105-121.

Bolton, M. L.C, Zehng, X., Molinaro, K., Houser, A., & Li, M. (2017). Improving the scalability of formal human-automation interaction verification analyses that use task analytic models. Innovation in Systems and Software Engineering, 13(1), 1-17.

Hasanain, B., Boyd, A. D., & Bolton, M. L. (2017). A Formal Approach to Discovering Simultaneous Additive Masking Between Auditory Medical Alarms. Applied Ergonomics, 58, 500-514.

Hasanain, B., Boyd, A. D., & Bolton, M. L. (2016). Using model checking to detect simultaneous masking in medical alarms. IEEE Transactions on Human-Machine Systems, 46(2), 174 - 185.

Bolton, M. L. (2015). Model Checking Human-Human Communication Protocols Using Task Models and Miscommunication Generation. Journal of Aerospace Information Systems, 12, 476-489.

Bolton, M. L., Jimenez, N., van Paassen, M. M., & Trujillo, M. (2014). Automatically generating specification properties from task models for the formal verification of human-automation interaction. IEEE Transactions on Human-Machine Systems, 44(5), 561-575.

Bolton, M.L., Goknur, S., & Bass, E.J. (2014). Framework to support scenario development for human-centered alerting system evaluation. IEEE Transactions on Human-machine Systems, 43(6), 595-606.

Bolton, M. L. & Bass, E. J. (2013). Generating erroneous human behavior from strategic knowledge in task models and evaluating its impact on system safety with model checking. IEEE Transactions on Systems, Man and Cybernetics: Systems, 43(6), 1314-1327.

Bolton, M. L. (2013). Automatic validation and failure diagnosis of human-device interfaces using task analytic models and model checking. Computational and Mathematical Organization Theory,19(3), 288-312.

Bolton, M. L., Bass, E. J., & Siminiceanu, R. I. (2013). Using formal verification to evaluate human-automation interaction in safety critical systems, a review. IEEE Transactions on Systems, Man and Cybernetics: Systems, 43(3), 488-503.

Bolton, M. L., Bass, E. J., & Siminiceanu, R. I. (2012). Generating phenotypical erroneous human behavior to evaluatehuman–automation interaction using model checking. International Journal of Human-Computer Studies, 70(11), 888–906.

Bolton, M. L., & Bass, E. J (2012). Using model checking to explore checklist-guided pilot behavior. International Journal of Aviation Psychology. 22(4), 343–366.

Bolton, M. L., Siminiceanu, R. I., & Bass, E. J. (2011). A systematic approach to model checking human-automation interaction using task analytic models. IEEE Transactions on Systems, Man and Cybernetics, Part A: Systems and Humans, 41(5), 961-976.

Bolton, M. L., & Bass, E. J. (2010). Formally verifying human-automation interaction as part of a system model: Limitations and tradeoffs. Innovations in Systems and Software Engineering: A NASA Journal, 6(3), 219-231.

Bolton, M. L. & Bass, E. J. (2009). Comparing perceptual judgment and subjective measures of spatial awareness. Applied Ergonomics, 40, 597-607.

Bolton, M. L. & Bass, E. J. (2008). Using relative position and temporal judgments to identify biases in spatial awareness for synthetic vision systems. International Journal of Aviation Psychology, 18(2), 183-206.

Bolton, M. L., Bass, E. J., & Comstock, J. R. (2007). Spatial awareness in synthetic vision systems: Using spatial and temporal judgments to evaluate texture and field of view. Human Factors, 49, 961-974.

Peer-reviewed Conference Papers

Wang, X., Bisantz, A. M., Bolton, M. L., Cavuoto, L., & Chandola, V. (2020). Cognitive Work Analysis and Visualization Design for the Graduate Admission Decision Making Process. Proceedings of the 2020 International Annual Meeting of the Human Factors and Ergonomics Society (5 pages). Sage: Thousand Oaks.

Li, M. & Bolton, M. L. (2019). Task-based automated test case generation for human-machine interaction. Proceedings of the 2019 International Annual Meeting of the Human Factors and Ergonomics Society (pp. 807-811). Sage: Thousand Oaks.

Wei, J., Bolton, M. L., & Humphrey, L. (2019). Subjective measurement of trust: Is it on the level? Proceedings of the 2019 International Annual Meeting of the Human Factors and Ergonomics Society (pp. 212-216). Sage: Thousand Oaks.

Molinaro, K. & Bolton, M. L. (2019). Using the lens model and cognitive continuum theory to understand the effects of cognition on phishing victimization. Proceedings of the 2019 International Annual Meeting of the Human Factors and Ergonomics Society (pp. 173-177). Sage: Thousand Oaks.

Ma, L. M.C, Houser, A., Feigh, K., & Bolton, M. L.(2019). An analysis of air traffic management concepts of operation using simulation and formal verification. AIAA SciTech Forum (15 pages). Reston, AIAA.

Li, M., Behdad, Sara, & Bolton, M. L. (2018). A Formal methods approach to predicting how users will utilize system features. Proceedings of the 2018 International Annual Meeting of the Human Factors and Ergonomics Society (pp. 641-645). Santa Monica: HFES.

Bolton, M. L., Edwothy, J., & Boyd, A. D. (2018). A Formal Analysis of Masking Between Reserved Alarm Sounds of the IEC 60601-1-8 International Medical Alarm Standard. Proceedings of the 2018 International Annual Meeting of the Human Factors and Ergonomics Society (pp. 523-527). Santa Monica: HFES.

Zheng, X., Bolton, M. L.C, Daly, C., & Feng, L. (2017). A formal human reliability analysis of a community pharmacy dispensing procedure. Proceedings of the Human Factors and Ergonomics Society Annual Meeting (pp. 728-732). Santa Monica: HFES.

Bolton, M. L. (2017). Novel developments in formal methods for human factors engineering. Proceedings of the Human Factors and Ergonomics Society Annual Meeting (pp. 715-717). Santa Monica: HFES.

Houser, A. & Bolton, M. L. (2017). Formal Mental Models for Inclusive Privacy and Security. Proceedings of the Symposium on Usable Privacy and Security (SOUPS) (3 pages). Santa Clara: USENIX.

Tiferes, J.*, Bisantz, A. M., Bolton, M. L., Higginbotham, D. J., O’Hara, R. P., Wawrzyniak, N. K., Kozlowski, J. D., Ahmad, B., Hussein, A. A., & Guru, K. A. (2016). Multimodal team interactions in robot-assisted surgery. Proceedings of the 2016 International Annual Meeting of the Human Factors and Ergonomics Society (pp. 518-522). Santa Monica: Human Factors and Ergonomics Society.

Bolton, M. L.*, Hasanain, B., Boyd, A. D., & Edwothy, J. (2016). Using model checking to detect masking in IEC 60601-1-8-compliant alarm configurations. Proceedings of the 2016 International Annual Meeting of the Human Factors and Ergonomics Society (pp. 636-640). Santa Monica: Human Factors and Ergonomics Society.

Houser, A., Ma, L. M., Feigh, K., & Bolton, M. L. (2015). A formal approach to modeling and analyzing human taskload in simulated air traffic scenarios. In Proceedings of the IEEE International Conference on Complex Systems Engineering (6 pages). Piscataway: IEEE.

Li, M., Molinaro, K., & Bolton, M. L. (2015). Learning formal human-machine interface designs from task analytic models. In Proceedings of the HFES Annual Meeting (pp. 652-656). Santa Monica: HFES.

van Paassen, M. M., Bolton, M. L., Jimenez, N. (2014). Checking formal verification models for human-automation interaction. In Proceedings of the IEEE International Conference on Systems Man and Cybernetics. (pp. 3709-3714). Piscataway: IEEE.

Hasanain, B., Boyd, A.D., & Bolton, M. L. (2014). An approach to model checking the perceptual interactions of medical alarms. Proceedings of the 2014 International Annual Meeting of the Human Factors and Ergonomics Society (pp. 822-826). Santa Monica: Human Factors and Ergonomics Society.

Bolton, M. L., Ebrahimi, S. (2014). An approach to generating human-computer interfaces from task models. In Proceedings of AAAI 2014 Symposium on Modeling in Human-machine Systems: Challenges for Formal Verification (pp. 92-97). Palo Alto: AAAI.

Bass, E. J., Brantley, K., Perez, T., Bolton, M. L., Helms, A., Bartel, L. (2013). Information, data entry, and reporting requirements for a resident handoff of care support tool. In Proceedings of the IEEE International Conference on Systems Man and Cybernetics (pp. 675-680). Piscataway: IEEE.

Bolton, M. L., Jimenez, N., van Paassen, M. M., & Trujillo, M. (2013). Formally verifying human-automation interaction with specification properties generated from task analytic models. In Proceedings of the Sixth IAASS Conference. Montreal: IAASS.

Bolton, M. L., & Bass, E. J. (2013). Evaluating human-human communication protocols with miscommunication generation and model checking. In Proceedings of the Fifth NASA Formal Methods Symposium. Moffett Field: NASA Ames Research Center (pp. 48–62). Moffett Field: NASA Ames Research Center.

Bolton, M. L., Wallace, C. M., & Zuck, L. D. (2012). On policies and intents. In Proceedings of the Eighth International Conference on Information Systems Security (pp. 104–118). Berlin: Springer.

Bass, E. J., Bolton, M. L., 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 (pp. 1817-1824). Piscataway: IEEE.

Bolton, M. L. & Bass, E. J. (2011). Using task analytic behavior models, strategic knowledge-based erroneous human behavior generation, and model checking to evaluate human-automation interaction. In Proceedings of the IEEE International Conference on Systems Man and Cybernetics (pp. 1788-1794). Piscataway: IEEE.
    Winner of the Franklin V. Taylor Memorial Award for the Best Conference Paper (out of 612 accepted papers).

Bolton, M. L. (2011). Validating human-device interfaces with model checking and temporal logic properties automatically generated from task analytic models. In Proceedings of the 20th Behavior Representation in Modeling and Simulation Conference (pp. 130-137). Sundance: The BRIMS Society.
    Winner of a best paper award (out of 24 accepted papers).

Bolton, M. L., & Bass, E. J. (2010). Using task analytic models and phenotypes of erroneous human behavior to discover system failures using model checking. In Proceedings of the 54th Annual Meeting of the Human Factors and Ergonomics Society (pp. 992-996). Santa Monica: Human Factors and Ergonomics Society.

Bolton, M. L., & Bass, E. J. (2010). Using task analytic models to visualize model checker counterexamples. In Proceedings of the IEEE International Conference on Systems Man and Cybernetics (pp. 2069-2074). Piscataway: IEEE.

Bolton, M. L., & Bass, E. J. (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 (pp. 764-768). Santa Monica: Human Factors and Ergonomics Society.

Bolton, M. L., & Bass, E. J. (2009). Enhanced operator function model: A generic human task behavior modeling language. In Proceedings of the IEEE International Conference on Systems Man and Cybernetics (pp. 2983-2990). Piscataway: IEEE.

Bolton, M. L., & Bass, E. J. (2009). Building a formal model of a human-interactive system: Insights into the integration of formal methods and human factors engineering. In Proceedings of the First NASA Formal Methods Symposium (pp. 6-15). Moffett Field: NASA Ames Research Center.
    One of the 7 best papers (out of 22 accepted papers) invited to submit an extended manuscript as a journal article.

Bolton, M. L. (2008). Modeling human perception: Could Stevens' power law be an emergent feature? In Proceedings of IEEE the International Conference on Systems Man and Cybernetics (pp. 1073-1078). Piscataway: IEEE.

Bolton, M. L. & Bass, E. J. (2007). Spatial awareness: Comparing judgment-based and subjective measures. In Proceedings of IEEE the International Conference on Systems Man and Cybernetics (pp. 2582-2587). Piscataway: IEEE.

Bolton, M. L., Bass, E. J., & Comstock, J. R. (2006). Using relative position and temporal judgments to assess the effects of texture and field of view on spatial awareness in synthetic vision systems displays. In Proceedings of the 50th Annual Meeting of the Human Factors and Ergonomics Society (pp. 961-974). Santa Monica: Human Factors and Ergonomics Society.

Bolton, M. L., Bass, E. J., & Comstock, J. R. (2006). Using videos derived from simulations to support the analysis of spatial awareness in synthetic vision displays. In Proceedings of the IEEE International Conference on Systems Man and Cybernetics (pp. 2582-2587). Piscataway: IEEE.

Bolton, M. L. & Bass, E. J. (2005). Cognitive Systems Engineering Educational Software (CSEES): Educational software addressing quantitative models of performance. In Proceedings of the IEEE International Conference on Systems Man and Cybernetics (pp. 3380-3386). Piscataway: IEEE.

Göknur, S., Bolton, M. L., & Bass, E. J. (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 on Systems Man and Cybernetics (pp. 886-892). Piscataway: IEEE.

Other Conference Papers

Pan, D., Bolton, M. L. (2015). A Formal Method for Evaluating the Performance Level of Human-Human Collaborative Procedures. In Proceedings of HCI International 2015 (pp. 186-197). Berlin: Springer.

Bolton, M. L., Bass, E. J., Siminiceanu, R. I. (2008). Using formal methods to predict human error and system failures. In Proceedings of the Second International Conference on Applied Human Factors and Ergonomics (CD-ROM). Las Vegas: Applied Human Factors and Ergonomics International.

Bolton, M. L. & Bass, E. J. (2007). Spatial awareness biases in synthetic vision systems displays. In Proceedings of the 14th International Symposium on Aviation Psychology (pp. 63-69). Dayton: Association for Aviation Psychology.

Bolton, M. L., Bass, E. J., & Comstock, J. R. (2006). A toolset to support the development of spatial and temporal judgment experiments for synthetic vision systems. In Proceedings of the IEEE Systems and Information Engineering Design Symposium (pp. 55-60). Piscataway: IEEE.

Bolton, M. L., Hagan, T., Kustu, D., LaChance, L., Li, S., & Bass, E. J. (2006). Assessment and enhancement of synthetic vision systems experimentation software. In Proceedings of the IEEE Systems and Information Engineering Design Symposium (pp. 61-66). Piscataway: IEEE.
    Winner of the best paper award for the Human Computer Interface track.

Peer-reviewed Abstracts

Bolton, M. L. (2021). Task Models: A Possible Tool for Formally Modeling and Proving Properties about Artificial Intelligence and Machine Learning in Systems Engineering. To appear in the

Proceedings of the 2021 AAAI Spring Symposium Series: Leveraging Systems Engineering to Realize Synergistic AI/Machine Learning Capabilities.

AAAI: Stanford.

Bolton, M. L., Darget, T., Biltekoff, E., Edworthy, J., Boyd, A. (2020). Medical Alarm Audibility System Checker (MAASC): A computational tool for checking medical alarm configurations for simultaneous masking (pp. 302-303). Proceedings of the International Symposium on Human Factors and Ergonomics in Health Care. Sage: Thousand Oaks.

Molinaro, K. & Bolton, M. L. (2019). Applying the lens model and cognitive continuum theory to the analysis of phishing email judgments (pp. 21-23). The Brunswick Society Newsletter, 34. Albany: The Brunswick Society.

Molinaro, K. & Bolton, M. L. (2018). Applying the lens model and cognitive continuum theory to the analysis of phishing email judgments (pp. 22-25). The Brunswick Society Newsletter, 33. Albany: The Brunswick Society.

Wang, X., Bisantz, A., Bolton, M. L., Cavuoto, L., Chandola, V. (2018). Towards Better Interpretability of Machine Learning-based Decision Support Systems (1 page). Proceedings of the AHFE 2018 International Conference on Human Factors and Systems Interaction. Berlin: Springer.

Bolton, M. L. (2015). Formal methods for human-systems engineering. In Proceedings of the Industrial & Systems Engineering Research Conference (1 page). Norcross: Institute of Industrial Engineers.

Bass, E. J., Bolton, M. L., Feigh, K. M., Gunter, E. L., & Rushby, J. (2012). Toward an integrated model checking, theorem proving and simulation framework for analyzing authority and autonomy. In Proceeding of the Workshop on Formal Methods in Human-Machine Interaction (Formal H) (CD-ROM). London: England.

Bolton, M. L. & Bass, E. J. (2012). Model checking human-automation interaction with enhanced operator function model. In Proceeding of the Workshop on Formal Methods in Human-Machine Interaction (Formal H) (CD-ROM). London: England.

Bolton, M. L., & Bass, E. J. (2008). Formal modeling of erroneous human behavior and its implications for model checking. In Proceedings of the Sixth NASA Langley Formal Methods Workshop (pp. 62-64). Hampton: NASA Langley Research Center.

Dissertations and Theses

Hall, C. (2020). Simultaneous Masking Between Audio Alarms in Terminal Air Traffic Control for Raytheon’s Standard Terminal Automation Replacement System. MS Thesis, University at Buffalo, State University of New York, Buffalo.

Jhonson, J. (2020). The UX of voice assistants for people with disability. MS Thesis, University at Buffalo, State University of New York, Buffalo.

Wang, X. (2020). Towards Better Interpretability of Machine Learning-based Decision Support Systems Doctoral dissertation, University at Buffalo, State University of New York, Buffalo.

Robin, W. (2019). The Level of Measurement of Human-Automation Trust: Is It on the Level? Doctoral dissertation, University at Buffalo, State University of New York, Buffalo.

Molinaro, K. (2019). Understanding the Phish: Using Judgment Analysis to Evaluate the Human Judgment of Phishing Emails. Doctoral dissertation, University at Buffalo, State University of New York, Buffalo.

Singleton, S. N. (2018). An Analysis of Simultaneous Masking Between Reserved Alarm Sounds of the International Standard. MS Thesis, University at Buffalo, State University of New York, Buffalo.

Houser,A. (2018). Mental Models for Cybersecurity: A Formal Methods Approach. Doctoral dissertation, University at Buffalo, State University of New York, Buffalo.

Li, M. (2018). Formal Methods for User Experience Evaluation and Testing. Doctoral dissertation, University at Buffalo, State University of New York, Buffalo.

Hasanain, B. (2016). A Formal Approach for Detecting Masking in Medical Alarms. Doctoral dissertation, University of Illinois Chicago, Chicago.

Bolton, M. L. (2010). Using Task Analytic Behavior Modeling, Erroneous Human Behavior Generation, and Formal Methods to Evaluate the Role of Human-automation Interaction in System Failure. Doctoral dissertation, University of Virginia, Charlottesville, Virginia.