Sage Journals: Discover world-class research

Abstract

User-centered design (UCD) is an approach for creating human-machine interfaces so that they support human operator tasks. UCD can be challenging because designers can fail to account for human-machine interactions that occur due to the inherent concurrence between the human and the other elements of the system. Formal methods are tools that enable analysts to consider all of the possible system interactions using a combination of formal modeling, specification, and proof-based verification. However, the creation of formal models of interface designs can be extremely difficult. This work describes a method that supports UCD by automatically generating formal designs of human-machine interface behavior from task analytic models, where the resulting interface will always support the behavior captured in the task model. This paper describes the method and demonstrates its capabilities with a vending machine application. Results and future research directions are discussed.

Get full access to this article

View all access options for this article.

References

Angluin

(1987). Learning regular sets from queries and counterexamples. Information and computation, 75(2), 87–106.

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, 488–503.

Bolton

M. L.

Ebrahimi

(2014). An approach to generating human- computer interfaces from task models. In 2014 aaai spring symposium series (pp. 92–97). Palo Alto: AAAI.

Bolton

M. L.

Jimenez

van Paassen

M. M.

Trujillo

(2014). Automatically generating specification properties from task models for the formal verification of human-automation interaction. Human-Machine Systems, IEEE Transactions on, 44(5), 561–575.

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, 41(5), 961–976.

Clarke

E. M.

Grumberg

Peled

D. A.

(1999). Model checking. Cambridge: MIT Press.

Combéfis

Giannakopoulou

Pecheur

Feary

(2011). Learning system abstractions for human operators. In Proceedings of the 2011 International Workshop on Machine Learning Technologies in Software Engineering (pp. 3–10). New York: ACM.

Degani

Heymann

(2002). Formal verification of human-automation interaction. Human Factors, 44(1), 28–43.

De Moura

Owre

Shankar

(2003). The SAL language manual (Tech. Rep. No. CSL-01-01). Menlo Park: Computer Science Laboratory, SRI International.

10.

DIS

ISO

. (2009). 9241-210: 2010. Ergonomics of human system interaction-part 210: Human-centred design for interactive systems. International Organization for Standardization (ISO), Switzerland.

11.

García

J. G.

Lemaigre

González-Calleros

J. M.

Vanderdonckt

(2008). Model-driven approach to design user interfaces for workflow information systems. Journal of Universal Computer Science, 14(19), 3160–3173.

12.

Heitmeyer

(1998). On the need for practical formal methods. In Proceedings of the 5th International Symposium on Formal Techniques in Real-Time Fault-Tolerant Systems (pp. 18–26). London: Springer.

13.

Kirwan

Ainsworth

L. K.

(1992). A guide to task analysis. London: Taylor and Francis.

14.

Mealy

G. H.

(1955). A method for synthesizing sequential circuits. Bell System Technical Journal, 34(5), 1045–1079.

15.

Moore

E. F.

(1956). Gedanken-experiments on sequential machines. Automata studies, 34, 129–153.

16.

Parnas

D. L.

(1969). On the use of transition diagrams in the design of a user interface for an interactive computer system. In Proceedings of the 24th National ACM Conference (pp. 379–385). New York: ACM.

17.

Raffelt

Steffen

Berg

(2005). Learnlib: A library for automata learning and experimentation. In Proceedings of the 10th international workshop on formal methods for industrial critical systems (pp. 62–71).

18.

Rushby

(2012). The versatile synchronous observer. In Gheyi

Nau-mann

(Eds.), Formal methods: Foundations and applications (Vol. 7498). Springer Berlin Heidelberg.

19.

Tran

Kolp

Vanderdonckt

Wautelet

Faulkner

(2010).

20.

Agent-based user interface generation from combined task, context and domain models. In Proceedings of the 8th international workshop on task models and diagrams for user interface design (pp. 146–161). Berlin: Springer.

Learning Formal Human-machine Interface Designs From Task Analytic Models

Abstract

Get full access to this article

References