{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,5]],"date-time":"2026-10-05T09:01:42Z","timestamp":1791190902347,"version":"4.1.0"},"reference-count":57,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2011,12,22]],"date-time":"2011-12-22T00:00:00Z","timestamp":1324512000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Auton Robot"],"published-print":{"date-parts":[[2012,4]]},"DOI":"10.1007\/s10514-011-9271-y","type":"journal-article","created":{"date-parts":[[2011,12,21]],"date-time":"2011-12-21T16:55:43Z","timestamp":1324486543000},"page":"303-331","source":"Crossref","is-referenced-by-count":38,"title":["Guaranteeing functional safety: design for provability and computer-aided verification"],"prefix":"10.1007","volume":"32","author":[{"given":"Holger","family":"T\u00e4ubig","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Udo","family":"Frese","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christoph","family":"Hertzberg","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christoph","family":"L\u00fcth","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stefan","family":"Mohr","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Elena","family":"Vorobev","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dennis","family":"Walter","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2011,12,22]]},"reference":[{"key":"9271_CR1","doi-asserted-by":"crossref","first-page":"1078","DOI":"10.1109\/IVS.2010.5548121","volume-title":"Intelligent vehicles symposium (IV), 2010 IEEE","author":"M. Althoff","year":"2010","unstructured":"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.\u00a01078\u20131083)."},{"key":"9271_CR2","unstructured":"ANSI R15.06 (1999). Industrial robots and robot systems\u2014safety requirements."},{"key":"9271_CR3","volume-title":"High integrity software: the SPARK approach to safety and security","author":"J. Barnes","year":"2003","unstructured":"Barnes, J. (2003). High integrity software: the SPARK approach to safety and security. Reading: Addison-Wesley."},{"key":"9271_CR4","unstructured":"Baudin, P., Cuoq, P., Filli\u00e2tre, J. C., March\u00e9, C., Monate, B., Moy, Y., & Prevosto, V. (2008). ACSL: ANSI C specification language. http:\/\/frama-c.com\/download\/acsl_1.4.pdf , version\u00a01.4, retrieved Jan 2011."},{"key":"9271_CR5","series-title":"Proc. of workshop on verification and control of hybrid systems III","first-page":"232","volume-title":"Lecture notes in computer science","author":"J. Bengtsson","year":"1995","unstructured":"Bengtsson, J., Larsen, K. G., Larsson, F., Pettersson, P., & Yi, W. (1995). Uppaal\u2014a tool suite for automatic verification of real-time systems. In Lecture notes in computer science: Vol.\u00a01066. Proc. of workshop on verification and control of hybrid systems III (pp.\u00a0232\u2013243). Berlin: Springer."},{"issue":"1","key":"9271_CR6","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1109\/MRA.2008.931631","volume":"16","author":"S. Bensalem","year":"2009","unstructured":"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\u201377.","journal-title":"IEEE Robotics & Automation Magazine"},{"issue":"3","key":"9271_CR7","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1049\/iet-sen.2009.0011","volume":"4","author":"S. Bensalem","year":"2010","unstructured":"Bensalem, S., Bozga, M., Nguyen, T. H., & Sifakis, J. (2010a). Compositional verification for component-based systems and application. IET Software, 4(3), 181\u2013193. doi: 10.1049\/iet-sen.2009.0011 .","journal-title":"IET Software"},{"key":"9271_CR8","volume-title":"DRHE 2010 dependable robots in human environments, seventh IARP workshop on technical challenges for dependable robots in human environments","author":"S. Bensalem","year":"2010","unstructured":"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."},{"key":"9271_CR9","unstructured":"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."},{"key":"9271_CR10","first-page":"853","volume-title":"Proceedings of the IEEE\/RSJ international conference on intelligent robots and systems","author":"J. M. B. Braman","year":"2007","unstructured":"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.\u00a0853\u2013858), San Diego."},{"issue":"3","key":"9271_CR11","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L. Burdy","year":"2005","unstructured":"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\u2013232.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"9271_CR12","series-title":"TPHOLs 2009","volume-title":"Lecture notes in computer science","author":"E. Cohen","year":"2009","unstructured":"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.\u00a05674. TPHOLs 2009. Berlin: Springer."},{"key":"9271_CR13","first-page":"1427","volume-title":"VDI 12th international conference: electronic systems for vehicles, VDI","author":"B. Dion","year":"2005","unstructured":"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\u20131436)."},{"key":"9271_CR14","series-title":"Hybrid and real-time systems","first-page":"154","volume-title":"Lecture notes in computer science","author":"E. Dolginova","year":"1997","unstructured":"Dolginova, E., & Lynch, N. (1997). Safety verification for automated platoon maneuvers: a case study. In Lecture notes in computer science: Vol.\u00a01201. Hybrid and real-time systems (pp. 154\u2013170). Berlin: Springer."},{"key":"9271_CR15","first-page":"30","volume-title":"Intelligent vehicle control systems: proceedings of the 2nd international workshop on intelligent vehicle control systems (IVCS)","author":"N. E. Du Toit","year":"2008","unstructured":"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\u201339). Setubal: INSTICC Press."},{"key":"9271_CR16","unstructured":"EN 1525 (1997). Safety of industrial trucks\u2014driverless trucks and their systems."},{"key":"9271_CR17","volume-title":"Real-time collision detection","author":"C. Ericson","year":"2005","unstructured":"Ericson, C. (2005). Real-time collision detection. San Mateo: Morgan Kaufmann."},{"key":"9271_CR18","unstructured":"European Parliament and Council (2006). Directive 2006\/42\/EC. Official Journal of the European Union L 157."},{"key":"9271_CR19","doi-asserted-by":"crossref","first-page":"760","DOI":"10.1177\/027836499801700706","volume":"17","author":"P. Fiorini","year":"1998","unstructured":"Fiorini, P., & Shillert, Z. (1998). Motion planning in dynamic environments using velocity obstacles. The International Journal of Robotics Research, 17, 760\u2013772.","journal-title":"The International Journal of Robotics Research"},{"issue":"1","key":"9271_CR20","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1109\/100.580977","volume":"4","author":"D. Fox","year":"1997","unstructured":"Fox, D., Burgard, W., & Thrun, S. (1997). The dynamic window approach to collision avoidance. IEEE Robotics & Automation Magazine, 4(1), 23\u201333.","journal-title":"IEEE Robotics & Automation Magazine"},{"key":"9271_CR21","volume-title":"Proceedings of the IEEE international conference on robotics and automation","author":"T. Fraichard","year":"2007","unstructured":"Fraichard, T. (2007). A short paper about motion safety. In Proceedings of the IEEE international conference on robotics and automation."},{"issue":"10","key":"9271_CR22","doi-asserted-by":"crossref","first-page":"1001","DOI":"10.1163\/1568553042674662","volume":"18","author":"T. Fraichard","year":"2004","unstructured":"Fraichard, T., & Asama, H. (2004). Inevitable collision states\u2014a step towards safer robots? Advanced Robotics, 18(10), 1001\u20131024.","journal-title":"Advanced Robotics"},{"issue":"January","key":"9271_CR23","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1038\/scientificamerican0107-58","volume":"296","author":"B. Gates","year":"2007","unstructured":"Gates, B. (2007). A robot in every home. Scientific American, 296(January), 58\u201365. doi: 10.1038\/scientificamerican0107-58 .","journal-title":"Scientific American"},{"key":"9271_CR24","series-title":"Edinburgh LCF: a mechanised logic of computation","volume-title":"Lecture notes in computer science","author":"M. Gordon","year":"1979","unstructured":"Gordon, M., Milner, R., & Wadsworth, C. (1979). Lecture notes in computer science: Vol.\u00a078. Edinburgh LCF: a mechanised logic of computation. Berlin: Springer."},{"issue":"1","key":"9271_CR25","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1145\/343369.343384","volume":"1","author":"Y. Gurevich","year":"2000","unstructured":"Gurevich, Y. (2000). Sequential abstract state machines capture sequential algorithms. ACM Transactions on Computational Logic, 1(1), 77\u2013111.","journal-title":"ACM Transactions on Computational Logic"},{"key":"9271_CR26","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"Harel, D. (1987). StateCharts: a visual formalism for complex systems. Science of Computer Programming, 8, 231\u2013274.","journal-title":"Science of Computer Programming"},{"key":"9271_CR27","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"T. A. Henzinger","year":"1997","unstructured":"Henzinger, T. A., Ho, P. H., & Wong-Toi, H. (1997). HyTech: a model checker for hybrid systems. Software Tools for Technology Transfer, 1, 110\u2013122.","journal-title":"Software Tools for Technology Transfer"},{"issue":"10","key":"9271_CR28","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1145\/1562764.1562779","volume":"52","author":"C. A. R. Hoare","year":"2009","unstructured":"Hoare, C. A. R. (2009). Viewpoint: retrospective: an axiomatic basis for computer programming. Communications of the ACM, 52(10), 30\u201332.","journal-title":"Communications of the ACM"},{"key":"9271_CR29","volume-title":"The SPIN model checker: primer and reference manual","author":"G. J. Holzmann","year":"2003","unstructured":"Holzmann, G. J. (2003). The SPIN model checker: primer and reference manual. Reading: Addison-Wesley."},{"key":"9271_CR30","unstructured":"IEC 61508 (2000). Functional safety of electrical\/electronic\/programmable electronic safety-related systems."},{"key":"9271_CR31","unstructured":"ISO 10218-1 (2006). Robots for industrial environments\u2014safety requirements\u2014part 1: Robot."},{"key":"9271_CR32","unstructured":"ISO 15623 (2002). Road vehicles: forward vehicle collision warning system\u2014performance requirements and test procedures."},{"key":"9271_CR33","unstructured":"ISO 26262 (2011). Road vehicles\u2014functional safety (Final draft)."},{"issue":"1","key":"9271_CR34","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1177\/027836498600500106","volume":"5","author":"O. Khatib","year":"1986","unstructured":"Khatib, O. (1986). Real-time obstacle avoidance for manipulators and mobile robots. The International Journal of Robotics Research, 5(1), 90\u201398.","journal-title":"The International Journal of Robotics Research"},{"issue":"1","key":"9271_CR35","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1109\/100.924355","volume":"8","author":"A. Lankenau","year":"2001","unstructured":"Lankenau, A., & R\u00f6fer, T. (2001). A safe and versatile mobility assistant. IEEE Robotics & Automation Magazine, 8(1), 29\u201337.","journal-title":"IEEE Robotics & Automation Magazine"},{"key":"9271_CR36","series-title":"Formal methods","first-page":"42","volume-title":"Lecture notes in computer science","author":"S. Loos","year":"2011","unstructured":"Loos, S., Platzer, A., & Nistor, L. (2011). Adaptive cruise control: hybrid, distributed, and now formally verified. In Lecture notes in computer science: Vol.\u00a06664. Formal methods (pp. 42\u201356). Berlin: Springer."},{"key":"9271_CR37","series-title":"Formal methods","first-page":"419","volume-title":"Lecture notes in computer science","author":"C. L\u00fcth","year":"2009","unstructured":"L\u00fcth, C., & Walter, D. (2009). Certifiable specification and verification of C programs. In Lecture notes in computer science: Vol.\u00a05850. Formal methods (pp. 419\u2013434). Berlin: Springer."},{"key":"9271_CR38","series-title":"Automated deduction in geometry","volume-title":"Lecture notes in computer science","author":"L. Meikle","year":"2009","unstructured":"Meikle, L., & Fleuriot, J. (2009). Mechanical theorem proving in computational geometry. In Lecture notes in computer science: Vol.\u00a03763. Automated deduction in geometry. Berlin: Springer."},{"key":"9271_CR39","first-page":"1","volume-title":"Advances in object-oriented software engineering","author":"B. Meyer","year":"1991","unstructured":"Meyer, B. (1991). Design by contract. In D. Mandrioli & B. Meyer (Eds.), Advances in object-oriented software engineering (pp.\u00a01\u201350). New York: Prentice Hall."},{"issue":"1","key":"9271_CR40","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1109\/TRA.2003.820849","volume":"20","author":"J. Minguez","year":"2004","unstructured":"Minguez, J., & Montano, L. (2004). Nearness diagram (ND) navigation: collision avoidance in troublesome scenarios. IEEE Transactions on Robotics and Automation, 20(1), 45\u201359.","journal-title":"IEEE Transactions on Robotics and Automation"},{"key":"9271_CR41","volume-title":"MISRA-C:2004\u2014guidelines for the use of the C language in critical systems","author":"MISRA","year":"2004","unstructured":"MISRA (2004). MISRA-C:2004\u2014guidelines for the use of the C language in critical systems. Nuneaton: Motor Industry Research Association (MIRA) Limited."},{"key":"9271_CR42","unstructured":"Nilsson, N. J. (1984). Shakey the robot. Tech. rep. 323, SRI International, Menlo Park, California."},{"key":"9271_CR43","series-title":"Isabelle\/HOL\u2014a proof assistant for higher-order logic","volume-title":"Lecture notes in computer science","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L. C., & Wenzel, M. (2002). Lecture notes in computer science: Vol.\u00a02283. Isabelle\/HOL\u2014a proof assistant for higher-order logic. Berlin: Springer."},{"key":"9271_CR44","volume-title":"Proceedings of the IEEE international conference on robotics and automation","author":"R. Parthasarathi","year":"2007","unstructured":"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."},{"key":"9271_CR45","volume-title":"Proceedings of the IEEE international conference on robotics and automation","author":"R. Philippsen","year":"2003","unstructured":"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."},{"key":"9271_CR46","series-title":"Formal methods","first-page":"547","volume-title":"Lecture notes in computer science","author":"A. Platzer","year":"2009","unstructured":"Platzer, A., & Clarke, E. M. (2009). Formal verification of curved flight collision avoidance maneuvers: a case study. In Lecture notes in computer science: Vol.\u00a05850. Formal methods (pp.\u00a0547\u2013562). Berlin: Springer."},{"key":"9271_CR47","first-page":"3597","volume-title":"Proceedings of the American control conference","author":"A. Puri","year":"1995","unstructured":"Puri, A., & Varaiya, P. (1995). Driving safely in smart cars. In Proceedings of the American control conference (Vol.\u00a05, pp. 3597\u20133599)."},{"key":"9271_CR48","doi-asserted-by":"crossref","first-page":"398","DOI":"10.1109\/IVS.2007.4290147","volume-title":"Proceedings of the IEEE intelligent vehicles symposium","author":"C. Rabe","year":"2007","unstructured":"Rabe, C., Franke, U., & Gehrig, S. (2007). Fast detection of moving objects in complex scenarios. In Proceedings of the IEEE intelligent vehicles symposium (pp.\u00a0398\u2013403)."},{"key":"9271_CR49","volume-title":"The theory and practice of concurrency","author":"A. W. Roscoe","year":"1998","unstructured":"Roscoe, A. W. (1998). The theory and practice of concurrency. New York: Prentice Hall."},{"key":"9271_CR50","unstructured":"RT-Tester (2006). User manual. Verified Systems International GmbH, http:\/\/www.verified.de\/en\/products\/rt-tester , retrieved Jan. 2011."},{"key":"9271_CR51","volume-title":"Proceedings of the IEEE\/RSJ international conference on intelligent robots and systems","author":"C. Schlegel","year":"1998","unstructured":"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."},{"key":"9271_CR52","volume-title":"1st national workshop on control architectures of robots: software approaches and issues CAR\u201906","author":"D. Simon","year":"2006","unstructured":"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\u201906, Montpellier, France."},{"key":"9271_CR53","volume-title":"Proceedings of the IEEE\/RSJ international conference on intelligent robots and systems (IROS)","author":"H. T\u00e4ubig","year":"2011","unstructured":"T\u00e4ubig, H., B\u00e4uml, 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."},{"issue":"2","key":"9271_CR54","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1109\/9.250509","volume":"38","author":"P. Varaiya","year":"1993","unstructured":"Varaiya, P. (1993). Smart cars on smart roads: problems of control. IEEE Transactions on Automatic Control, 38(2), 195\u2013207.","journal-title":"IEEE Transactions on Automatic Control"},{"issue":"12","key":"9271_CR55","doi-asserted-by":"crossref","first-page":"1005","DOI":"10.1177\/0278364903022012002","volume":"22","author":"A. C. Victorino","year":"2003","unstructured":"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\u20131118.","journal-title":"The International Journal of Robotics Research"},{"key":"9271_CR56","volume-title":"Handbuch Fahrerassistenzsysteme","year":"2009","unstructured":"Winner, H., Haskuli, S., & Wolf, G. (Eds.) (2009). Handbuch Fahrerassistenzsysteme. Berlin: Vieweg+Teubner (in German)."},{"key":"9271_CR57","series-title":"Hybrid systems: computation and control","first-page":"396","volume-title":"Lecture notes in computer science","author":"T. Wongpiromsarn","year":"2009","unstructured":"Wongpiromsarn, T., Mitra, S., Murray, R., & Lamperski, A. (2009). Periodically controlled hybrid systems. In Lecture notes in computer science: Vol.\u00a05469. Hybrid systems: computation and control (pp.\u00a0396\u2013410). Berlin: Springer."}],"container-title":["Autonomous Robots"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10514-011-9271-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10514-011-9271-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10514-011-9271-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T19:15:59Z","timestamp":1559157359000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10514-011-9271-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,12,22]]},"references-count":57,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2012,4]]}},"alternative-id":["9271"],"URL":"https:\/\/doi.org\/10.1007\/s10514-011-9271-y","relation":{},"ISSN":["0929-5593","1573-7527"],"issn-type":[{"value":"0929-5593","type":"print"},{"value":"1573-7527","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,12,22]]}}}