Formal techniques for guaranteeing software correctness have made tremendous progress in recent decades. However, applying these techniques to real-world safety-critical systems remains challenging in practice. The Neutrons Project is a largescale case study that applies modern verification techniques to check safety properties of a radiotherapy system in current clinical use. Because of the diversity and complexity of the system’s components (software, hardware, and physical), no single tool is suitable for both checking critical component properties and ensuring that their composition implies critical system properties. Our work uses state-of-the-art approaches to develop specialized tools for verifying safety properties of individual components, as well as an extensible tool for composing those properties to check the safety of the system as a whole. This has lead to key lessons and design decisions that diverged from previous approaches and that enabled us to practically apply our approach to provide machine-checked guarantees. Our case studies uncovered subtle safety-critical flaws in a prerelease of the latest version of the radiotherapy system’s control software, and we have been working closely with the CNTS team since to help improve the reliability of the radiotherapy control software.
Automatic Formal Verification for EPICS
Jonathan Jacky, Stefani Banerian, Michael D. Ernst, Calvin Loncaric, Stuart Pernsteiner, Zachary Tatlock, Emina Torlak
Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers
Stuart Pernsteiner, Calvin Loncaric, Emina Torlak, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Jonathan Jacky
Toward a Dependability Case Language and Workflow for a Radiation Therapy System
Michael D. Ernst, Dan Grossman, Jon Jacky, Calvin Loncaric, Stuart Pernsteiner, Zachary Tatlock, Emina Torlak, and Xi Wang