Slashdot Mirror
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."
I guess it's really a public beta...
Do not connect these things to the internet, please.
“He’s not deformed, he’s just drunk!”
if you override all the safety settings and manually program abdominal surgery for a female patient on a machine only programmed for male patients, don't be surprised if your squidbabby isn't properly aborted.
also, who's liable if the bulb in the service light burns out right after the serviceman checks out the system?
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 !
Just run it through the autoclave.
wow, does it solve the halting problem as well?
... will lead to sloppy software being written. Why write high-quality software when you know any bugs will be caught later on?
what about your day?
For any software that has the possibility of creating harm to humans something like this should be norm.
"I believe it's called Test Driven Development. Thank yew..." - comic book guy
I wanted to read the article to find out information about the method, but there website ain't working. Too much traffic.
I believe that all people fall into one of two categories: either they can write good code or they can come up with clever names for things. Clearly this software was written by the former group.
This debugs the algorithm, not the software, nor the hardware used. There is an enormous difference.
This raises the idea that we need more solid systems both in software and hardware so no problems occur. Error-less is something we've yet to see, this is only the first of many reasons to develop a system which is both secure, real-time and without error. For industries with this type of demand.
Huey, Louie and Dewey, please report to the Medical Bay.
(I must have gotten the drone mfr/model from the novelization. I don't think it's ever mentioned in the movie.)
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.
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.
Your jamesl...like you say...Just run it through the autoclave.
posting to undo an accidental moderation
Am I the only one who read the title and laughed because of a Patton Oswalt joke?
Source: http://www.youtube.com/watch?v=qbai-yBRyHg
PS: I don't reply to ACs.
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;
}
I haven't thought of anything clever to put here, but then again most of you haven't either.
Who's debugging the debuggers?
The problem is to construct a control system such that the robot scalpel (controlled by a person by a force-feedback device) will not exit some pre-defined boundaries. E.g. boundaries that prevent the scalpel cutting a nerve. The preivous system was flawed as it didn't take into account delays in the reponse of the scalpel. By creating a more accurate model, and using methods that are able to prove things about the dynamic system, they prove that using their new control algorithm no matter what the human operator does, the scalpel will always remain in the boundaries.
It's not clear to me whether the lack of safety in the original control algorithm was a real problem. After all, it's not like the operation will be perfectly safe and a success as long as the scalpel never leaves the boundary. So it's not necessarily worth spending a huge amount of effort to go from "X happens with probability 1e-6" to "X never happens" if there are other more important risks.
The whole article is written with the notion of a total replacement debugging/designing solution for all software.
It is really dealing with mechanical and human motion behaviours like inertial overshoot, path avoidances and realistic feedback to the operator rather than things like buffer overruns, atomic accesses and race conditions.
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.
More accurately, this is a distinction between stateless and stateful systems. Stateless machines always perform the same operations. They makes them much easier to test than stateful systems whose behavior depends on memory of prior events.
Software is always stateful although it can approach stateless behavior. Analog electronics and mechanical systems are generally stateless. Digital systems can be built either way but registers and memories are pretty fundamental so almost all modern digital chips are stateful even if they don't embed cpu's and software.
The software world isn't as aware of the technology.
It's not "less aware of" so much as "this technology is less useful/more difficult to apply in the kind of complex semantic domains where software operates".
Hardware has very limited semantics compared to software: the number of distinct types on a chip is small compared to the number of distinct types in even a moderately complex application.
Each type of thing has its own set of behaviours that have to be encoded in the checking software. This encoding process has proven thus far to have very high difficulty, and every time you introduce a custom type you have to specify it in the language of the checking program.
None of this is to say that such work isn't making progress (particularly in the functional world) but that the problem in the hardware domain really is easier, so we should expect software to lag, relatively speaking.
Blasphemy is a human right. Blasphemophobia kills.
Let's stick these folks who believe in this verification technique underneath the robot as the first patients.
Just do some pointless surgery, open em up, and stitch them back up.
If they survive then trials on other people can start.