Improving the scalability of formal human–automation interaction verification analyses that use task-analytic models. (March 2017)

• Record Type: Journal Article
• Authors: Bolton, Matthew; Zheng, Xi; Molinaro, Kylie; Houser, Adam; Li, Meng
• Is Part Of: Innovations in systems and software engineering. Volume 13:Number 1(2017)
• Page Start: 1
• Page End: 17
• Publication Date: 2017-03
• Subjects: Model checking -- Task analytic models -- Formal methods -- Scalability; Software engineering -- Periodicals; Systems engineering -- Periodicals; Génie logiciel -- Périodiques; Ingénierie des systèmes -- Périodiques; Electronic journals; 005.1
• DOI: 10.1007/s11334-016-0272-z
• Languages: English
• ISSNs: 1614-5046

Abstract

Abstract The enhanced operator function model with communications (EOFMCs) is a task-analytic modeling formalism used for including human behavior in formal models of larger systems. This allows the contribution of human behavior to the safety of the system to be evaluated with model checking. The previous method for translating the EOFMCs into model checker input language was conceptually straightforward, but extremely statespace inefficient. This limited the applications that could be formally verified using EOFMC. In this paper, we present an alternative approach for formally representing EOFMCs that substantially decreases the model's statespace size and verification time. This paper motivates this effort, describes how the improvement was achieved, presents benchmarks demonstrating the improvements in statespace size and verification time, discusses the implications of these results, and outlines directions for future improvement.