Testing a radiotherapy support system with QuickCheck

Abstract

In this report we present a case study on using light-weight formal methods for testing an implementation of a medical device. The device is a real-time organ position tracking system used in radiotherapy. The system properties to be tested were modeled and verified through automated test cases generated by QuickCheck. QuickCheck demonstrated to be beneficial tool for reducing the complexity inherent to testing medical devices by detecting faults at system level, supporting a better type of regression testing and supporting the detection of abnormal cases that could be analyzed and fixed afterwards in the system.