TitleInvestigating safety of a radiotherapy machine using system models with pluggable checkers
Publication TypeConference Paper
Year of Publication2016
AuthorsPernsteiner S, Loncaric C, Torlak E, Tatlock Z, Wang X, Ernst MD, Jacky J
Conference NameCAV 2016: 28th International Conference on Computer Aided Verification
Pagination23-41
Date or Month PublishedJuly
Conference LocationToronto, Canada
AbstractFormal 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. Inspired by goals set out in prior work, we report on a large-scale 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 was suitable for both checking critical component properties and ensuring that their composition implies critical system properties. This paper describes how we used 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. We describe the key design decisions that diverged from previous approaches and that enabled us to practically apply our approach to provide machine-checked guarantees. Our case study uncovered subtle safety-critical flaws in a pre-release of the latest version of the radiotherapy system's control software.
Citation KeyPernsteinerLTTWEJ2016