Top

Published in:

01-06-2015

Building high assurance human-centric decision systems

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

Published in: Automated Software Engineering | Issue 2/2015

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

previous article An experiment in ontology use for command and control interoperability

next article Designing automotive embedded systems with adaptive genetic algorithms

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now

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.

These preconditions ensure that \({\mathcal W}\) is a well-formed Moded Scenarios Description.

We treat multiple robots as a generalization of multiple UAVs.

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)

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)

Archer, M.: TAME: Using PVS strategies for special-purpose theorem proving. Ann Math Artif Intell 29(1–4), 131–189 (2001)MathSciNet

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)

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)

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

Bumiller, E., Shanker, T.: War evolves with drones, some tiny as bugs. New York Times, (2011)

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)

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

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., 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)

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)

Fawcett, T.: An introduction to ROC analysis. Pattern Recognit Lett 27(8), 861–874 (2006)CrossRefMathSciNet

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)

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)

Giannakopoulou, D., Magee, J.: Fluent model checking for event-based systems. ACM SIGSOFT Softw Eng Notes 28, 257–266 (2003)CrossRef

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)

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

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., 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., 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., 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.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., 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., 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)

Heninger, K.L.: Specifying software requirements for complex systems: New techniques and their application. IEEE Trans Softw Eng 6(1), 2–13 (1980)CrossRef

ITU: Message Sequence Charts. Recommendation Z.120, Intern. Telecomm. Union, Telecomm. Standardization Sector (1999)

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.D., Heitmeyer, C.L.: A strategy for efficiently verifying requirements. ACM SIGSOFT Softw Eng Notes 28, 28–37 (2003)CrossRef

Just, M.A., Carpenter, P.A.: Eye fixations and cognitive processes. Cogn Psychol 8(4), 441–480 (1976)CrossRef

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)

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., 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)

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)

Ratwani, R., Trafton, J.G.: A real-time eye tracking system for predicting postcompletion errors. Hum Comput Interact 26(3), 205–245 (2011)

Rayner, K.: Eye movements in reading and information processing: 20 years of research. Psychol Bull 124(3), 372 (1998)CrossRef

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)

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)

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)

Selic, B.: The pragmatics of model-driven development. IEEE Softw 20(5), 19–25 (2003)CrossRef

Sengupta, S.: U.S. border agency allows others to use its drones. New York Times, (2013)

Š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)

Swets, J.A.: Signal detection theory and ROC analysis in psychology and diagnostics: Collected Papers. Lawrence Erlbaum Associates, Mahawa (1996)MATH

Uchitel, S., Kramer, J., Magee, J.: Synthesis of behavioral models from scenarios. IEEE Trans Softw Eng 29(2), 99–115 (2003)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

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)

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)

Title: Building high assurance human-centric decision systems
Authors: Constance L. Heitmeyer
Marc Pickett
Elizabeth I. Leonard
Myla M. Archer
Indrakshi Ray
David W. Aha
J. Gregory Trafton
Publication date: 01-06-2015
Publisher: Springer US
Published in: Automated Software Engineering / Issue 2/2015
Print ISSN: 0928-8910
Electronic ISSN: 1573-7535
DOI: https://doi.org/10.1007/s10515-014-0157-z

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Other articles of this Issue 2/2015

An experiment in ontology use for command and control interoperability

Designing automotive embedded systems with adaptive genetic algorithms

Guest editorial: special issue on realizing AI synergies in software engineering (part 2)

A semantic web enabled approach to reuse functional requirements models in web engineering

Premium Partner