To support navigability, user documentation designers may use a table of contents, cross-References within procedures with page locations for related procedures, and in the case of PDF documentation, hyperlinks. Although standards and guidance exist for supporting navigable user documentation, problems appear across multiple industries including aviation and healthcare. To support user documentation development, we present a reachability analysis approach leveraging computational tree logic (CTL) reachability specifications as usability criteria coupled with a CTL model checker. A case study informed by an entry in an industry database highlights the effectiveness of the approach.
Get full access to this article
View all access options for this article.
References
1.
AbbateA. J.BassE. J.ThrockmortonA. L. (in press). Using formal task analytic models to support user manual development: An LVAD case study. In Proceedings of the International Symposium of Human Factors and Ergonomics in Health Care. Baltimore.
2.
AbowdG. D.WangH.MonkA. F. (1995). A formal technique for automated dialogue development. In Proceedings of the 1st Conference on Designing Interactive Systems (pp. 219–226). New York: ACM.
3.
AddisonM.ThimblebyH. (1994). Manuals as structured programs. In Proceedings of the Conference on People and Computers IX (pp. 67–79).
BackingerC.KingsleyP. (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.
6.
BoltonM. L.BassE. 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).
7.
BoltonM. L.BassE. J.SiminiceanuR. I. (2013). Using formal verification to evaluate human-automation interaction: A review. Systems, Man, and Cybernetics: Systems, IEEE Transactions on, 43(3), 488–503.
8.
BoltonM. L.JimenezN.van PaassenM.TrujilloM. (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.
9.
BoltonM. L.SiminiceanuR. I.BassE. 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.
10.
ClarkeE. M.EmersonE. A.SistlaA. 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.
11.
De MouraL.OwreS.ShankarN. (2003). The SAL language manual (Tech. Rep. No. CSL-01-01). Menlo Park: Computer Science Laboratory, SRI International.
12.
FAA. (2011). Aviation Safety Reporting System (Advisory Circular 00-46E). Washington, DC: U.S. Department of Transportation, Federal Aviation Administration.
13.
FAA. (2012). Airplane flight manual change 1 (Document AC 25.1581-1). Washington, DC: U.S. Department of Transportation, Federal Aviation Administration.
14.
FuhrmannP. A. (1972). On weak and strong reachability and controllability of infinite-dimensional linear systems. Journal of Optimization Theory and Applications, 9(2), 77–89.
15.
HolzmannG. (1991). Design and validation of communication protocols. Prentice Hall.
16.
IEEE. (2008). ISO/IEC 26514:2008: Systems and software engineering– Requirements for designers and developers of user documentation.
17.
ShankarN.SoreaM. (2003). Counterexample-driven model checking (Tech. Rep. No. SRI-CSL-03-04). Menlo Park: Computer Science Laboratory, SRI International.
18.
ThimblebyH.AddisonM. (1996). Hyperdoc: an interactive systems tool. In Proceedings of the HCI’95 Conference on People and Computers X (pp. 95-106).
