Scientists Tout New Way To Debug Surgical Bots

coondoggie writes "When it comes to having robotic surgeons slicing around inside your brain, heart or other important body organ, surgeons and patients need to know that a software or hardware glitch isn't going to ruin their day. That's why a new technique developed by researchers at Carnegie Mellon University and the Johns Hopkins University Applied Physics Laboratory that promises to reliably detect software bugs and verify the software safety of surgical robots could be a significant development."

Comments

Free surgery?

[techsimian]

I guess it's really a public beta...

For real safety

[fustakrakich]

Do not connect these things to the internet, please.

ruin their day ?

[middlemen]

This is typical "doctor" talk. They are worried about ruining their day or malpractice suits. How about for a change think about not ruining a patient's life with your negligence !

Re:ruin their day ?

[Anonymous Coward]

This is what you get with a market-based approach to healthcare.

Re:ruin their day ?

[ColdWetDog]

If the doctor doesn't ruin your life, then you don't get to ruin his day. Works for both 'concerns'.

Not that I'm sure the touted system will work as planned (it never does) but trying to minimize bad outcomes is sort of the whole point to improving medical practice.

It's not just BMWs and trophy wives.

Re:ruin their day ?

[Anonymous Coward]

No, this is what you get with a market-based approach to healthcare coupled with a government-granted monopoly in the form of ridiculous licensing laws.

If you increased the competition these people face, they wouldn't be so smug anymore.

How to debug a surgical bot?

[jamesl]

Just run it through the autoclave.

Can detect buggy software?

[Zerth]

wow, does it solve the halting problem as well?

Re:Can detect buggy software?

[Jane Q. Public]

"wow, does it solve the halting problem as well?"

Pretty close to my thoughts as well.

Reliably finding all "bugs" is not possible without an intimate knowledge of exactly what the software is trying to accomplish. You can find certain kinds of errors algorithmically (what amount to "compile time" errors), and even prevent many kinds of run-time errors.

But there is simply no way to prevent the program from doing something unintentional (like cutting the wrong thing) without prior detailed knowledge of the actual intent.

Re:Can detect buggy software?

[jeffasselin]

It's doable to ensure a program does exactly what its specs say it should do. See http://en.wikipedia.org/wiki/Formal_verification.

It's not often done because it's extraordinarily time-consuming; the time it takes to do goes up exponentially with program length/complexity, I believe.

Re:Can detect buggy software?

[radtea]

But there is simply no way to prevent the program from doing something unintentional (like cutting the wrong thing) without prior detailed knowledge of the actual intent.

Back in the '80's David Parnas argued that software verification was fundamentally different from hardware verification precisely because software has very nearly infinite bandwidth, which is precisely the opposite of the argument being made in the article.

That is, for hardware, a small change in some parameter will in almost all practical cases result in behaviour that is not wildly different from the behaviour with the original value. This means that we can test it under a finite set of conditions and smoothly extrapolate to the rest.

With software, a single bit flipped can result in behaviour that is arbitrarily different from the original behaviour. As such, nothing short of exhaustive testing over all possible accessible states can prove software correct.

Algorithmic testing of the kind described here will catch some bugs, but provably correct algorithms can still run into practical implementation details that will result in arbitrarily large deviations from ideal behaviour. For example: the inertial navigation module on the Ariane V could have had provably correct code (for all I know it actually did) and the rocket still would have destroyed itself.

Most problems with embedded systems are of the kind, "The hardware did something unexpected and the software responded by doing something inappropriate." Anticipating the things the (incorrectly assembled, failure-prone, unexpectedly capable) hardware might do and figuring out what the appropriate response is constitutes the greater part of building robust embedded code, and this kind of verificationist approach, while useful as a starting point, won't address those issues at all.

This new technique...

[QuietLagoon]

... will lead to sloppy software being written. Why write high-quality software when you know any bugs will be caught later on?

Re:This new technique...

[DamnStupidElf]

The proof verifier won't verify sloppy software without a proof of correctness. It's much harder to write a formal proof of correctness for sloppy code, so anything that can pass the verification stage will most likely be well written, simple, and very human readable since a human has to read and understand it sufficiently to write the formal proof of correctness for it. Writing the formal proofs will also probably be the largest part of the workload in the software development process so it makes no sense to write sloppy code when the cost will be magnified during the verification stage.

Misleading summary

[MasseKid]

This debugs the algorithm, not the software, nor the hardware used. There is an enormous difference.

Re:Yes, can detect buggy software.

[Animats]

wow, does it solve the halting problem as well?

That's not insightful, it's clueless about the subject.The halting problem is very rarely a problem in program verification. It's possible to write a program for which halting is undecidable. That's a bug in the program.

The Microsoft Static Driver Verifier, in practice, runs into problems it can't decide about 5% of the time. The goal is to determine that the driver is memory-safe to be in the kernel and calls all the driver APIs with valid parameters. If it does that, the driver can't crash the rest of the OS, and any problems it has are confined to its own device. The Static Driver Verifier tries to either find a case that will crash or prove that a crash can't happen. The 5% of cases the Verifier can't decide are considered bugs. Really, if it's that hard to decide if a driver can cause a crash, the driver is broken.

I'm not sure how sound this new verification system is. There's been a lot of progress in this area in the last 30 years, since I worked on it. Formal verification is widely used in IC design, where "patch and release" doesn't work. The software world isn't as aware of the technology.

The halting problem is practically solved.

[ebiederm]

In the general case it is true that you can not tell if an program will halt. However most programs do halt and most programmers understand why. Theorem provers present a language to their users that does not admit the general case in which halting is guaranteed which is part of a more important guarantee that all programs can be reduced to a normal form.

Which means that the halting problem is solved for a program written in a language like coq.

The practical challenge seems to be that formal detailed requirements and specifications for algorithms are about as hard to write as the algorithms themselves.

undo mod

[necro81]

posting to undo an accidental moderation

Wonder how they do it

[TheSkepticalOptimist]

bool DidBrainBotOperateSuccessfullyOn(Patient patient)
{
          if ( patient != null && patient.IsVegetable && !patient.WasVegetable )
                    throw new PendingLawsuitException(patient.Lawyer, Doctor.Lawyers, Hospital.Lawyers, University.Lawyers, Manufacturer.Lawyers);
          return true;
}