News

Aug 13, 2009

Bug-free computer software: Australia paves the way

A computer crash and reboot will hopefully soon be a thing of the past, thanks to new Australian research on microkernels and bug free computer systems.

Stilgherrian — Technology writer and broadcaster

Stilgherrian

Technology writer and broadcaster

A computer crash and reboot are frustrating enough, but even more so when it’s an embedded system running a surgical robot, a weapons system or a self-driving car. Waste time rebooting and you could be dead.

5 comments

Leave a comment

5 thoughts on “Bug-free computer software: Australia paves the way

  1. Stilgherrian

    Before anyone else says it, yes, I do know that not all operating systems have a microkernel. But, like, how much Deep Geek can people cope with?

  2. Evan Beaver

    I know nothing about this at all, but suspect some hard maths has gone down. Very interesting stuff; I can cope with more nerdiness.

  3. Barry Brannan

    Presumably to get to the point of being able to prove that a program implements its specification correctly, one needs to go through extensive testing and debugging. The question would be how much time and effort one wants to devote to that task before releasing a program. Current practices show that there is a limit – a certain level of defects is accepted, especially with time pressures and commercial pressures.

    This research may have its uses and I’m curious to know how easy it is to re-prove correctness after a change in specifications or implementation.

    Certainly won’t result in bug-free software though.

  4. Barry Brannan

    Another problem with this approach is that it moves complexity from the implementation to the specification. I’d be interested in seeing what their formal specifications look like. If, as they say, a specification defines “what” something should do rather than the “how” it does it, it might be marginally better than the implementation. However, for a specification to fully define a problem I expect it would still be almost as complex.

    If they have done what they say they have done then essentially we should be able to get a new programming language – the one used for the formal specification.

  5. Stilgherrian

    @Barry Brannan: Some good points and questions there. I’ll do some more digging.

    Part of the point of a formal proof is that you wouldn’t need as much testing because, well, you’ve proved that it does what it was specified to do Yes, that does mean the specification needs to be in a formal language too, not just hand-waving manager-speak. Specification languages look kinda like programming languages — and there are many in existence already, though I daresay most working programmers never use them and may not even know they exist.

    Yes, formal methods are a lot more work — at least until this NICTA work came along. My understanding is that all this dramatically changes the relative effort involved in formal methods, which in turn means they can be used in places where they’d previously have been too expensive.

Share this article with a friend

Just fill out the fields below and we'll send your friend a link to this article along with a message from you.

Your details

Your friend's details

Sending...