Skip to main content
Erschienen in: Automated Software Engineering 2/2015

01.06.2015

Building high assurance human-centric decision systems

verfasst von: Constance L. Heitmeyer, Marc Pickett, Elizabeth I. Leonard, Myla M. Archer, Indrakshi Ray, David W. Aha, J. Gregory Trafton

Erschienen in: Automated Software Engineering | Ausgabe 2/2015

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

Many future decision support systems will be human-centric, i.e., require substantial human oversight and control. Because these systems often provide critical services, high assurance is needed that they satisfy their requirements. This paper, the product of an interdisciplinary research team of experts in formal methods, adaptive agents, and cognitive science, addresses this problem by proposing a new process for developing high assurance human-centric decision systems. This process uses AI (artificial intelligence) methods—i.e., a cognitive model to predict human behavior and an adaptive agent to assist the human—to improve system performance, and software engineering methods—i.e., formal modeling and analysis—to obtain high assurance that the system behaves as intended. The paper describes a new method for synthesizing a formal system model from Event Sequence Charts, a variant of Message Sequence Charts, and a Mode Diagram, a specification of system modes and mode transitions. It also presents results of a new pilot study investigating the optimal level of agent assistance for different users in which the agent design was evaluated using synthesized user models. Finally, it reviews a cognitive model for predicting human overload in complex human-centric systems. To illustrate the development process and our new techniques, we describe a human-centric decision system for controlling unmanned vehicles.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Fußnoten
1
An example of a predicate that may be impossible to capture in a formula is the reachability predicate where there are infinitely many possible scenario states.
 
2
These preconditions ensure that \({\mathcal W}\) is a well-formed Moded Scenarios Description.
 
3
We treat multiple robots as a generalization of multiple UAVs.
 
