کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
434130 | 1441664 | 2014 | 18 صفحه PDF | دانلود رایگان |
• We analyze a critical C code involving floating-point computations.
• The code is dealing with rotations represented by quaternions.
• A functional requirement is given, about the norms of quaternions involved.
• We express the requirement in a formal specification language.
• Code is verified with respect to the specification using theorem proving.
We report a case study that was conducted as part of an industrial research project on static analysis of critical C code. The example program considered in this paper is an excerpt of an industrial code, only slightly modified for confidentiality reasons, involving floating-point computations. The objective was to establish a property on the functional behavior of this code, taking into account rounding errors made during computations. The property is formalized using ACSL, the behavioral specification language available inside the Frama-C environment, and it is verified by automated theorem proving.
Journal: Science of Computer Programming - Volume 96, Part 3, 15 December 2014, Pages 279–296