3 ms·

Think of it as a double checking your code. If you had a bug per 100 LOCs you can reduce that to a bug per 1000-10000 LOCs. Which is achievable with other metho

by zzzcpan 10y ago

Think of it as a double checking your code. If you had a bug per 100 LOCs you can reduce that to a bug per 1000-10000 LOCs. Which is achievable with other methods too, without the burden of formal verification.

philipkglass 10y ago
Are the other methods for reducing errors to one bug per 10000 LOCs measured to be less burdensome? I've read with interest about how Jet Propulsion Laboratory produces code with low defect rates for spacecraft (without formal verification), but it appears to be a pretty drastic departure from ordinary commercial practice too.
- nickpsecurity 10y ago
  I know of at least three: Hamilton's 001 Tool Suite http://htius.com/ http://htius.com/ Cleanroom Software Methodology http://infohost.nmt.edu/~al/cseet-paper.html http://infohost.nmt.edu/~al/cseet-paper.html Praxis Correct-by-Construction http://www.anthonyhall.org/c_by_c_secure_system.pdf http://www.anthonyhall.org/c_by_c_secure_system.pdf All three have some upfront time in specification with Praxis doing refinements, too. However, they all knock out tons of debugging and integration problems since errors don't slip in at all. Altran/Praxis charges 50% premium on top of normal contract so the extra labor is probably less than 50% given they're profitable. Cleanroom anecdotes showed the reduced debugging and maintenance issues meant it actually barely cost anything extra in time or money. A few outliers had it saving time. There's also a number of people and companies that are encoding business logic into specs that they implement with logic programming languages. This eliminates mismatch between business requirements and code with quite a bit of productivity and safety advantages if it works in one's use-case. I haven't evaluated their effectiveness but here's two: http://www.missioncriticalit.com/technology.html http://www.missioncriticalit.com/technology.html https://dtai.cs.kuleuven.be/CHR/files/Elston_SecuritEase.pdf https://dtai.cs.kuleuven.be/CHR/files/Elston_SecuritEase.pdf

by zzzcpan 10y ago

philipkglass 10y ago

Are the other methods for reducing errors to one bug per 10000 LOCs measured to be less burdensome? I've read with interest about how Jet Propulsion Laboratory produces code with low defect rates for spacecraft (without formal verification), but it appears to be a pretty drastic departure from ordinary commercial practice too.

nickpsecurity 10y ago
I know of at least three: Hamilton's 001 Tool Suite http://htius.com/ http://htius.com/ Cleanroom Software Methodology http://infohost.nmt.edu/~al/cseet-paper.html http://infohost.nmt.edu/~al/cseet-paper.html Praxis Correct-by-Construction http://www.anthonyhall.org/c_by_c_secure_system.pdf http://www.anthonyhall.org/c_by_c_secure_system.pdf All three have some upfront time in specification with Praxis doing refinements, too. However, they all knock out tons of debugging and integration problems since errors don't slip in at all. Altran/Praxis charges 50% premium on top of normal contract so the extra labor is probably less than 50% given they're profitable. Cleanroom anecdotes showed the reduced debugging and maintenance issues meant it actually barely cost anything extra in time or money. A few outliers had it saving time. There's also a number of people and companies that are encoding business logic into specs that they implement with logic programming languages. This eliminates mismatch between business requirements and code with quite a bit of productivity and safety advantages if it works in one's use-case. I haven't evaluated their effectiveness but here's two: http://www.missioncriticalit.com/technology.html http://www.missioncriticalit.com/technology.html https://dtai.cs.kuleuven.be/CHR/files/Elston_SecuritEase.pdf https://dtai.cs.kuleuven.be/CHR/files/Elston_SecuritEase.pdf