From: David Crocker (dcrocker(at)eschertech.com)
Date: Tue 29 Oct 2002 - 00:24:39 GMT
Roger & list, We did some investigation into the issue of correctness of programs involving floating point operations when we came to design the floating point model in our formal methods product (Perfect Developer). We came to the conclusion that for very simple systems, we can track the error bound in the formal model; but for anything more complicated (e.g. matrix inversion), numerical analysis has to be used to determine the error bound, because the formal model gives a worst-case error bound far worse than reality (and too bad to be of any use in practice). We are hoping in the future to do some research in conjunction with an organisation having numerical methods expertise, so that we can add a more comprehensive treatment of floatng point maths to our product. For now we support a very simple floating point model that is correct but of limited use (e.g. we don't assume addition is associative, because it isn't when working to a finite precision). I don't see much problem in using the hardware floating point unit of a popular processor rather than libraries, providing one avoids very recent processors (or new steppings of processors), since the bugs in a popular processor tend to be found quite quickly (and quality management has doubtless been tightened up since the Pentium FDIV bug, including I believe the introduction of formal methods). In this respect I would generally trust hardware more than software (unless then software is very mature and well-understood), since hardware manufacturers have a much greater financial incentive to get it right first time. Naturally, one should seek evidence of correctness. David Crocker Escher Technologies Ltd. www.eschertech.com -----Original Message----- From: safety-critical-request(at)cs.york.ac.uk [mailto:safety-critical-request(at)cs.york.ac.uk]On Behalf Of Rivett, Roger (R.S.) Sent: 28 October 2002 17:33 To: 'safety-critical(at)cs.york.ac.uk' Subject: [sc] Use of floating point arithmetic in embedded control software Dear list members We have been having a debate within my department as to the appropriateness, or otherwise, of using floating arithmetic if the target microprocessor has a hardware floating point unit allowing the use of software libraries to be banned. I thought this is just the sort of topic to stir a quiescent mailing list into life.