Literatur
Zurück zum Zitat Alspaugh, T.A., Faulk, S.R., Britton, K.H., Parker, R.A., Parnas, D.L., Shore, J.E.: Software requirements for the A-7E aircraft. Tech. Rep. NRL-9194, Naval Research Laboratory, Washington, DC (1992) Alspaugh, T.A., Faulk, S.R., Britton, K.H., Parker, R.A., Parnas, D.L., Shore, J.E.: Software requirements for the A-7E aircraft. Tech. Rep. NRL-9194, Naval Research Laboratory, Washington, DC (1992)
Zurück zum Zitat Alur, R., Yannakakis, M.: Model checking of Message Sequence Charts. Proceedings of the 10th International Conference on Concurrency Theory (CONCUR), pp. 114–129. Eindhoven, The Netherlands (1999) Alur, R., Yannakakis, M.: Model checking of Message Sequence Charts. Proceedings of the 10th International Conference on Concurrency Theory (CONCUR), pp. 114–129. Eindhoven, The Netherlands (1999)
Zurück zum Zitat Archer, M.: TAME: Using PVS strategies for special-purpose theorem proving. Ann Math Artif Intell 29(1–4), 131–189 (2001)MathSciNet Archer, M.: TAME: Using PVS strategies for special-purpose theorem proving. Ann Math Artif Intell 29(1–4), 131–189 (2001)MathSciNet
Zurück zum Zitat Bharadwaj, R., Heitmeyer, C.: Developing high assurance avionics systems with the SCR requirements method. In: Proceedings of the 19th Digital Avionics Systems Conference (DASC), Philadelphia, Pennsylvania (2000) Bharadwaj, R., Heitmeyer, C.: Developing high assurance avionics systems with the SCR requirements method. In: Proceedings of the 19th Digital Avionics Systems Conference (DASC), Philadelphia, Pennsylvania (2000)
Zurück zum Zitat Boussemart, Y., Cummings, M.: Behavioral recognition and prediction of an operator supervising multiple heterogeneous unmanned vehicles. In: Proceedings of the 1st International Conference on Humans Operating Unmanned Systems (HUMOUS), Brest, France (2008) Boussemart, Y., Cummings, M.: Behavioral recognition and prediction of an operator supervising multiple heterogeneous unmanned vehicles. In: Proceedings of the 1st International Conference on Humans Operating Unmanned Systems (HUMOUS), Brest, France (2008)
Zurück zum Zitat Breslow, L.A., Gartenberg, D., McCurry, J.M., Trafton, J.G.: Dynamic operator overload: A model for predicting workload during supervisory control. IEEE Trans Hum Mach Syst 44(1), 30–40 (2014)CrossRef Breslow, L.A., Gartenberg, D., McCurry, J.M., Trafton, J.G.: Dynamic operator overload: A model for predicting workload during supervisory control. IEEE Trans Hum Mach Syst 44(1), 30–40 (2014)CrossRef
Zurück zum Zitat Bumiller, E., Shanker, T.: War evolves with drones, some tiny as bugs. New York Times, (2011) Bumiller, E., Shanker, T.: War evolves with drones, some tiny as bugs. New York Times, (2011)
Zurück zum Zitat Crandall, J.W., Goodrich, M.A., D R Olsen, J., Nielsen, C.W.: Validating human-robot systems in multi-tasking environments. IEEE Transactions on Systems, Man, and Cybernetics 35(4), 438–449 (2005) Crandall, J.W., Goodrich, M.A., D R Olsen, J., Nielsen, C.W.: Validating human-robot systems in multi-tasking environments. IEEE Transactions on Systems, Man, and Cybernetics 35(4), 438–449 (2005)
Zurück zum Zitat Cummings, M.L., Mitchell, P.J.: Predicting controller capacity in supervisory control of multiple UAVs. IEEE Trans Syst Man Cybern 38(2), 451–460 (2008)CrossRef Cummings, M.L., Mitchell, P.J.: Predicting controller capacity in supervisory control of multiple UAVs. IEEE Trans Syst Man Cybern 38(2), 451–460 (2008)CrossRef
Zurück zum Zitat Damas, C., Lambeau, B., Dupont, P., van Lamsweerde, A.: Generating annotated behavior models from end-user scenarios. IEEE Trans Softw Eng 31(12), 1056–1073 (2005)CrossRef Damas, C., Lambeau, B., Dupont, P., van Lamsweerde, A.: Generating annotated behavior models from end-user scenarios. IEEE Trans Softw Eng 31(12), 1056–1073 (2005)CrossRef
Zurück zum Zitat Damas, C., Lambeau, B., Roucoux, F., van Lamsweerde, A.: Analyzing critical process models through behavior model synthesis. In: Proceedings of the 31st International Conference on Software Engineering (ICSE), pp. 241–251. Vancouver, Canada (2009) Damas, C., Lambeau, B., Roucoux, F., van Lamsweerde, A.: Analyzing critical process models through behavior model synthesis. In: Proceedings of the 31st International Conference on Software Engineering (ICSE), pp. 241–251. Vancouver, Canada (2009)
Zurück zum Zitat DSB: The role of autonomy in DoD systems. Tech. rep., Defense Science Board, Office of the Under Secretary of Defense for Acquisition, Technology and Logistics, Washington, DC (2012) DSB: The role of autonomy in DoD systems. Tech. rep., Defense Science Board, Office of the Under Secretary of Defense for Acquisition, Technology and Logistics, Washington, DC (2012)
Zurück zum Zitat Gargantini, A., Heitmeyer, C.: Using model checking to generate tests from requirements specifications. In: Proceedings of the 7th European Software Engineering Conference and 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), pp. 146–162. Toulouse, France (1999) Gargantini, A., Heitmeyer, C.: Using model checking to generate tests from requirements specifications. In: Proceedings of the 7th European Software Engineering Conference and 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), pp. 146–162. Toulouse, France (1999)
Zurück zum Zitat Gartenberg, D., Breslow, L., Park, J., McCurry, J., Trafton, J.: Adaptive automation and cue invocation: The effect of cue timing on operator error. In: Proceedings of the ACM SIGCHI Conference on Human Factors in Computing Systems (CHI), pp. 3121–3130. France, Paris (2013) Gartenberg, D., Breslow, L., Park, J., McCurry, J., Trafton, J.: Adaptive automation and cue invocation: The effect of cue timing on operator error. In: Proceedings of the ACM SIGCHI Conference on Human Factors in Computing Systems (CHI), pp. 3121–3130. France, Paris (2013)
Zurück zum Zitat Giannakopoulou, D., Magee, J.: Fluent model checking for event-based systems. ACM SIGSOFT Softw Eng Notes 28, 257–266 (2003)CrossRef Giannakopoulou, D., Magee, J.: Fluent model checking for event-based systems. ACM SIGSOFT Softw Eng Notes 28, 257–266 (2003)CrossRef
Zurück zum Zitat Gray, W.D., Boehm-Davis, D.A.: Milliseconds matter: An introduction to microstrategies and to their use in describing and predicting interactive behavior. J Exp Psychol 6(4), 322 (2000) Gray, W.D., Boehm-Davis, D.A.: Milliseconds matter: An introduction to microstrategies and to their use in describing and predicting interactive behavior. J Exp Psychol 6(4), 322 (2000)
Zurück zum Zitat Hanke, M., Halchenko, Y.O., Sederberg, P.B., Olivetti, E., Fründ, I., Rieger, J.W., Herrmann, C.S., Haxby, J.V., Hanson, S.J., Pollmann, S.: PyMVPA: a Python toolbox for multivariate pattern analysis of fMRI data. Neuroinformatics 7(1), 37–53 (2009)CrossRef Hanke, M., Halchenko, Y.O., Sederberg, P.B., Olivetti, E., Fründ, I., Rieger, J.W., Herrmann, C.S., Haxby, J.V., Hanson, S.J., Pollmann, S.: PyMVPA: a Python toolbox for multivariate pattern analysis of fMRI data. Neuroinformatics 7(1), 37–53 (2009)CrossRef
Zurück zum Zitat Heitmeyer, C., Jeffords, R.: Applying a formal requirements method to three NASA systems: Lessons learned. In: Proceedings of the IEEE Aerospace Conference, Big Sky, Montana, p 84 (2007) Heitmeyer, C., Jeffords, R.: Applying a formal requirements method to three NASA systems: Lessons learned. In: Proceedings of the IEEE Aerospace Conference, Big Sky, Montana, p 84 (2007)
Zurück zum Zitat Heitmeyer, C., Kirby, J., Labaw, B., Archer, M., Bharadwaj, R.: Using abstraction and model checking to detect safety violations in requirements specifications. IEEE Trans Softw Eng 24(11), 927–948 (1998)CrossRef Heitmeyer, C., Kirby, J., Labaw, B., Archer, M., Bharadwaj, R.: Using abstraction and model checking to detect safety violations in requirements specifications. IEEE Trans Softw Eng 24(11), 927–948 (1998)CrossRef
Zurück zum Zitat Heitmeyer, C., Archer, M., Bharadwaj, R., Jeffords, R.: Tools for constructing requirements specifications: The SCR toolset at the age of ten. Comput Syst Sci Eng 20(1), 19–35 (2005) Heitmeyer, C., Archer, M., Bharadwaj, R., Jeffords, R.: Tools for constructing requirements specifications: The SCR toolset at the age of ten. Comput Syst Sci Eng 20(1), 19–35 (2005)
Zurück zum Zitat Heitmeyer, C., Pickett, M., Breslow, L., Aha, D., Trafton, J.G., Leonard, E.: High assurance human-centric decision systems. In: Proc of the 2nd International NSF-Sponsored Workshop on Realizing Artificial Intelligence Synergies in Software Engineering (RAISE) (2013a) Heitmeyer, C., Pickett, M., Breslow, L., Aha, D., Trafton, J.G., Leonard, E.: High assurance human-centric decision systems. In: Proc of the 2nd International NSF-Sponsored Workshop on Realizing Artificial Intelligence Synergies in Software Engineering (RAISE) (2013a)
Zurück zum Zitat Heitmeyer, C.L., Jeffords, R.D., Labaw, B.G.: Automated consistency checking of requirements specifications. ACM Trans Softw Eng Methodol 5(3), 231–261 (1996)CrossRef Heitmeyer, C.L., Jeffords, R.D., Labaw, B.G.: Automated consistency checking of requirements specifications. ACM Trans Softw Eng Methodol 5(3), 231–261 (1996)CrossRef
Zurück zum Zitat Heitmeyer, C.L., Archer, M.M., Leonard, E.I., McLean, J.D.: Applying formal methods to a certifiably secure software system. IEEE Trans Softw Eng 34(1), 82–98 (2008)CrossRef Heitmeyer, C.L., Archer, M.M., Leonard, E.I., McLean, J.D.: Applying formal methods to a certifiably secure software system. IEEE Trans Softw Eng 34(1), 82–98 (2008)CrossRef
Zurück zum Zitat Heitmeyer, C.L., Shukla, S., Archer, M.M., Leonard, E.I.: On model-based software development. In: Munch, J., Schmid, K. (eds) Perspectives on the Future of Software Engineering, Springer, Berlin, Germany, pp 49–60 (2013b) Heitmeyer, C.L., Shukla, S., Archer, M.M., Leonard, E.I.: On model-based software development. In: Munch, J., Schmid, K. (eds) Perspectives on the Future of Software Engineering, Springer, Berlin, Germany, pp 49–60 (2013b)
Zurück zum Zitat Heninger, K.L.: Specifying software requirements for complex systems: New techniques and their application. IEEE Trans Softw Eng 6(1), 2–13 (1980)CrossRef Heninger, K.L.: Specifying software requirements for complex systems: New techniques and their application. IEEE Trans Softw Eng 6(1), 2–13 (1980)CrossRef
Zurück zum Zitat ITU: Message Sequence Charts. Recommendation Z.120, Intern. Telecomm. Union, Telecomm. Standardization Sector (1999) ITU: Message Sequence Charts. Recommendation Z.120, Intern. Telecomm. Union, Telecomm. Standardization Sector (1999)
Zurück zum Zitat Jeffords, R., Heitmeyer, C.: Automatic generation of state invariants from requirements specifications. In: Proceedings of the 6th ACM SIGSOFT Symposium on Foundations of Software Engineering (FSE), pp. 56–69. Lake Buena Vista, Florida (1998) Jeffords, R., Heitmeyer, C.: Automatic generation of state invariants from requirements specifications. In: Proceedings of the 6th ACM SIGSOFT Symposium on Foundations of Software Engineering (FSE), pp. 56–69. Lake Buena Vista, Florida (1998)
Zurück zum Zitat Jeffords, R.D., Heitmeyer, C.L.: A strategy for efficiently verifying requirements. ACM SIGSOFT Softw Eng Notes 28, 28–37 (2003)CrossRef Jeffords, R.D., Heitmeyer, C.L.: A strategy for efficiently verifying requirements. ACM SIGSOFT Softw Eng Notes 28, 28–37 (2003)CrossRef
Zurück zum Zitat Just, M.A., Carpenter, P.A.: Eye fixations and cognitive processes. Cogn Psychol 8(4), 441–480 (1976)CrossRef Just, M.A., Carpenter, P.A.: Eye fixations and cognitive processes. Cogn Psychol 8(4), 441–480 (1976)CrossRef
Zurück zum Zitat Kira, K., Rendell, L.A.: A practical approach to feature selection. In: Proceedings of the 9th International Workshop on Machine Learning (ML), pp. 249–256. Aberdeen, Scotland (1992) Kira, K., Rendell, L.A.: A practical approach to feature selection. In: Proceedings of the 9th International Workshop on Machine Learning (ML), pp. 249–256. Aberdeen, Scotland (1992)
Zurück zum Zitat Leonard, E.I., Heitmeyer, C.L.: Program synthesis from formal requirements specifications using APTS. High Order Symb Comput 16(1–2), 63–92 (2003)CrossRefMATH Leonard, E.I., Heitmeyer, C.L.: Program synthesis from formal requirements specifications using APTS. High Order Symb Comput 16(1–2), 63–92 (2003)CrossRefMATH
Zurück zum Zitat Leonard, E.I., Archer, M., Heitmeyer, C.L., Jeffords, R.D.: Direct generation of invariants for reactive models. In: Proc. 10th ACM/IEEE Conference on Formal Methods and Models for Co-Design (MEMOCODE), pp 119–130 (2012) Leonard, E.I., Archer, M., Heitmeyer, C.L., Jeffords, R.D.: Direct generation of invariants for reactive models. In: Proc. 10th ACM/IEEE Conference on Formal Methods and Models for Co-Design (MEMOCODE), pp 119–130 (2012)
Zurück zum Zitat Pickett, M., Aha, D.W., Trafton, J.G.: Acquiring user models to test automated assistants. In: Proceedings of the 26th International Florida Artificial Intelligence Research Society Conference (FLAIRS), pp 112–117 (2013) Pickett, M., Aha, D.W., Trafton, J.G.: Acquiring user models to test automated assistants. In: Proceedings of the 26th International Florida Artificial Intelligence Research Society Conference (FLAIRS), pp 112–117 (2013)
Zurück zum Zitat Ratwani, R., Trafton, J.G.: A real-time eye tracking system for predicting postcompletion errors. Hum Comput Interact 26(3), 205–245 (2011) Ratwani, R., Trafton, J.G.: A real-time eye tracking system for predicting postcompletion errors. Hum Comput Interact 26(3), 205–245 (2011)
Zurück zum Zitat Rayner, K.: Eye movements in reading and information processing: 20 years of research. Psychol Bull 124(3), 372 (1998)CrossRef Rayner, K.: Eye movements in reading and information processing: 20 years of research. Psychol Bull 124(3), 372 (1998)CrossRef
Zurück zum Zitat Rayner, K., Morris, R.K.: Do eye movements reflect higher order processes in reading? In: From Eye to Mind. Information Acquisition in Perception, Search, and Reading, North-Holland, pp 191–204 (1990) Rayner, K., Morris, R.K.: Do eye movements reflect higher order processes in reading? In: From Eye to Mind. Information Acquisition in Perception, Search, and Reading, North-Holland, pp 191–204 (1990)
Zurück zum Zitat Rothamel, T., Heitmeyer, C., Leonard, E., Liu, A.: Generating optimized code from SCR specifications. In: Proceedings of the ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2006) (2006) Rothamel, T., Heitmeyer, C., Leonard, E., Liu, A.: Generating optimized code from SCR specifications. In: Proceedings of the ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2006) (2006)
Zurück zum Zitat Sammut, C., Hurst, S., Kedzier, D., Michie, D.: Learning to fly. In: Sleeman, D.H., Edwards, P. (eds.) Proceedings of the 9th International Workshop on Machine Learning (ML), pp. 385–393. Morgan Kaufmann, Aberdeen, Scotland (1992) Sammut, C., Hurst, S., Kedzier, D., Michie, D.: Learning to fly. In: Sleeman, D.H., Edwards, P. (eds.) Proceedings of the 9th International Workshop on Machine Learning (ML), pp. 385–393. Morgan Kaufmann, Aberdeen, Scotland (1992)
Zurück zum Zitat Selic, B.: The pragmatics of model-driven development. IEEE Softw 20(5), 19–25 (2003)CrossRef Selic, B.: The pragmatics of model-driven development. IEEE Softw 20(5), 19–25 (2003)CrossRef
Zurück zum Zitat Sengupta, S.: U.S. border agency allows others to use its drones. New York Times, (2013) Sengupta, S.: U.S. border agency allows others to use its drones. New York Times, (2013)
Zurück zum Zitat Šuc, D., Bratko, I., Sammut, C.: Learning to fly simple and robust. In: Proceedings of the 15th European Conference on Machine Learning (ECML), pp. 407–418. Pisa, Italy (2004) Šuc, D., Bratko, I., Sammut, C.: Learning to fly simple and robust. In: Proceedings of the 15th European Conference on Machine Learning (ECML), pp. 407–418. Pisa, Italy (2004)
Zurück zum Zitat Swets, J.A.: Signal detection theory and ROC analysis in psychology and diagnostics: Collected Papers. Lawrence Erlbaum Associates, Mahawa (1996)MATH Swets, J.A.: Signal detection theory and ROC analysis in psychology and diagnostics: Collected Papers. Lawrence Erlbaum Associates, Mahawa (1996)MATH
Zurück zum Zitat Uchitel, S., Kramer, J., Magee, J.: Synthesis of behavioral models from scenarios. IEEE Trans Softw Eng 29(2), 99–115 (2003)CrossRef Uchitel, S., Kramer, J., Magee, J.: Synthesis of behavioral models from scenarios. IEEE Trans Softw Eng 29(2), 99–115 (2003)CrossRef
Zurück zum Zitat Uchitel, S., Brunet, G., Chechik, M.: Synthesis of partial behaviour model synthesis from properties and scenarios. IEEE Trans Softw Eng 35(3), 384–406 (2009)CrossRef Uchitel, S., Brunet, G., Chechik, M.: Synthesis of partial behaviour model synthesis from properties and scenarios. IEEE Trans Softw Eng 35(3), 384–406 (2009)CrossRef
Zurück zum Zitat US Senate: The future of drones in America: law enforcement and privacy considerations, hearing before the Committee on the Judiciary. Tech. Rep. J-113-10, Washington, DC (2013) US Senate: The future of drones in America: law enforcement and privacy considerations, hearing before the Committee on the Judiciary. Tech. Rep. J-113-10, Washington, DC (2013)
Zurück zum Zitat Whittle, J., Schumann, J.: Generating statechart designs from scenarios. In: Proceedings of the 22nd International Conference on Software Engineering (ICSE), pp. 314–323. Limerick, Ireland (2000) Whittle, J., Schumann, J.: Generating statechart designs from scenarios. In: Proceedings of the 22nd International Conference on Software Engineering (ICSE), pp. 314–323. Limerick, Ireland (2000)
Metadaten
Titel
Building high assurance human-centric decision systems
verfasst von
Constance L. Heitmeyer
Marc Pickett
Elizabeth I. Leonard
Myla M. Archer
Indrakshi Ray
David W. Aha
J. Gregory Trafton
Publikationsdatum
01.06.2015
Verlag
Springer US
Erschienen in
Automated Software Engineering / Ausgabe 2/2015
Print ISSN: 0928-8910
Elektronische ISSN: 1573-7535
DOI
https://doi.org/10.1007/s10515-014-0157-z

Weitere Artikel der Ausgabe 2/2015

Automated Software Engineering 2/2015 Zur Ausgabe

Premium Partner