Database of Case Studies Achieved Using CADP

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)

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:
or from our FTP 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:
or from our FTP site in PDF or PostScript
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

Further remarks: This case study, amongst others, is described on the CADP Web site:

Last modified: Fri Feb 19 09:12:04 2016.

Back to the CADP case studies page