Zachary Tatlock, University of Washington

Formally Checking Safety Cases for a Radiotherapy Machine


The Clinical Neutron Therapy System (CNTS) at the University of Washington has successfully operated for over 30 years without major incident. CNTS spans a diverse array of networked machines including custom beam controls running on general purpose operating systems, specialized Programmable Logic Controllers, mechanical interlocks, and even a trusty PDP-11. To achieve their excellent safety record, CNTS engineers have painstakingly written their control software (primarily in C), manually reviewed it line by line, and thoroughly tested it for decades. Recently, the CNTS team has developed a new control system to enable additional radiotherapy treatments. This new system, which replaces the existing C control software, is developed in the EPICS programming language. EPICS is a dataflow language commonly used in the control of radio telescopes and particle accelerators, but which has not been previously applied in safety critical settings nor studied by the verification community. To help maintain the excellent safety record of such a large, complex system, we have been developing a set of tools for constructing dependability cases that help ensure end-to-end correctness. Our talk will present background on CNTS, detail the CNTS dependability case, survey our methodology and verification tools, and discuss a new formal semantics we developed for EPICS.


Zach Tatlock is an Assistant Professor at the University of Washington in the Programming Languages and Software Engineering (PLSE) group. He and his students focus their research on reliability for the software infrastructure that many other programs depend on (compilers, distributed systems, networks, web browsers); control programs in safety-critical applications (radiotherapy devices, robotics); and approximations used in engineering and manufacturing (floating point, 3D printing).