nach oben

Erschienen in:

2015 | OriginalPaper | Buchkapitel

Coverage-Driven Verification —

An Approach to Verify Code for Robots that Directly Interact with Humans

verfasst von : Dejanira Araiza-Illan, David Western, Anthony Pipe, Kerstin Eder

Erschienen in: Hardware and Software: Verification and Testing

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

Collaborative robots could transform several industries, such as manufacturing and healthcare, but they present a significant challenge to verification. The complex nature of their working environment necessitates testing in realistic detail under a broad range of circumstances. We propose the use of Coverage-Driven Verification (CDV) to meet this challenge. By automating the simulation-based testing process as far as possible, CDV provides an efficient route to coverage closure. We discuss the need, practical considerations, and potential benefits of transferring this approach from microelectronic design verification to the field of human-robot interaction. We demonstrate the validity and feasibility of the proposed approach by constructing a custom CDV testbench and applying it to the verification of an object handover task.

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

Vorheriges Kapitel The Verification Cockpit – Creating the Dream Playground for Data Analytics over the Verification Process

Nächstes Kapitel PANDA: Simultaneous Predicate Abstraction and Concrete Execution

http://www.ros.org/.

http://gazebosim.org/.

http://moveit.ros.org/.

http://www.uppaal.org/.

http://www.cprover.org/cbmc/.

http://javapathfinder.sourceforge.net/.

http://nedbatchelder.com/code/coverage/.

Alexander, R., Hawkins, H., Rae, D.: Situation Coverage - A Coverage Criterion for Testing Autonomous Robots. Department of Computer Science, University of York, Technical Report (2015)

Armoni, R., Korchemny, D., Tiemeyer, A., Vardi, M.Y., Zbar, Y.: Deterministic dynamic monitors for linear-time assertions. In: Havelund, K., Núñez, M., Roşu, G., Wolff, B. (eds.) FATES 2006 and RV 2006. LNCS, vol. 4262, pp. 163–177. Springer, Heidelberg (2006) CrossRef

Bordini, R.H., Fisher, M., Sierhuis, M.: Formal verification of human-robot teamwork. In: Proceedings of ACM/IEEE HRI, pp. 267–268 (2009)

Boren, J., Cousins, S.: The SMACH high-level executive. IEEE Robot. Autom. Mag. 17(4), 18–20 (2010)CrossRef

Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)

Cowley, A., Taylor, C.J.: Towards language-based verification of robot behaviors. In: Proceedings of IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pp. 4776–4782. IEEE (2011)

Eder, K., Harper, C., Leonards, U.: Towards the safety of human-in-the-loop robotics: challenges and opportunities for safety assurance of robotic co-workers. In: Proceedings of IEEE ROMAN, pp. 660–665 (2014)

Foster, H.D., Krolnik, A.C., Lacey, D.J.: Assertion-Based Design, 2nd edn. Springer, Heidelberg (2004)

Grigore, E.C., Eder, K., Lenz, A., Skachek, S., Pipe, A.G., Melhuish, C.: Towards safe human-robot interaction. In: Groß, R., Alboul, L., Melhuish, C., Witkowski, M., Prescott, T.J., Penders, J. (eds.) TAROS 2011. LNCS, vol. 6856, pp. 323–335. Springer, Heidelberg (2011) CrossRef

10.

Haedicke, F., Le, H., Grosse, D., Drechsler, R.: CRAVE: an advanced constrained random verification environment for System C. In: Proceedings of SoC, pp. 1–7 (2012)

11.

Hartmanns, A., Hermanns, H.: A modest approach to checking probabilistic timed automata. In: Proceedings of QEST, pp. 187–196 (2009)

12.

Havelund, K., Roşu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 342–356. Springer, Heidelberg (2002) CrossRef

13.

Ioannides, C., Eder, K.I.: Coverage-directed test generation automated by machine learning - a review. ACM Trans. Des. Autom. Electron. Syst. 17(1), 7:1–7:21 (2012)CrossRef

14.

Kouskoulas, Y., Renshaw, D.W., Platzer, A., Kazanzides, P.: Certifying the safe design of a virtual fixture control algorithm for a surgical robot. In: Belta, C., Ivancic, F. (eds.) Proceedings of Hybrid Systems: Computation and Control (HSCC), pp. 263–272. ACM (2013)

15.

Lackner, H., Schlingloff, B.: Modeling for automated test generation a comparison. In: Proceedings of MBEES Workshop (2012)

16.

Lakhotia, K., McMinn, P., Harman, M.: Automated test data generation for coverage: haven’t we solved this problem yet? In: Proceedings TAIC (2009)

17.

Lenz, A., Skachek, S., Hamann, K., Steinwender, J., Pipe, A., Melhuish, C.: The BERT2 infrastructure: an integrated system for the study of human-robot interaction. In: Proceedings of IEEE-RAS Humanoids, pp. 346–351 (2010)

18.

Milner, R.: A Calculus of Communicating Systems. LNCS. Springer, Heidelberg (1980) CrossRefMATH

19.

Mohammed, A., Furbach, U., Stolzenburg, F.: Multi-robot systems: modeling, specification, and model checking. In: Robot Soccer, pp. 241–265 (2010)

20.

Muradore, R., Bresolin, D., Geretti, L., Fiorini, P., Villa, T.: Robotic surgery. IEEE Robot. Autom. Mag. 18(3), 24–32 (2011)CrossRef

21.

Nielsen, B., Skou, A.: Automated test generation from timed automata. Int. J. Softw. Tools Technol. Transfer 5, 59–77 (2003)CrossRefMATH

22.

Nielsen, B.: Towards a method for combined model-based testing and analysis. In: Proceedings of MODELSWARD, pp. 609–618 (2014)

23.

Piziali, A.: Functional Verification Coverage Measurement and Analysis. Kluwer Academic, Boston (2004)

24.

Trojanek, P., Eder, K.: Verification and testing of mobile robot navigation algorithms: a case study in SPARK. In: Proceedings of IROS, pp. 1489–1494 (2014)

25.

Webster, M., Dixon, C., Fisher, M., Salem, M., Saunders, J., Koay, K.L., Dautenhahn, K.: Formal verification of an autonomous personal robotic assistant. In: Proceedings of AAAI FVHMS 2014, pp. 74–79 (2014)

26.

Wile, B., Goss, J.C., Roesner, W.: Comprehensive Functional Verification. Morgan Kaufmann, San Francisco (2005)

Titel: Coverage-Driven Verification —
verfasst von: Dejanira Araiza-Illan
David Western
Anthony Pipe
Kerstin Eder
Verlag: Springer International Publishing
Buch: Hardware and Software: Verification and Testing
Print ISBN: 978-3-319-26286-4

Electronic ISBN: 978-3-319-26287-1

Copyright-Jahr: 2015
DOI: https://doi.org/10.1007/978-3-319-26287-1_5

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner