Abstract
The nature of radiotherapy accelerators is briefly explained. It is argued that these complex safety-critical systems need a systematic basis for testing their software. The paper describes a novel application of protocol specification and testing methods to radiotherapy accelerators. An outline specification is given in Lotos (Language Of Temporal Ordering Specification) of the accelerator control system. It is completely infeasible to use this directly for test generation. Instead, specification inputs are restricted using annotations in a Parameter Constraint Language. This is automatically translated into Lotos and combined with the accelerator specification. It then becomes manageable to generate tests automatically of the actual accelerator to check that it agrees with its specification according to the relation ioconf(input-output conformance). Sample input annotations, their translation to Lotos, and the resulting test cases are described.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
M. Calder and C. E. Shankland. A symbolic semantics and bisimulation for full Lotos. In M. Kim, B. Chin, S. Kang, and D. Lee, editors, Proc. Formal Techniques for Networked and Distributed Systems, pages 184–200. Kluwer, London, UK, Sept. 2001.
EC. Medical devices directive. Technical Report 93/42/EEC, European Commission, Brussels, Belgium, June 1993.
FDA. Medical devices: Current good manufacturing practice. Technical Report 61 FD 195, US Food and Drug Administration, NewYork, USA, Oct. 1996.
J.-C. Fernández, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier, and M. Sighireanu. CADP (CÆSAR/ALDÉBARAN Development Package):A protocol validation and verification toolbox. In R. Alur and T.A. Henzinger, editors, Proc. 8th. Conference on Computer-AidedVerification, LNCS 1102, pages 437–440. Springer-Verlag, Berlin, Germany,Aug. 1996.
D. Greene and P. C. Williams. Linear Accelerators for Radiation Therapy. IOP Publishing Ltd., Bristol and Philadelphia, 1997.
R. C. Ho, C. H. Yang, M. A. Horowitz, and D. L. Dill. Architecture validation for processors. In Proc. 22nd. Annual International Symposium on Computer Architecture, 1995.
IEC. Medical Electrical Equipment-Part 2: Particular Requirements for Safety. IEC 601-2. International Electrotechnical Commission, Geneva, Switzerland, 1988.
ISO/IEC. Information Processing Systems-Open Systems Interconnection-LOTOS-A Formal Description Technique based on the Temporal Ordering of Observational Behaviour. ISO/IEC 8807. International Organization for Standardization, Geneva, Switzerland, 1989.
ISO/IEC. Information Processing Systems-Open Systems Interconnection-Enhanced LOTOS-A Formal Description Technique based on the Temporal Ordering of Observational Behaviour. ISO/IEC 15437. International Organization for Standardization, Geneva, Switzerland, 2001.
J. Jacky, J. Unger, M. Patrick, D. Reid, and R. Risler. Experience with Z developing a control program for a radiation therapy machine. In J. P. Bowen, editor, Proc. 10th. International Conference of Z Users, LNCS. Springer-Verlag, Berlin, Germany, Dec. 1996.
J. Jacobson and O. Andersen. Software controlled medical devices. Technical Report SPRapport 1997:11, European Network of Clubs for Reliability and Safety of Software, Apr. 1997. ISBN 91-7848-669-6.
Ji He and K. J. Turner. Protocol-inspired hardware testing. In G. Csopaki, S. Dibuz, and K. Tarnay, editors, Proc. Testing Communicating Systems XII, pages 131–147. Kluwer, London, UK, Sept. 1999.
E. J. Joyce. Accelerator linked to fifth radiation overdose. American Medical News, 1, Feb. 1987.
C. J. Karzmark. Procedural and operator error aspects of radiation accidents in radiotherapy. International Journal of Radiation Oncology Biological Physics, 13:1599–1602, Jan. 1987.
N. Leveson and C. S. Turner. An investigation of the Therac-25 accidents. IEEE Computer, 26(7):18–41, July 1993.
R. Nath, P. J. Biggs, F. J. Bova, C. C. Ling, J. A. Purdy, J. van de Geijn, and M. S. Weinhous. AAPM code of practice for radiotherapy accelerators. Medical Physics, 21(7):1093–1121, July 1994.
Qian Bing and K. J. Turner. Input value constraints for radiotherapy accelerator specification. Technical Report CSM-161, Computing Science and Mathematics, University of Stirling, UK, Aug. 2002.
M. H. Thomas. The story of the Therac-25 in Lotos. High Integrity Systems Journal, 1(1):3–15, Feb. 1994.
J. Tretmans. Test generation with inputs, outputs and repetitive quiescence. Software Concepts and Tools, 17:103–120, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Turner, K.J., Bing, Q. (2002). Protocol Techniques for Testing Radiotherapy Accelerators. In: Peled, D.A., Vardi, M.Y. (eds) Formal Techniques for Networked and Distributed Sytems — FORTE 2002. FORTE 2002. Lecture Notes in Computer Science, vol 2529. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36135-9_6
Download citation
DOI: https://doi.org/10.1007/3-540-36135-9_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00141-6
Online ISBN: 978-3-540-36135-0
eBook Packages: Springer Book Archive