Abstract
Since underwater systems operate out of immediate reach, often autonomously, for extended periods of time, the correctness of both the software and hardware constituting these systems is of high concern. In this contribution, we review existing techniques to ensure the correctness of hardware and software using formal methods, and assess their applicability to underwater robotics. We identify several promising areas: system modelling, program verification and algorithm design for guaranteed efficiency and correctness (certifying algorithms).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
In the form above, not quite: what is lacking is the requirement that out is actually one of the points in ps.
References
Albers S (2010) Energy-efficient algorithms. Commun ACM 53(5):86–96
Alkassar E, Bohme S, Mehlhorn K, Schweitzer P (2011) An introduction to certifying algorithms. IT–Inf Technol 53:287–293
Bampis E, Kononov AV, Letsios D, Lucarelli G, Sviridenko M (2018) Energy-efficient scheduling and routing via randomized rounding. J Sched 21(1):35–51
Blum M, Kannan S (1995) Designing programs that check their work. J ACM 42(1):269–291
Bonifaci V, Chan H-L, Marchetti-Spaccamela A, Megow N (2012) Algorithms and complexity for periodic real-time scheduling. ACM Trans Algorithms 9:601–619
Bonifaci V, Marchetti-Spaccamela A, Megow N, Wiese A (2013) Polynomial-time exact schedulability tests for harmonic real-time tasks. In: Proceedings of RTSS. IEEE, pp 236–245
Chen L, Megow N, Rischke R, Stougie L (2015) Stochastic and robust scheduling in the cloud. In: Proceedings of APPROX, LIPIcs,vol 40. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, pp 175–186
Chen L, Megow N, Schewior K (2018) An \(\cal{O}(\log m)\)-competitive algorithm for online machine minimization. SIAM J Comput 47(6):2057–2077
Irani S, Pruhs K (2005) Algorithmic problems in power management. SIGACT News 36(2):63–76
Klein G (2010) The L4. Verified project: next steps. In: Proceedings of the third international conference on verified software: theories, tools, experiments, VSTTE’10. Springer, Berlin, pp 86–96
Koczor A, Matoga L, Penkala P, Pawlak A (2016) Verification approach based on emulation technology. In: International symposium on design and diagnostics of electronic circuits & systems (DDECS), pp 169–174
Kühne U, Beyer S, Bormann J, Barstow J (2010) Automated formal verification of processors based on architectural models. Form Methods Comput Aided Des 9:129–136
Le HM, Große D, Herdt V, Drechsler R (2013) Verifying System C using an intermediate verification language and symbolic simulation. In: Design automation conference, pp 116
LEDA (Library of Efficient Data Types and Algorithms). www.algorithmic-solutions.com
Leroy X (2009) Formal verification of a realistic compiler. Commun ACM 52(7):107–115
Lüth C, Ring M, Drechsler R (2017) Towards a methodology for self-verification. In: Khatri S (ed) 6th International conference on reliability, infocom technologies and optimization (ICRITO 2017)
Lüth C, Walter D (2009) Certifiable specification and verification of C programs. In: FM 2009: Formal methods, Lecture notes in computer science, vol 5350. Springer, pp 419–434
McConnell RM, Mehlhorn K, Näher S, Schweitzer P (2011) Certifying algorithms. Comput Sci Rev 5(2):119–161
Megow N, Mehlhorn K, Schweitzer P (2012) Online graph exploration: new results on old and new algorithms. Theor Comput Sci 463:62–72
Megow N, Skutella M, Verschae J, Wiese A (2016) The power of recourse for online MST and TSP. SIAM J Comput 45:859–880
Megow N, Uetz M, Vredeveld T (2006) Models and algorithms for stochastic online scheduling. Math Oper Res 31(3):513–525
Megow N, Verschae J (2018) Dual techniques for scheduling on a machine with varying speed. SIAM J Discret Math 32:1541–1571
Nipkow T, Paulson LC, Wenzel M (2002) Isabelle/HOL: a proof assistant for higher-order logic, vol 2283. Lecture notes in computer science. Springer
Ring M, Bornebusch F, Lüth C, Wille R, Drechsler R (2019) Better late than never: verification of embedded systems after deployment. In: Design, automation and test in Europe. Florence, Italy. IEEE
Smith D, Simpson K (2004) Functional safety, 2nd edn. Elsevier
Täubig H, Frese U, Hertzberg C, Lüth C, Mohr S, Vorobev E, Walter D (2012) Guaranteeing functional safety: design for provability and computer-aided verification. Auton Robot 32:303–331
Thrun S, Martin C, Liu Y, Hahnel D, Emery-Montemerlo R, Chakrabarti D, Burgard W (2004) A real-time expectation-maximization algorithm for acquiring multiplanar maps of indoor environments with mobile robots. IEEE Trans Robot Autom 20(3):433–443
Yao FF, Demers AJ, Shenker S (1995) A scheduling model for reduced CPU energy. In: Proceedings of the 36th annual symposium on foundations of computer science (FOCS 1995), pp 374–382
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Lüth, C., Megow, N., Drechsler, R., Frese, U. (2020). Verification for Autonomous Underwater Systems. In: Kirchner, F., Straube, S., Kühn, D., Hoyer, N. (eds) AI Technology for Underwater Robots. Intelligent Systems, Control and Automation: Science and Engineering, vol 96. Springer, Cham. https://doi.org/10.1007/978-3-030-30683-0_15
Download citation
DOI: https://doi.org/10.1007/978-3-030-30683-0_15
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-30682-3
Online ISBN: 978-3-030-30683-0
eBook Packages: Intelligent Technologies and RoboticsIntelligent Technologies and Robotics (R0)