Investigating safety of a radiotherapy machine using system models with pluggable checkers

Download: PDF, slides (PDF).

“Investigating safety of a radiotherapy machine using system models with pluggable checkers” by Stuart Pernsteiner, Calvin Loncaric, Emina Torlak, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Jonathan Jacky. In CAV 2016: 28th International Conference on Computer Aided Verification, (Toronto, Canada), July 2016, pp. 23-41.

Abstract

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. 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.

Download: PDF, slides (PDF).

BibTeX entry:

@inproceedings{PernsteinerLTTWEJ2016,
   author = {Stuart Pernsteiner and Calvin Loncaric and Emina Torlak and
	Zachary Tatlock and Xi Wang and Michael D. Ernst and Jonathan
	Jacky},
   title = {Investigating safety of a radiotherapy machine using system
	models with pluggable checkers},
   booktitle = {CAV 2016: 28th International Conference on Computer Aided
	Verification},
   pages = {23-41},
   address = {Toronto, Canada},
   month = jul,
   year = {2016}
}

(This webpage was created with bibtex2web.)

Back to Michael Ernst's publications.