When Bugs Aren't Allowed 489
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."
2 defacto models of software development (Score:5, Informative)
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.
Re:Whatever (Score:4, Informative)
I was pitching for "how people would like to think things are" rather than how things actually work. In practice Praxis, at least, does deliver such software, and does so with extremely low defect rates. They are proof that it can be done, even if it isn't always how things work now.
Jedidiah.
Re:Still can have bugs (Score:5, Informative)
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.
Re:Bugs and Beta testing. (Score:3, Informative)
Re:Microsoft error rates (Score:3, Informative)
You say that like it's a good thing!
The only way Windows will be fixed is to start with a clean sheet of paper, completely re-write the entire code base. There are errors in XP that were unfixed errors in 98. I've seen 2 errors in XP that were identical to ones in 3.1. That is a lack of attention to detail.
My Bogosity meter is wiggling (Score:4, Informative)
Re:productivity around 30 LOC per day (Score:5, Informative)
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 [slashdot.org] 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.
Re:The right programming language helps hugely (Score:5, Informative)
If you find that interesting, but Ada isn't to your taste, you can try JML [iastate.edu] 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 [ed.ac.uk] and HasCASL [uni-bremen.de] 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.
Re:Do you think it would help? (Score:2, Informative)
http://wired-vig.wired.com/news/technology/0,1282
Or air traffic controllers:
http://www.techworld.com/opsys/news/index.cfm?New
Or nuclear power plants:
http://www.securityfocus.com/news/6767 [securityfocus.com]
Regardless of how you rate the intelligence of the parties involved in these little incidents I think you'll find that Windows is very often deployed in mission critical areas.
And yes, often with catastrophic consequences. >)
Re:The right programming language helps hugely (Score:4, Informative)
Yesterday, I had to do an analysis for someone on whether eliminating the electoral college would hurt states with a low turnout or not. The data is online in a nice plain text table, and the calculations are dirt-simple and take under a second in whatever language you want. Gawk all the way, got the project done in half an hour, if I had used C or Java I'd probably have spent triple the time for the same results. Several months ago I had to do image processing with a GUI wrapped around it -- C for the number crunching, .NET something or other for the GUI. A year ago I had to write a distributed application to do some crazy intense number crunching -- wrote the number crunching loop in C*, wrote the network code and interface in Java.
* Credit where credit is due: I borrowed 99.95% of it from GPLed code designed to do the same task on a single machine.
Re:nearly unlimited funding (Score:5, Informative)
Jedidiah.
Nearly unlimited risk helps too-Theorem. (Score:4, Informative)
http://www.edn.com/archives/1995/080395/16df4.htm [edn.com]
"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
Re:Here, here... (Score:3, Informative)
It sounds apocryphal, but I really want it to be true. :-)
It really is true, but it happened in a simulator [66.102.7.104].
Re:I have to wonder.... (Score:4, Informative)
And why are softwares so buggy and have such a lousy reputation anyway? Not to start a flamewar, but let's just list a few possible "reaons" here:
I think, to be honest, that it is a combination of a number of the factors you mention.
Why aren't schools teaching this methodoly thoroughly? Why aren't this toolset and programming language taught in school by default?
To do proper formal specification, one of the key parts of Praxis' Correct by Construction approach, does require a decent solid mathematical background. I think a lot of CS departments, facing students who want vocational training, struggle to demand the sort of mathematical requirements that are needed. As to SPARK - it is something that Praxis developed themselves, and it is proprietary (the toolset at least, the annotation language is well documented). You can pick up a book and learn the language, but the tools cost money if you want to use them commercially. On the other hand, the base specification language Praxis uses, Z [wikipedia.org], is entirely open, and there are a variety of freely available tools for it [sourceforge.net]. There are also other specification langauges (I quite like CASL [wikipedia.org] which has a number of useful extensions) that have freely available tools associated with them. There's also JML [iastate.edu] and ESC/Java2 [secure.ucd.ie] which are freely available and seek to provide the same sort of functionality or Java that SPARK adds to Ada. There are places that teach JML [uni-bremen.de], but they are still few and far between.
Programmers are asked to do the impossible.
I think this is a big part of it in some ways. Partly this is because, for a large number of software projects, the degree of exactness and quality just isn't required. I don't need a professional architect to help me build a doghouse in my backyard (though I'd certainly want one if I was building a skyscraper), and I don't need assurances of bug free software for a simple web front-end to a database. At the same time programmers are often unwilling to let customers know exactly what the limits are when developing software. To quote you: "If a customer dares to ask a civil engineer to add 2 more stories between the 3rd and 4th floor after the custom-built building is finished, guess what would the civil engineer say?"; if software engineers aren't prepared to stand up for quality and tell customers that somethings can't be done without sacrificing the quality of the product the problem will remain. In part I think this is due to the fact that software development is a young industry, and programmers are still of the mentality that they need to do everything they possibly can to please a customer. Partly it's because software projects are diverse (as are building projects!) and sometimes it's okay to make late changes; sometimes it's how things ought to be done - the key is to identify exactly what sort of project it is as early as you can. Are you building a treehouse for your kids, which doesn't require exactness and benefits from incremental design and feedback, or are you building a 4 story building where quality is important, and late changes will jepordise that?
Programmers are a bunch of bozos who know shit about proper engineering.
Sadly this is partly the case. There are an awful lot of cowboys out there when it comes to software engineering. There are, of course, a lot of fantastic programmers as well who are otherwise beset by some of the other points mentioned. There is, however, a remarkable degree of tolerance for cowboys, sloppiness and lack of quality in software engineering that you don't see in other engineering disciplines. Partly I thin
Re:Bugs and Beta testing. (Score:3, Informative)
However, fingerprints are not an entirely genetic characteristic. Scientists love to use this topic as an example of the old "nature vs. nurture" debate. Fingerprinting, along with other physical characteristics, is an example of a phenotype -- meaning that it is determined by the interaction of an indivdual's genes and the developmental environment in the uterus.
The ultimate shape of fingerprints are believed to be influenced by environmental factors during pregnancy, like nutrition, blood pressure, position in the womb and the growth rate of the fingers at the end of the first trimester. Thus, you will find similar partterns of whorls and ridges in the fingerprints of identical twins. But there will also be differences -- just as there are differences between the fingers on any individual's hands.
Taken from about.com [about.com]