Using Formal Task Analytic Models to Support User Manual Development: An LVAD Case Study

Abstract

Thousands of medical devices are employed to diagnose and treat human health problems each day. These devices can be complicated to use, maintain, and troubleshoot when alarm conditions occur. Patients often turn to the provided instructions for use (IFUs) for step-by-step guidance in alarm mitigation. Despite standards and guidance provided by standardization organizations and regulatory agencies to support user manual usability, inadequate IFUs may be contributing to adverse events. To address potential limitations of currently employed user manual design methods, we present a model-based approach to support user manual development. Our approach leverages formal task modeling, finite state automata, linear temporal logic (LTL) and symbolic model checking, all of which contribute individually and additively to our analysis. We demonstrate the value of our approach using a case study of a left ventricular assist device (LVAD) and a set of troubleshooting instructions from its patient handbook.

Get full access to this article

View all access options for this article.

References

Backinger

, & Kingsley

(1993). Write it right: Recommendations for developing user instruction manuals for medical devices used in home health care (HHS Publication FDA 93-4258). Washington, DC: Food and Drug Administration. Center for Devices and Radiological Health.

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 1st NASA Formal Methods Symposium (pp. 6–15). Moffett Field: NASA Ames Research Center.

Bolton

M. L.

, & Bass

E. J.

(2010). Using task analytic models to visualize model checker counterexamples. In Systems Man and Cybernetics (SMC), 2010 IEEE International Conference on (pp. 2069–2074).

Bolton

M. L.

, Bass

E. J.

, & Siminiceanu

R. I.

(2013). Using formal verification to evaluate human-automation interaction: A review. Systems, Man, and Cybernetics: Systems, IEEE Transactions on, 43(3), 488–503.

Bolton

M. L.

, Jimenez

, van Paassen

, & 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. Systems, Man and Cybernetics, Part A: Systems and Humans, IEEE Transactions on, 41(5), 961–976.

Clarke

E. M.

, Emerson

E. A.

, & Sistla

A. P.

(1986). Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems (TOPLAS), 8(2), 244–263.

De Moura

, Owre

, & Shankar

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

Emerson

E. A.

(1990). Temporal and modal logic. In van Leeuwen

, Meyer

A. R.

, Nivat

, Paterson

, & Perrin

(Eds.), Handbook of Theoretical Computer Science (pp. 995-1072). Cambridge: MIT Press.

10.

IEEE. (2008). ISO/IEC 26514:2008: Systems and software engineering- Requirements for designers and developers of user documentation.

11.

IEEE. (2010). ISO/IEC 60601-1-6:2010: Medical electrical equipment -Parts 1-6: General requirements for basic safety and essential performance - Collateral standard: Usability.

12.

Shankar

(2000). Symbolic analysis of transition systems. In Proceedings of the International Workshop on Abstract State Machines, Theory and Applications (pp. 287–302). London: Springer.

13.

U.S. Food and Drug Administration. (2011). Draft Guidance for Industry and Food and Drug Administration Staff - Applying Human Factors and Usability Engineering to Optimize Medical Device Design (HHS Publication FDA 1757). Center for Devices and Radiological Health.