[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

Guaranteeing functional safety: design for provability and computer-aided verification

  • Published:
Autonomous Robots Aims and scope Submit manuscript

Abstract

When autonomous robots begin to share the human living and working spaces, safety becomes paramount. It is legally required that the safety of such systems is ensured, e.g. by certification according to relevant standards such as IEC 61508. However, such safety considerations are usually not addressed in academic robotics. In this paper we report on one such successful endeavor, which is concerned with designing, implementing, and certifying a collision avoidance safety function for autonomous vehicles and static obstacles. The safety function calculates a safety zone for the vehicle, depending on its current motion, which is as large as required but as small as feasible, thus ensuring safety against collision with static obstacles. We outline the algorithm which was specifically designed with safety in mind, and present our verification methodology which is based on formal proof and verification using the theorem prover Isabelle. The implementation and our methodology have been certified for use in applications up to SIL 3 of IEC 61508 by a certification authority (TÜV Süd Rail GmbH, Germany). Throughout, issues we recognized as being important for a successful application of formal methods in robotics are highlighted. Moreover, we argue that formal analysis deepens the understanding of the algorithm, and hence is valuable even outside the safety context.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

References

  • Althoff, M., Althoff, D., Wollherr, D., & Buss, M. (2010). Safety verification of autonomous vehicles for coordinated evasive maneuvers. In Intelligent vehicles symposium (IV), 2010 IEEE (pp. 1078–1083).

    Chapter  Google Scholar 

  • ANSI R15.06 (1999). Industrial robots and robot systems—safety requirements.

  • Barnes, J. (2003). High integrity software: the SPARK approach to safety and security. Reading: Addison-Wesley.

    Google Scholar 

  • Baudin, P., Cuoq, P., Filliâtre, J. C., Marché, C., Monate, B., Moy, Y., & Prevosto, V. (2008). ACSL: ANSI C specification language. http://frama-c.com/download/acsl_1.4.pdf, version 1.4, retrieved Jan 2011.

  • Bengtsson, J., Larsen, K. G., Larsson, F., Pettersson, P., & Yi, W. (1995). Uppaal—a tool suite for automatic verification of real-time systems. In Lecture notes in computer science: Vol. 1066. Proc. of workshop on verification and control of hybrid systems III (pp. 232–243). Berlin: Springer.

    Google Scholar 

  • Bensalem, S., Gallien, M., Ingrand, F., Kahloul, I., & Nguyen, T. H., (2009). Designing autonomous robots: toward a more dependable software architecture. IEEE Robotics & Automation Magazine, 16(1), 67–77.

    Article  Google Scholar 

  • Bensalem, S., Bozga, M., Nguyen, T. H., & Sifakis, J. (2010a). Compositional verification for component-based systems and application. IET Software, 4(3), 181–193. doi:10.1049/iet-sen.2009.0011.

    Article  Google Scholar 

  • Bensalem, S., da Silva, L., Gallien, M., Ingrand, F., & Yan, R. (2010b). Verifiable and correct-by-construction controller for robots in human environments. In DRHE 2010 dependable robots in human environments, seventh IARP workshop on technical challenges for dependable robots in human environments, Toulouse, France.

    Google Scholar 

  • Braman, J. M. B. (2009). Safety verification of goal-based control programs for autonomous robotic systems. Talk at ICRA09 workshop on formal methods in robotics.

  • Braman, J. M. B., Murray, R. M., & Wagner, D. A. (2007). Safety verification of a fault tolerant reconfigurable autonomous goal-based robotic control system. In Proceedings of the IEEE/RSJ international conference on intelligent robots and systems (pp. 853–858), San Diego.

    Google Scholar 

  • Burdy, L., Cheon, Y., Cok, D., Ernst, M. D., Kiniry, J., Leavens, G. T., Leino, K. R. M., & Poll, E. (2005). An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer, 7(3), 212–232.

    Article  Google Scholar 

  • Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., & Tobies, S. (2009). VCC: a practical system for verifying concurrent C. In Lecture notes in computer science: Vol. 5674. TPHOLs 2009. Berlin: Springer.

    Google Scholar 

  • Dion, B., & Gartner, J. (2005). Efficient development of embedded automotive software with IEC 61508 objectives using SCADE drive. In VDI 12th international conference: electronic systems for vehicles, VDI (pp. 1427–1436).

    Google Scholar 

  • Dolginova, E., & Lynch, N. (1997). Safety verification for automated platoon maneuvers: a case study. In Lecture notes in computer science: Vol. 1201. Hybrid and real-time systems (pp. 154–170). Berlin: Springer.

    Google Scholar 

  • Du Toit, N. E., Wongpiromsarn, T., Burdick, J. W., & Murray, R. M. (2008). Situational reasoning for road driving in an urban environment. In Intelligent vehicle control systems: proceedings of the 2nd international workshop on intelligent vehicle control systems (IVCS) (pp. 30–39). Setubal: INSTICC Press.

    Google Scholar 

  • EN 1525 (1997). Safety of industrial trucks—driverless trucks and their systems.

  • Ericson, C. (2005). Real-time collision detection. San Mateo: Morgan Kaufmann.

    Google Scholar 

  • European Parliament and Council (2006). Directive 2006/42/EC. Official Journal of the European Union L 157.

  • Fiorini, P., & Shillert, Z. (1998). Motion planning in dynamic environments using velocity obstacles. The International Journal of Robotics Research, 17, 760–772.

    Article  Google Scholar 

  • Fox, D., Burgard, W., & Thrun, S. (1997). The dynamic window approach to collision avoidance. IEEE Robotics & Automation Magazine, 4(1), 23–33.

    Article  Google Scholar 

  • Fraichard, T. (2007). A short paper about motion safety. In Proceedings of the IEEE international conference on robotics and automation.

    Google Scholar 

  • Fraichard, T., & Asama, H. (2004). Inevitable collision states—a step towards safer robots? Advanced Robotics, 18(10), 1001–1024.

    Article  Google Scholar 

  • Gates, B. (2007). A robot in every home. Scientific American, 296(January), 58–65. doi:10.1038/scientificamerican0107-58.

    Article  Google Scholar 

  • Gordon, M., Milner, R., & Wadsworth, C. (1979). Lecture notes in computer science: Vol. 78. Edinburgh LCF: a mechanised logic of computation. Berlin: Springer.

    Google Scholar 

  • Gurevich, Y. (2000). Sequential abstract state machines capture sequential algorithms. ACM Transactions on Computational Logic, 1(1), 77–111.

    Article  MathSciNet  Google Scholar 

  • Harel, D. (1987). StateCharts: a visual formalism for complex systems. Science of Computer Programming, 8, 231–274.

    Article  MathSciNet  MATH  Google Scholar 

  • Henzinger, T. A., Ho, P. H., & Wong-Toi, H. (1997). HyTech: a model checker for hybrid systems. Software Tools for Technology Transfer, 1, 110–122.

    Article  MATH  Google Scholar 

  • Hoare, C. A. R. (2009). Viewpoint: retrospective: an axiomatic basis for computer programming. Communications of the ACM, 52(10), 30–32.

    Article  Google Scholar 

  • Holzmann, G. J. (2003). The SPIN model checker: primer and reference manual. Reading: Addison-Wesley.

    Google Scholar 

  • IEC 61508 (2000). Functional safety of electrical/electronic/programmable electronic safety-related systems.

  • ISO 10218-1 (2006). Robots for industrial environments—safety requirements—part 1: Robot.

  • ISO 15623 (2002). Road vehicles: forward vehicle collision warning system—performance requirements and test procedures.

  • ISO 26262 (2011). Road vehicles—functional safety (Final draft).

  • Khatib, O. (1986). Real-time obstacle avoidance for manipulators and mobile robots. The International Journal of Robotics Research, 5(1), 90–98.

    Article  MathSciNet  Google Scholar 

  • Lankenau, A., & Röfer, T. (2001). A safe and versatile mobility assistant. IEEE Robotics & Automation Magazine, 8(1), 29–37.

    Article  Google Scholar 

  • Loos, S., Platzer, A., & Nistor, L. (2011). Adaptive cruise control: hybrid, distributed, and now formally verified. In Lecture notes in computer science: Vol. 6664. Formal methods (pp. 42–56). Berlin: Springer.

    Google Scholar 

  • Lüth, C., & Walter, D. (2009). Certifiable specification and verification of C programs. In Lecture notes in computer science: Vol. 5850. Formal methods (pp. 419–434). Berlin: Springer.

    Google Scholar 

  • Meikle, L., & Fleuriot, J. (2009). Mechanical theorem proving in computational geometry. In Lecture notes in computer science: Vol. 3763. Automated deduction in geometry. Berlin: Springer.

    Google Scholar 

  • Meyer, B. (1991). Design by contract. In D. Mandrioli & B. Meyer (Eds.), Advances in object-oriented software engineering (pp. 1–50). New York: Prentice Hall.

    Google Scholar 

  • Minguez, J., & Montano, L. (2004). Nearness diagram (ND) navigation: collision avoidance in troublesome scenarios. IEEE Transactions on Robotics and Automation, 20(1), 45–59.

    Article  Google Scholar 

  • MISRA (2004). MISRA-C:2004—guidelines for the use of the C language in critical systems. Nuneaton: Motor Industry Research Association (MIRA) Limited.

    Google Scholar 

  • Nilsson, N. J. (1984). Shakey the robot. Tech. rep. 323, SRI International, Menlo Park, California.

  • Nipkow, T., Paulson, L. C., & Wenzel, M. (2002). Lecture notes in computer science: Vol. 2283. Isabelle/HOL—a proof assistant for higher-order logic. Berlin: Springer.

    Google Scholar 

  • Parthasarathi, R., & Fraichard, T. (2007). An inevitable collision state-checker for a car-like vehicle. In Proceedings of the IEEE international conference on robotics and automation.

    Google Scholar 

  • Philippsen, R., & Siegwart, R. (2003). Smooth and efficient obstacle avoidance for a tour guide robot. In Proceedings of the IEEE international conference on robotics and automation.

    Google Scholar 

  • Platzer, A., & Clarke, E. M. (2009). Formal verification of curved flight collision avoidance maneuvers: a case study. In Lecture notes in computer science: Vol. 5850. Formal methods (pp. 547–562). Berlin: Springer.

    Google Scholar 

  • Puri, A., & Varaiya, P. (1995). Driving safely in smart cars. In Proceedings of the American control conference (Vol. 5, pp. 3597–3599).

    Google Scholar 

  • Rabe, C., Franke, U., & Gehrig, S. (2007). Fast detection of moving objects in complex scenarios. In Proceedings of the IEEE intelligent vehicles symposium (pp. 398–403).

    Chapter  Google Scholar 

  • Roscoe, A. W. (1998). The theory and practice of concurrency. New York: Prentice Hall.

    Google Scholar 

  • RT-Tester (2006). User manual. Verified Systems International GmbH, http://www.verified.de/en/products/rt-tester, retrieved Jan. 2011.

  • Schlegel, C. (1998). Fast local obstacle avoidance under kinematic and dynamic constraints for a mobile robot. In Proceedings of the IEEE/RSJ international conference on intelligent robots and systems.

    Google Scholar 

  • Simon, D., Pissard-Gibollet, R., & Arias, S. (2006). Orccad, a framework for safe robot control design and implementation. In 1st national workshop on control architectures of robots: software approaches and issues CAR’06, Montpellier, France.

    Google Scholar 

  • Täubig, H., Bäuml, B., & Frese, U. (2011). Real-time swept volume and distance computation for self collision detection. In Proceedings of the IEEE/RSJ international conference on intelligent robots and systems (IROS), San Francisco, CA, United States.

    Google Scholar 

  • Varaiya, P. (1993). Smart cars on smart roads: problems of control. IEEE Transactions on Automatic Control, 38(2), 195–207.

    Article  MathSciNet  Google Scholar 

  • Victorino, A. C., Rives, P., & Borelly, J. J. (2003). Safe navigation for indoor mobile robots. Part I: A sensor-based navigation framework. The International Journal of Robotics Research, 22(12), 1005–1118.

    Article  Google Scholar 

  • Winner, H., Haskuli, S., & Wolf, G. (Eds.) (2009). Handbuch Fahrerassistenzsysteme. Berlin: Vieweg+Teubner (in German).

    Google Scholar 

  • Wongpiromsarn, T., Mitra, S., Murray, R., & Lamperski, A. (2009). Periodically controlled hybrid systems. In Lecture notes in computer science: Vol. 5469. Hybrid systems: computation and control (pp. 396–410). Berlin: Springer.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. FB 3—Computer Science, University of Bremen, Bremen, Germany

    Udo Frese, Christoph Hertzberg & Elena Vorobev

  2. Cyber-Physical Systems, German Research Center for Artificial Intelligence (DFKI), Bremen, Germany

    Holger Täubig, Christoph Lüth & Dennis Walter

  3. Leuze Electronic, Fürstenfeldbruck, Germany

    Stefan Mohr

Authors
  1. Holger Täubig
    View author publications

    You can also search for this author inPubMed Google Scholar

  2. Udo Frese
    View author publications

    You can also search for this author inPubMed Google Scholar

  3. Christoph Hertzberg
    View author publications

    You can also search for this author inPubMed Google Scholar

  4. Christoph Lüth
    View author publications

    You can also search for this author inPubMed Google Scholar

  5. Stefan Mohr
    View author publications

    You can also search for this author inPubMed Google Scholar

  6. Elena Vorobev
    View author publications

    You can also search for this author inPubMed Google Scholar

  7. Dennis Walter
    View author publications

    You can also search for this author inPubMed Google Scholar

Corresponding author

Correspondence to Holger Täubig.

Electronic Supplementary Material

Below is the link to the electronic supplementary material.

(AVI 17.0 MB)

Rights and permissions

Reprints and permissions

About this article

Cite this article

Täubig, H., Frese, U., Hertzberg, C. et al. Guaranteeing functional safety: design for provability and computer-aided verification. Auton Robot 32, 303–331 (2012). https://doi.org/10.1007/s10514-011-9271-y

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10514-011-9271-y

Keywords