Abstract
We present a tool for the automatic generation of test stimuli for small numerical support functions, e.g., code for trigonometric functions, quaternions, filters, or table lookup. Our tool is based on KLEE to produce a set of test stimuli for full path coverage. We use a method of iterative deepening over abstractions to deal with floating-point values. During actual testing the stimuli exercise the code against a reference implementation. We illustrate our approach with results of experiments with low-level trigonometric functions, interpolation routines, and mathematical support functions from an open source UAS autopilot.
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
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Charette, R.: This car runs on code (2009), http://spectrum.ieee.org/green-tech/advanced-cars/this-car-runs-on-code
Intl. standard ISO 26262 Road Vehicles – functional safety 1st edn. (2011)
RTCA: DO-178C: Software considerations in airborne systems and equipment certification (2011)
Hart, J.F., Cheney, E.W., Lawson, C.L., Maehly, H.J., Mesztenyi, C.K., Rice, J.R., Thacher, J.H.G., Witzgall, C.: Computer Approximations. SIAM Series in Applied Mathematics. John Wiley and Sons (1968)
Cadar, C., Dunbar, D., Engler, D.R.: KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: 8th USENIX Symp. on Operating Systems Design and Implementation, OSDI, pp. 209–224 (2008)
Collingbourne, P., Cadar, D., Kelly, P.: Symbolic Crosschecking of Floating-Point and SIMD Code. In: EuroSys (2011)
IEEE standard 754 for floating-point arithmetic (2008)
Overton, M.L.: Numerical computing with IEEE floating point arithmetic - including one theorem, one rule of thumb, and 101 exercises. SIAM (2001)
Huckle, T., Schneider, S.A.: Numerische Methoden: Eine Einführung für Informatiker, Naturwissenschaftler, Ingenieure und Mathematiker. Springer (2006)
Giannakopoulou, D., Bushnell, D.H., Schumann, J., Erzberger, H., Heere, K.: Formal testing for separation assurance. Annals of Mathematics and Artificial Intelligence 63, 5–30 (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Schumann, J., Schneider, SA. (2014). Automated Testcase Generation for Numerical Support Functions in Embedded Systems. In: Badger, J.M., Rozier, K.Y. (eds) NASA Formal Methods. NFM 2014. Lecture Notes in Computer Science, vol 8430. Springer, Cham. https://doi.org/10.1007/978-3-319-06200-6_20
Download citation
DOI: https://doi.org/10.1007/978-3-319-06200-6_20
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-06199-3
Online ISBN: 978-3-319-06200-6
eBook Packages: Computer ScienceComputer Science (R0)