Slashdot Mirror
When Bugs Aren't Allowed
Coryoth writes "When you're writing software for an air traffic control system, military avionics software, or an authentication system for the NSA, the delivered code can't afford to have bugs. Praxis High Integrity Systems, who were the feature of a recent IEEE article, write exactly that kind of software. In "Correctness by Construction: A Manifesto for High-Integrity Software" developers from Praxis discuss their development method, explaining how they manage such a low defect rate, and how they can still maintain very high developer productivity rates using a more agile development method than the rigid processes usually associated with high-integrity software development."
In the world of software development, there have come to be two defacto models.
1. Get the software out the door ASAP - quite simply, bang out code as fast as possible that meets a loosely defined specification. Then once the product is adopted, parachute help in like no tomorrow to steadily improve the product.
2. Engineer the software - not as a simple as it sounds. This requires that a specification be drawn. A plan be prepared. A team of solid engineers formed and lead by a competent manager. Then, throughout the entire development cycle, test and debug code.
My company does the latter and to do date we have retained 100% of our customers. I'm shocked by the number of developers that approach our company for jobs that don't have the first clue about how to even write a test harness, let alone do any real debugging. Then again, they don't teach much of that stuff in school and it seems that unless your role was specifically in testing at a previous job, that you're not going to have too much experience in that area. Its economics and marketing that put the bugs in software, not computer science.
If you can prove through solid design and input and output types that the program wont lose control then your set. Its buffer overflows and flawed design that has not been tested with every concievable input/output that causes most serious bugs in medical and aerospace applications.
Praxis uses a subset of Ada together with annotations in a language called SPARK to write most of their software. They also have tools which work with such code to do considerable static checking - much as type checking catches errors, checking the annotations catches many more just as efficiently - and generate proof obligations, which they can then formally prove. That means, for many of their projects, the actaully have formal proofs that buffer overflows cannot and will not occur.
However in practice this challenge is a little unpractical when deadlines and interopability with closed source software get in the way.
Again, this is where the tools and methodology matter. Praxis delivers code as fast as traditional development techniques, so deadlines aren't the problem. They can do this by using SPARKAda and the SPARK tools to do exceptionally robust testing on a regular basis for each incremental deliverable. This allows catching bugs much earlier, when they are cheaper and faster to fix.
The only method I have seen with almost perfect reliability is where the inputs and outputs are overloaded to handle any datatype and can be proven mathamatically not to crash. I guess a CS degree is still usefull.
It is pretty much this sort of mathematical rigor, injected into the development process as early as possible, that allows Praxis to produce the sort of defect rates that they do. And yes, that does mean that developers at Praxis are probably required to have stronger math and CS backgrounds that elsewhere. Given that, due to their ability to deliver almost bug free software in very reasonable time frames, Praxis charges 50% more than the industry daily rate, yes having a math or CS degree really does count for something - more money for starters.
Jedidiah.
Craft Beer Programming T-shirts
I have some beef to pick with the article: 1. It alleges that CMM5 organizations have about 1 defect/KLOC. Having worked and knowing such organizations, I can anecdotally confirm numbers like these are fiction. CMM5 certification has more to do with greasing palms rather than any absolute defect measurement. 2. A defect rate of 0.04bugs/KLOC is not zero bugs/KLOC. The difference is infinite in magnitude if that single bug is -- kills the user. 3. Low defect rates are more often a product of poor testing, not superior development.
Their claims of massive error reduction are, at best, anecdotal. Let's see them do this after taking over a half-coded project with minimal design requirements, a hard deadline, and a budget that can be cut by governmental forces at will.
Their claims of error reduction are based on the development method and a lot of the important stuff happens very early on, taking over a half finished project that failed to follow such a method is of course not going to work. They can't make existing code bug free, but they can write new code that has vastly less errors than most software. As to hard deadlines and budgets - as far as I am aware Praxis already works with deadlines, and apparently their project for Mastercard was done on a fixed flat fee, so working with fixed or limited budgets doesn't appear to be an issue either.
Jedidiah.
Craft Beer Programming T-shirts
Praxis uses SPARK Ada, which is a subset of the Ada programming language and annotations that provide for extended static checking, and theorem proving. You can find more about SPARK at the Praxis website, or the Wikipedia article isn't too bad. It's a very nice language, and has fantastic tool support.
If you find that interesting, but Ada isn't to your taste, you can try JML for Java which provides similar (but lacking quite the same robustness and tool support) annotations. JML lets you automatically generate JUnit tests based on your annotations, and with ESC/Java2 allows for extended static checking.
If, as you appear, you are more of a fan of functional languages then I'd suggest you check out Extended ML and HasCASL which provide similar sorts of formal specification capabilities for ML and Haskell. Tool support for these is still a little limited, but they are both quite powerful and provide very expressive specification syntax.
Jedidiah.
Craft Beer Programming T-shirts
Yes, small teams help, but I think it really is worth taking a look at the tools and methods that Praxis uses because there are some remarkably good ideas in there. Take a look at SPARK Ada - the Wikipedia article has some basic examples, and Praxis provides sample chapters of a book on SPARK for download. Seriously, take a little time out of your day, sit down, and read a little about how they do what they do. There really are good ideas that go well beyond just "small teams" if you want to deliver correctly functioning code.
Jedidiah.
Craft Beer Programming T-shirts
"If you want to learn it you gotta either go to the original research articles from the 70s."
r ial/nEET.pdf
r ial/slidesAppC.pdf
http://www.edn.com/archives/1995/080395/16df4.htm
"The extra element theorem is used for analog circuitry. The gist of it is that you remove the reactive elements ( or dependant sources ) from a circuit and then put them back in through a process of correction factors."
[n-extra element theorem]
http://ece-www.colorado.edu/~ecen5807/course_mate
[Middlebrook's extra element theorem]
http://ece-www.colorado.edu/~ecen5807/course_mate