Formal techniques for guaranteeing software correctness have made tremendous progress in recent decades. However, applying these techniques to existing, 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 system components (software, hardware, and physical), no single tool was suitable for checking critical cross-component safety properties. This paper describes how we used state-of-the-art approaches to develop specialized tools for checking different components and an extensible Safety Case Checker (SCC) for composing the properties checked for each component. 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.
[ bib | project | paper ] Back
This file was generated by bibtex2html 1.97.