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

被引：6

作者：

Bolton M.L. ^{[1
]}

Zheng X. ^{[1
]}

Molinaro K. ^{[1
]}

Houser A. ^{[1
]}

Li M. ^{[1
]}

机构：

[1] Department of Industrial and Systems Engineering, State University of New York at Buffalo, Amherst, 14260, NY

来源：

Innovations in Systems and Software Engineering | 2017年 / 13卷 / 01期

基金：

美国国家航空航天局; 美国国家科学基金会;

关键词：

Formal methods; Model checking; Scalability; Task analytic models;

D O I：

10.1007/s11334-016-0272-z

中图分类号：

学科分类号：

摘要：

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. © 2016, Springer-Verlag London.

引用

页码：1 / 17

页数：16

共 45 条

[1]

Ait-Ameur Y., Baron M., Formal and experimental validation approaches in HCI systems design based on a shared event B model, Int J Softw Tools Technol Transfer, 8, 6, pp. 547-563, (2006)

[2]

Ait-Ameur Y., Baron M., Girard P., Formal validation of HCI user tasks. In: Proceedings of the international conference on software engineering research and practice, pp. 732-738, (2003)

[3]

Angluin D., Learning regular sets from queries and counterexamples, Inf Comput, 75, 2, pp. 87-106, (1987)

[4]

Basnyat S., Palanque P., Schupp B., Wright P., Formal socio-technical barrier modelling for safety-critical interactive systems design, Saf Sci, 45, 5, pp. 545-565, (2007)

[5]

Basnyat S., Palanque P.A., Bernhaupt R., Poupart E., 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, (2008)

[6]

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, Proceedings of the IEEE international conference on systems, man, and cybernetics, pp. 1817-1824

[7]

Bolton M.L., 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, (2010)

[8]

Bolton M.L., Automatic validation and failure diagnosis of human-device interfaces using task analytic models and model checking, Comput Math Organ Theory, 19, pp. 288-312, (2013)

[9]

Bolton M.L., Model checking human–human communication protocols using task models and miscommunication generation. J Aerosp Inf Syst, doi:10.2514/1.I010276, (2015)

[10]

Bolton M.L., Bass EJ (2009a) Building a formal model of a human-interactive system: insights into the integration of formal methods and human factors engineering, Proceedings of the 1st NASA formal methods symposium, pp. 6-15

← 1 2 3 4 5 →