(Press-News.org) PITTSBURGH—Surgical robots could make some types of surgery safer and more effective, but proving that the software controlling these machines works as intended is problematic. Researchers at Carnegie Mellon University and the Johns Hopkins University Applied Physics Laboratory have demonstrated that methods for reliably detecting software bugs and ultimately verifying software safety can be applied successfully to this breed of robot.
They used theorem-proving techniques to analyze a control algorithm for a research robot that would help a surgeon perform surgery at the base of the skull. Their method identified a safety flaw that could enable a scalpel or other surgical tool to go dangerously astray in this area, where the eye orbits, ear canals and major arteries and nerves are closely spaced and vulnerable to injury. It also guided development of a new algorithm and verified that the new controller was safe and reliable.
"These techniques are going to change how people build robotic surgery systems," predicted APL's Yanni Kouskoulas, who led the research study with André Platzer, assistant professor of computer science at Carnegie Mellon. Platzer and Kouskoulas say this formal verification technique also could change the way regulators evaluate new devices, providing more assurance of safety than is possible even with the most rigorous testing.
The researchers will present their findings April 11 at HSCC 2013, the Hybrid Systems: Computation and Control conference in Philadelphia. Other members of the study team were David Renshaw, a student in computer science at Carnegie Mellon, and Peter Kazanzides, associate research professor of computer science at Johns Hopkins.
Surgical robots are an example of a hybrid, or cyber-physical system — complex, computer-controlled devices that are becoming increasingly common. Other examples are aircraft collision avoidance systems, high-speed train controls and cars that avoid collisions, maintain their lanes or otherwise drive themselves.
"Because the consequences of these systems malfunctioning are so great, finding a way to prove they are free of design errors has been one of the most important and pressing challenges in computer science," Platzer said. Testing alone is inadequate because no test regimen can check all of the possible circumstances that the system might encounter.
A growing number of techniques have been developed to aid in formally verifying that computer hardware and software are free from design defects. These techniques analyze all the possible states of a system, much as a mathematician uses a proof to determine that a theorem is correct. But methods that work for computer circuitry or software, which may be complex but have a finite number of states, don't work for hybrid systems that must contend with the infinite variations of the physical world.
Platzer, however, has developed an approach based on differential dynamic logic and an associated tool called KeYmaeraD that can be used to model a hybrid system and its properties and then symbolically pick it apart. This approach, which Platzer already has used successfully to identify errors in aircraft collision avoidance systems and to verify the design of distributed car control systems, can verify that a design is safe or else help generate counterexamples of how the system can fail.
Platzer and his colleagues applied this approach to evaluate the control algorithm for the skull-base surgery robot. This robot aids in intricate surgery in small recesses of the brain by minimizing tiny movements as a surgeon manipulates a tool and by restricting the tool to movement within the surgical site. As the tool approaches the surgical boundary, beyond which healthy and vital tissues can be harmed, it exerts force feedback to warn the surgeon. If the tool reaches the boundary, the robot is supposed to stop it from going farther. This functionality is helpful for the surgeon, because the robot knows the delicate boundaries that the surgeon cannot necessarily see during the surgery.
Kouskoulas said the robot and the control algorithm were tested extensively, including on cadavers. "While it worked in the configurations in which it was tested, the fear was always that something unexpected could go wrong," he noted.
By using the formal verification method, the researchers showed that indeed something unexpected could occur in corners of the surgical site. They found that in some geometrical configurations, the safety feedback for one boundary would interfere with that of the adjoining boundary, canceling each other out and allowing the tool to be pushed beyond the limits set by the surgeon.
The tool generated examples of how this could occur. "It leads you to the problem," Kouskoulas explained. "You then have to be creative to find the solution." With that guidance, researchers were able to devise a new algorithm and use their method to prove it was safe.
"Medical robotics is an interesting problem area for hybrid systems," Platzer said. Existing certification procedures, which rely on trial-and-error testing, aren't appropriate for evaluating these software-intensive devices, he said. This study shows that formal verification methods can be applied successfully to medical robotics and that further development is warranted, he added.
###
The National Science Foundation supported this study.
About Carnegie Mellon University: Carnegie Mellon (http://www.cmu.edu) is a private, internationally ranked research university with programs in areas ranging from science, technology and business, to public policy, the humanities and the arts. More than 12,000 students in the university's seven schools and colleges benefit from a small student-to-faculty ratio and an education characterized by its focus on creating and implementing solutions for real problems, interdisciplinary collaboration and innovation. A global university, Carnegie Mellon's main campus in the United States is in Pittsburgh, Pa. It has campuses in California's Silicon Valley and Qatar, and programs in Africa, Asia, Australia, Europe and Mexico. The university is in the midst of "Inspire Innovation: The Campaign for Carnegie Mellon University," which aims to build its endowment, support faculty, students and innovative research, and enhance the physical campus with equipment and facility improvements.
The Applied Physics Laboratory, a not-for-profit division of The Johns Hopkins University located in Laurel, Md., meets critical national challenges through the innovative application of science and technology. For more information, visit http://www.jhuapl.edu.
END
We're all fatheads. That is, our brain cells are packed with fat molecules, more of them than almost any other cell type. Still, if the brain cells' fat content gets too high, they'll be in trouble. In a recent study in mice, researchers at Johns Hopkins pinpointed an enzyme that keeps neurons' fat levels under control, and may be implicated in human neurological diseases. Their findings are published in the May 2013 issue of Molecular and Cellular Biology.
"There are known connections between problems with how the body's cells process fats and neurodegenerative diseases ...
Antidiscrimination laws can have a significant positive impact on how gays and lesbians are treated in employment situations, according to new research from Rice University. The study on public awareness of sexual-orientation employment-antidiscrimination laws is one of the first to provide empirical evidence for the likely impact of pending antidiscrimination legislation.
"In many U.S. states and localities (including much of Texas), gays and lesbians remain unprotected from employment discrimination," said Laura Barron, a 2008 Rice alumna and now personnel research ...
Philadelphia, PA, April 8, 2013 – Although mammography, the gold standard of breast cancer screening, reduces breast cancer mortality, it has important limitations. Critics point to reduced sensitivity for women with dense breasts, a high rate of false positives leading to excessive biopsies, and concerns about long-term effects of repeated radiation. With greater understanding of risk stratification, the authors of this review envision a re-thinking of the typical breast cancer paradigm to include new technologies that allow a more individualized approach that integrates ...
Religious and nonreligious organizations may have a similar impact on the ability of immigrants to acclimate to life in the U.S., despite the organizations' different motivations for providing charitable services, according to new research from Rice University.
"There's been a lot of discussion as to whether religious organizations offer some special or unique benefit to immigrant groups that will help them better adapt to American society," said the study's lead author, Elaine Howard Ecklund, the Herbert S. Autrey Professor of Sociology and director of Rice's Religion ...
AUGUSTA, Ga. – The relationship between obesity and polycystic ovary syndrome may be exaggerated, likely because the women who actively seek care for the condition tend to be heavier than those identified through screening of the general population, researchers report.
PCOS affects about 10 percent of women and is characterized by excess male hormone, irregular ovulation and menstruation as well as increased risk of metabolic diseases often associated with being overweight.
The study in the Journal of Clinical Endocrinology & Metabolism looked at what have long been ...
Imagine a solar panel more efficient than today's best solar panels, but using 10 000 times less material. This is what EPFL researchers expect given recent findings on these tiny filaments called nanowires. Solar technology integrating nanowires could capture large quantities of light and produce energy with incredible efficiency at a much lower cost. This technology is possibly the future for powering microchips and the basis for a new generation of solar panels.
Despite their size, nanowires have tremendous potential for energy production. "These nanowires capture ...
Some species of birds reproduce not by rearing their own young, but by handing that task on to adults of other species. Known as brood parasitism, this habit has been most thoroughly researched in the cuckoo. Previous research has found, however, that the nests of martins and swallows in Europe are rarely parasitized by cuckoos. A new study by Wen Liang from the Hainan Normal University in China and his colleagues suggests that swallows build their nests close to humans to reduce their susceptibility to brood parasitism. The findings are published in Springer's journal ...
Shaken, not stirred, is the essence of new research that's showing promise in creating the chemical reactions necessary for industries such as pharmaceutical companies, but eliminating the resulting waste from traditional methods. James Mack, a University of Cincinnati associate professor of chemistry, will present this research into greener chemistry on April 9, at the annual meeting of the American Chemical Society in New Orleans.
Instead of using solutions to create chemical reactions needed to manufacture products such as detergents, plastics and pharmaceuticals, ...
An analysis of U.S. Supreme Court decisions suggests "historical amnesia" regarding the growing power of speech rights for corporations in electronic media, versus the First Amendment rights of individuals. Jeff Blevins, associate professor and head of the University of Cincinnati's Department of Journalism, will present his research on Tuesday, April 9, at the 58th annual convention of the Broadcast Education Association in Las Vegas.
Blevins' presentation, titled "Historical Amnesia in First Amendment Jurisprudence on Corporate Power and Electronic Media," suggests ...
Scientists have described small genetic changes that enable the H5N1 bird flu virus to replicate more easily in the noses of mammals.
So far there have only been isolated cases of bird flu in humans, and no widespread transmission as the H5N1 virus can't replicate efficiently in the nose. The new study, using weakened viruses in the lab, supports the conclusions of controversial research published in 2012 which demonstrated that just a few genetic mutations could enable bird flu to spread between ferrets, which are used to model flu infection in humans.
Researchers ...
