Automated framework for formal operator task analysis

Ayesha Yasmeen, Elsa L. Gunter

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Aberrant behavior of human operators in safety critical systems can lead to severe or even fatal consequences. Human operators are unique in their decision making capability, judgment and nondeterminism. There is a need for a generalized framework that can allow capturing, modeling and analyzing the interactions between computer systems and human operators where the operators are allowed to deviate from their prescribed behaviors for executing a task. This will provide a formal understanding of the robustness of a computer system against possible aberrant behaviors by its human operators. We provide a framework for (i) modeling the human operators and the computer systems; (ii) formulating tolerable human operator action variations(protection envelope); (iii) determining whether the computer system can maintain its guarantees if the human operators operate within their protection envelopes; and finally, (iv) determining robustness of the computer system under weakening of the protection envelopes. We present Tutela, a tool that assists in accomplishing the first and second step, automates the third step and modestly assists in accomplishing the fourth step.

Original languageEnglish (US)
Title of host publication2011 International Symposium on Software Testing and Analysis, ISSTA 2011 - Proceedings
Pages78-88
Number of pages11
DOIs
StatePublished - 2011
Event20th International Symposium on Software Testing and Analysis, ISSTA 2011 - Toronto, ON, Canada
Duration: Jul 17 2011Jul 21 2011

Publication series

Name2011 International Symposium on Software Testing and Analysis, ISSTA 2011 - Proceedings

Other

Other20th International Symposium on Software Testing and Analysis, ISSTA 2011
CountryCanada
CityToronto, ON
Period7/17/117/21/11

Keywords

  • human operator
  • model generation
  • property satisfaction
  • protected task execution
  • system robustness
  • task analysis
  • verification framework

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Automated framework for formal operator task analysis'. Together they form a unique fingerprint.

Cite this