Weitere Kapitel dieses Buchs durch Wischen aufrufen
Floating-point subtleties are often overlooked by software developers, but they can have considerable impact over critical systems which make extensive manipulations of real numbers. This work presents a method for detecting floating-point absorption and cancellation when performing variable range analysis in design models. Employing this method as early as in the design phase permits cheaper detection and treatment of such floating-point anomalies. Our method works by analyzing sums and subtractions in a model and verifying if, given two variable ranges, there are sub-ranges of them on which absorption and cancellation can occur. We also provide the number of canceled bits for each sub-range in order to permit better assessment of the impact of each detected cancellation. We implemented our method in a range analysis tool that operates over SCADE models: results are presented in an HTML report and cancellations are depicted in graphs. This method can be used for early design analysis or as a basis for more complex, end-to-end numerical precision verification.
Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten
Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:
IEEE Computer Society (2008). IEEE standard for floating-point arithmetic. New York: Institute of Electrical and Electronics Engineers.
Carlone, R. V. (1992). Patriot Missile Defense: Software problem led to system failure at Dhahran, Saudi Arabia (GAO/IMTEC-92-26), U.S. Government Accountability Office, Technical report.
DO-178C (2011). Software considerations in airborne systems and equipment certification. Washington, DC: Radio Technical Commission for Aeronautics (RTCA).
International Electrotechnical Commission (2010). Functional safety of electrical/electronic/programmable electronic safety-related systems – Part 3: Software requirements. Geneva: International Electrotechnical Commission (IEC).
Honda, R. M., & Dias, L. A. V. (2013). Rangeanalyzer: An automatic tool for arithmetic overflow detection in model-based development. In ITNG 2013, Las Vegas (pp. 254–259).
Goldberg, D. (1991). What every computer scientist should know about floating-point arithmetic. ACM Computing Surveys, 23(1), 5–48. [Online] Available: http://doi.acm.org/10.1145/103162.103163
Cheney, E. W., & Kincaid, D. (2012). Numerical mathematics and computing (7th ed.). Boston: Brooks/Cole Publishing Co.
Delmas, D., Goubault, E., Putot, S., Souyris, J., Tekkal, K., & Védrine, F. (2009). Towards an industrial use of FLUCTUAT on safety-critical avionics software. In M. Alpuente, B. Cook, & C. Joubert (Eds.), Formal methods for industrial critical systems (Lecture notes in computer science, Vol. 5825, ch. 6, pp. 53–69). Berlin/Heidelberg: Springer. [Online] Available: http://dx.doi.org/10.1007/978-3-642-04570-7_6
Benz, F., Hildebrandt, A., & Hack, S. (2012). A dynamic program analysis to find floating-point accuracy problems. In Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI’12 (pp. 453–462). New York, NY: ACM. CrossRef
Lam, M. O. (2014). Automated floating-point precision analysis. Ph.D. dissertation, University of Maryland, College Park.
Ramachandran, J., Pasareanu, C. S., & Wahl, T. (2015). Symbolic execution for checking the accuracy of floating-point programs. ACM SIGSOFT Software Engineering Notes, 40(1), 1–5. CrossRef
Harrison, J. (2006). Floating-point verification using theorem proving. In M. Bernardo & A. Cimatti (Eds.), Formal Methods for Hardware Verification, 6th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (Lecture notes in computer science, Vol. 3965, pp. 211–242). Bertinoro: Springer.
Bao, T., & Zhang, X. (2013). On-the-fly detection of instability problems in floating-point program execution. In Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA’13 (pp. 817–832). New York, NY: ACM. [Online] Available: http://doi.acm.org/10.1145/2509136.2509526
Rubio-González, C., Nguyen, C., Nguyen, H. D., Demmel, J., Kahan, W., Sen, K., Bailey, D. H., Iancu, C., & Hough, D. (2013). Precimonious: Tuning assistant for floating-point precision. In Proceedings of the International Conference on High Performance Computing, Networking, Storage and Analysis, SC’13 (pp. 27:1–27:12). New York: ACM. [Online] Available: http://doi.acm.org/10.1145/2503210.2503296
Press, W. H., Teukolsky, S. A., Vetterling, W. T., & Flannery, B. P. (1992). Numerical recipes in C: The art of scientific computing (2nd ed.). New York: Cambridge University Press. MATH
- Enhancing Range Analysis in Software Design Models by Detecting Floating-Point Absorption and Cancellation
Marcus Kimura Lopes
Ricardo Bedin França
Luiz Alberto Vieira Dias
Adilson Marques da Cunha
Neuer Inhalt/© ITandMEDIA