-
Proc Hum Factors Ergon Soc Annu Meet · Nov 2009
A Method for the Formal Verification of Human-interactive Systems.
- Matthew L Bolton and Ellen J Bass.
- University of Virginia, Systems and Information Engineering, Charlottesville, Virginia.
- Proc Hum Factors Ergon Soc Annu Meet. 2009 Nov 12; 52 (12): 764-768.
AbstractPredicting failures in complex, human-interactive systems is difficult as they may occur under rare operational conditions and may be influenced by many factors including the system mission, the human operator's behavior, device automation, human-device interfaces, and the operational environment. This paper presents a method that integrates task analytic models of human behavior with formal models and model checking in order to formally verify properties of human-interactive systems. This method is illustrated with a case study: the programming of a patient controlled analgesia pump. Two specifications, one of which produces a counterexample, illustrate the analysis and visualization capabilities of the method.
Notes
Knowledge, pearl, summary or comment to share?You can also include formatting, links, images and footnotes in your notes
- Simple formatting can be added to notes, such as
*italics*,_underline_or**bold**. - Superscript can be denoted by
<sup>text</sup>and subscript<sub>text</sub>. - Numbered or bulleted lists can be created using either numbered lines
1. 2. 3., hyphens-or asterisks*. - Links can be included with:
[my link to pubmed](http://pubmed.com) - Images can be included with:
 - For footnotes use
[^1](This is a footnote.)inline. - Or use an inline reference
[^1]to refer to a longer footnote elseweher in the document[^1]: This is a long footnote..