Testing of Electron Beam Accelerators for Radiotherapy

Organisation:	University of Stirling (SCOTLAND, UNITED KINGDOM)
Method:	LOTOS
Tools used:	CADP (Construction and Analysis of Distributed Processes) TestGen
Domain:	Radiotherapy Equipment.
Period:	2002
Size:	910 lines of LOTOS, 180 of which are generated from the constraint annotations 41,097 states and 62,224 transitions 520 states and 546 transitions (after minimization with respect to observational equivalence) 256 test cases
Description:	Linear accelerators, which accelerate a beam of electrons to high-energy for use as X-rays, play an important role in cancer therapy. Their correct function is safety-critical and demands accurate delivery of radiation, usually used to destroy cancerous tissue: a radiation underdose is as undesirable as an overdose, since it might fail to kill a tumor, and not delivering radiation to the exact area damages surrounding healthy tissue. In contrary to early radiotherapy equipment, modern accelerators are complex-software controlled systems. Like for any application, the manufacturer upgrades the accelerator software from time to time. Thus it is desirable to check that the new version has not introduced any flaws. This case study describes the use of the conformance testing approach, originally developed for protocol verification, to the testing of radiotherapy accelerators. The suggested approach proceeds in several steps. Based on an understanding of the application via discussion with radiotherapy experts, an informal model of the system is created, and refined to a formal LOTOS specification, which is then annotated with constraints (significant test values and orderings of events). These constraints are translated automatically to LOTOS and integrated in the formal LOTOS specification. Using CADP, the labelled transition system corresponding to the specificiation including the constraints is generated and minimized. By traversing the generated labelled transition system, a suite of tests is generated automatically, and run against the implementation to decide whether it conforms to its specification.
Conclusions:	LOTOS is an appropriate language for the specification of radiotherapy accelerators, ties well with theories for test generation, and is well supported by readily available tools.
Publications:	[Turner-Bing-02] Kenneth J. Turner and Qian Bing. "Protocol Techniques for Testing Radiotherapy Accelerators". In Proceedings of the 22nd IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems FORTE'2002 (Houston, Texas, USA), 2002. Available on-line at: http://www.cs.stir.ac.uk/~kjt/research/pdf/test-rad.pdf or from the CADP Web site in PDF or PostScript [Turner-05-a] Kenneth J. Turner. "Test Generation for Radiotherapy Accelerators". In Springer International Journal on Software Tools for Technology Transfer (STTT), volume 7, number 4, August, 2005. Available on-line at: http://www.cs.stir.ac.uk/~kjt/research/pdf/test-gen.pdf or from the CADP Web site in PDF or PostScript
Contact:	Prof. Kenneth J. Turner Computing Science and Mathematics Room 4B78 University of Stirling Stirling FK9 4LA Scotland, United Kingdom Tel: +44-1786-467-423 Fax: +44-1786-464-551 Web: http://www.cs.stir.ac.uk/~kjt
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page