Allen School’s Zachary Tatlock and Neutrons software verification project featured in Communications of the ACM
Verifying that software runs safely and reliably is a mandate for mission-critical systems ranging from avionics to automobiles. A system of special significance to professor Zachary Tatlock and colleagues in the Allen School’s Programming Language and System Engineering (PLSE) group is the Clinical Neutron Therapy System (CNTS) at the UW Medical Center. One of only three radioactive therapy systems of its kind in the United States, the CNTS directs powerful radiation to patients’ heads to treat cancers of the tongue and esophagus. As Tatlock notes, “even a small mistake can be potentially deadly.”
In an article featured in the latest issue of Communications of the ACM, Tatlock discusses how he and a team of UW researchers are working to prevent such mistakes through the Neutrons project. The Neutrons project builds on Tatlock’s long-standing interest in devising and improving techniques to ensure that programs remain error free. Verifying systems like the CNTS presents its own set of challenges: the diversity and complexity of the radiotherapy system’s dozen components, each with its own level of criticality, meant that no single tool was suitable for checking critical component properties while also ensuring that their composition implies critical system properties.
Working with Dr. Jonathan Jacky, a radiation oncologist at UW, Tatlock and a team of Allen School researchers that includes professors Emina Torlak, Xi Wang, and Michael Ernst, and graduate students Stuart Pernsteiner and Calvin Loncaric applied modern software verification techniques to construct the first mechanically-checked safety case for a real safety-critical system in clinical use. The safety case includes a detailed formal model of the CNTS and a set of tools for establishing component properties specified by the model. Leveraging existing formal tools, the researchers built the entire case by writing just 2,700 lines of code.
The CNTS had been operating for over 30 years without incident. However, in constructing the case, Tatlock and the team revealed serious flaws that could potentially result in the beam operating outside of prescribed settings. They also discovered flaws in the implementation of the system’s EPICS language, which they reported to the CNTS staff.
Their work demonstrated that formal, checkable safety cases can provide significant practical benefits by focusing analysis effort on deep properties of system components that matter for the safety of the system as a whole.
“What we want to be able to do is ensure the reliability of all the pieces,” Tatlock explained in the article. “We want to make sure there are no bugs that can affect the parts that are critical.”
The Neutrons project is just one of several undertaken by PLSE researchers that use verification techniques described in the article, including Oeuf, which applies proof assistance to compilers; Verdi, for verifying distributed systems; and Bagpipe, for verifying internet router configurations.