Improving the scalability of formal human–automation interaction verification analyses that use task-analytic models

详细信息    查看全文

• 作者：Matthew L. Bolton ; Xi Zheng ; Kylie Molinaro…
• 关键词：Model checking ; Task analytic models ; Formal methods ; Scalability
• 刊名：Innovations in Systems and Software Engineering
• 出版年：2017
• 出版时间：March 2017
• 年：2017
• 卷：13
• 期：1
• 页码：1-17
• 全文大小：
• 刊物类别：Computer Science
• 刊物主题：Software Engineering; Computing Methodologies; Computer Applications;
• 出版者：Springer London
• ISSN：1614-5054
• 卷排序：13

文摘

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.