When Code Can't Have Errors

 
Jan 09, 2006

by Judith Dinowitz

There are some systems (like those at aircraft control towers or missile launching systems) where software bugs are things you simply can't afford. The September 2005 issue of Spectrum gives a nice overview of Praxis, a company based in Bath, England, that has developed a methodology called Correctness by Construction (CbyC). According to two engineers from Praxis (who wrote up this methodology in Crosstalk, the Journal of Defense Software Engineering), CbyC helps to "deliver software with defect rates an order of magnitude lower than current best commercial practices in a cost-effective manner, and to deliver durable software that is resilient to change throughout its life cycle." In the Crosstalk article, they claim that CbyC has delivered code with less than 0.1 defects/1,000 source lines of code (SLOC) with good productivity of up to around 30 lines of code (LOC) per day. While 30 lines of code may not seem like a lot, we have no idea what they're actually writing it in, and how they're measuring those thirty lines of code. For all we know, they could have written much more code per day, but 30 lines were deemed to be acceptable and ready to go to the client. Also, consider the low error rate they're citing!

The CbyC methodology uses mathematically based techniques known as formal methods. Basically, the programmers at Praxis (and other companies that use these formal methods) string together special symbols that represent the program's logic before they write any code. They can check these symbol strings (like a mathematician would check a mathematical theorum) to verify that they form logically correct statements, thereby discovering any logical errors in their program before they start.

This CbyC approach reminds me of the top-down design articles we've been doing on Test Driven Development. In both cases, the end result is calculated before the program is written, and the premise (or the code, in the case of TDD), is tested prior to or during development. The articles in Spectrum and Crosstalk are well-written and worth your time.

The Exterminators (Spectrum, September 2005)

Correctness by Construction: A Manifesto for High-Integrity Software (Crosstalk, December 2005)

Add a Comment
(If you subscribe, any new posts to this thread will be sent to your email address.)
  
Privacy | FAQ | Site Map | About | Guidelines | Contact | Advertising | What is ColdFusion?
House of Fusion | ColdFusion Jobs | Blog of Fusion | AHP Hosting