Radiation therapy machine

This page looks best when this and this X are about the same size: X. See these viewing tips.

This report presents portions of a formal specification for a real medical device, a radiation therapy machine. This specification, rather than the informal prose description, serves as the primary reference source for programming and test plannning. A paper [jacky95b] describes the development of part of the program based on the contents of this report.

This formal specification is based on a thorough informal (English prose) specification presented as Chapters 2 and 8 in [jacky92]. Here we attempt to formalize the requirements in that source. We have included many cross-references. Decimal numbers and integers (as in 8.4, 191) refer to chapter, section and page numbers in [jacky92], respectively.

The formal specification is expressed in the Z notation [spivey92]. We have corrected syntax and type errors detected by a checker [spivey92a].

Overview

Much of the apparent complexity in the prose requirements arises from the interaction of several subsystems which, by themselves, are simpler. In the formal specification we partition the system into subsystems and describe simple operations on each. For each operation on the system as a whole, we define a separate operation on each affected subsystem. The complex behaviors of the whole system emerge when we compose these simpler operations together.

Each subsystem is modelled by a Z state schema and a number of operation schemas on that state. This partition can itself be represented in Z.

$\begin{schema}{$		TherapyControl



		Session
		Field
		Intlk
		...
		Console

	$\end{schema}$

Session (section [sect:session]) models those aspects of the treatment session that are related to the prescription database (section [sect:prescr] models the database itself). Field (section [sect:field]) models the many settings that characterize a single field. Intlk (section [sect:intlk]) models software interlocks and other flags that indicate readiness. Console (section [sect:ui]) models the user interface. Section [sect:compose] combines operations from Session, Field and Console.

Related operations in different subsystems are distinguished by suffix: ExptModeS, ExptModeF, and ExptModeC are operations in the Session, Field and Console subsystems, respectively.

Each user interface operation in the Console subsystem ensures that corresponding operations in the Session and Field subsystems are only invoked when their preconditions are satisfied. Therefore only the Console operations need to be total; usually there is no need to define total operations in the Session and Field subsystems. For example the ExptModeC operation in the Console subsystem checks the precondition that only physicists can invoke this operation; in Console we define what happens when an operator who is not a physicist attempts to enter experiment mode. Therefore ExptModeS and ExptModeF can assume that this precondition has been satisfied and need not cover the other cases.

System configuration

Fixed aspects of the system configuration are represented by Z global constants: sets, functions and relations. This section introduces some of these constants. It should be possible to accommodate some configuration changes simply by changing their values.

Settings and registers

The state of the therapy machine is largely determined by the values of named items. At this writing the list of items is

calvolt1 | calvolt2 | p_dose | p_time | e_time

For brevity we omit formal declarations of the other collimator leaves, leaf1 .. leaf38.

There are many items but we can identify different subsets, where all of the members of each subset are treated the same way for some particular purpose.

Settings are items which are included in field prescriptions. Other items are kept in registers. In particular dose_reg items include calibration factors and other items concerned with the dosimetry system (In the C implementation setting and dose_reg are two different enumerations, separated so we can efficiently store and index zero-based C arrays. We may add other register enumerations in the future, for example for the LCC calibration factors.).

$\begin{axdef}$
		setting, dose_reg: $\power$ ITEM
	$\end{axdef}$

$\langle$ setting, dose_reg $\rangle$ partition ITEM

dose_reg = { pt_mode, pt_factor, press, temp, d_rate, t_fac,

calvolt1, calvolt2, p_dose, p_time, e_time )

Scales are items that are continously variable over some range; examples are gantry angle and every collimator leaf position. Selections can only take on certain discrete values; examples are wedge and flattening filter selection. Counters accumulate during treatment runs; examples are dose and the number of fractions.

$\begin{axdef}$
		scale, selection, counter: $\power$ ITEM
	$\end{axdef}$

$\langle$ selection, scale, counter $\rangle$ partition ITEM

counter = { nfrac, dose_tot, dose }

selection = { wedge, w_rot, filter, pt_mode }

A field is prescribed by determining the values of certain of its settings. Therapy fields are defined by the values of particular settings called prescriptions. Experiment fields are defined by the values of settings called presets (8.2, 171 third bullet; Table 8.2, 173). Readiness is determined by checking all the preset settings in experiment mode, and all the prescr settings (prescrip except the linear table motions) in therapy mode (8.9.8, 194). Most settings are machine motions, and the actual values of most settings are measured by sensors. The calibration constants are registers that are initially loaded with constants stored in the calibration database. At this writing

leaves == { leaf0, leaf39 }

preset == leaves $\cup$ {wedge, w_rot, filter }

motion == preset $\cup$ { gantry, collim, turnt, lat, longit, height }

prescrip == motion $\cup$ counter

prescr == prescrip \ { lat, longit, height }

sensor == setting \ { nfrac, dose_tot }

cal_const == { d_rate, t_fac, calvolt1, calvolt2 }

Values

Each item will be implemented by an appropriate (possibly floating point) numeric type. In this report it is sufficient to say they are all numbers, to indicate that we can do arithmetic with them.

Each item can assume a particular range of valid (physically achievable) values. For example, the gantry angle can vary from 0 to 359 (In the implementation gantry angle varies from 0.0 to 359.9. Decimal fractions are not built into Z.); the available wedge selections are no_wedge, 30, 45 and 60. We use valid to do range checking on numbers that the operator types in, and also on sensor readings, to check for faults (The C implementation includes one valid array indexed by setting and another (with a different name) indexed by dose_reg.). Every setting s has some valid values, and there is always a minimum and a maximum valid value. We define an uninitialized or blank value which is not valid for any setting. For each scale item, there is a tolerance within which variations in value are acceptable.

$\begin{axdef}$
		blank: VALUE
		tol: scale $\fun$ VALUE
		valid: ITEM $\fun$ $\finset$ ₁ VALUE

	$\where$

		$\forall$ s: ITEM blank $\notin$ valid s
	$\end{axdef}$

Prescription database

The prescription database stores patients and fields. We define a basic type for the names that identify them.

[NAME]

PATIENT == NAME; FIELD == NAME

An item's name usually corresponds to the text string that identifies it in screen displays and log files (We define one type for both kinds of names so the same specifications (and code) can be used to handle lists of patients and fields. In the implementation, elements of NAME are integer indices into arrays, usually of C structures that include the name string as one member.).

$\begin{axdef}$
		no_name: NAME
	$\end{axdef}$

no_patient == no_name; no_field == no_name

In experiment mode, we store fields under studies which are analogous to patients. In our model they have the same type.

$\begin{axdef}$
		studies,patients: $\power$ PATIENT

	$\where$

		no_patient $\notin$ studies $\land$ no_patient $\notin$ patients
	$\end{axdef}$

For each patient or study, several prescribed fields are stored (This differs from [jacky90d], which describes a single collection of experiment fields. Moreoever, for each experiment field we now store the same prescrip settings as for therapy fields, although we only check the preset settings for agreement with the stored prescription). We must check against delivering too many fractions or monitor units from the same field (8.9.4, 187 -- 188), so the accumulated values of the counters are also stored (for patient fields only).

ACCUMULATION == counter $\fun$ VALUE

PRESCRIPTION == prescrip $\fun$ VALUE

$\begin{axdef}$
		Preset: studies $\fun$ (FIELD $\pfun$ PRESCRIPTION)
		Prescribed: patients $\fun$ (FIELD $\pfun$ PRESCRIPTION)
		Accumulated: patients $\fun$ (FIELD $\pfun$ ACCUMULATION)

	$\where$

		$\forall$ s: studies no_field $\notin$ dom (Preset s)
		$\forall$ p: patients no_field $\notin$ dom (Prescribed p)
		$\land$ dom (Prescribed p) = dom (Accumulated p)
	$\end{axdef}$

The exceeded predicate tests whether the prescribed fractional dose, total dose or number of fractions have already been delivered.

$\begin{axdef}$
		exceeded _ : ACCUMULATION $\rel$ PRESCRIPTION

	$\where$

		$\forall$ counters: ACCUMULATION; fields: PRESCRIPTION
		exceeded(counters,fields) $\iff$ ( $\exists$ c: counter counters c $\geq$ fields c)
	$\end{axdef}$

In the following discussion consider field f of patient p; let prescribed = Prescribed p f and accumulated = Accumulated p f. The prescription includes the number of fractions prescribed n and the total dose prescribed dose_tot. We also keep track of the number of fractions accumulated to date accumulated n, the number of monitor units delivered since the beginning of the day accumulated dose and the total number of monitor units accumulated to date accumulated dose_tot (8.9.4, Fig. 83, 186).

Operators

Our OPERATOR type includes the operator's username and password. A special value indicates no operator has logged in. Physicists are operators who are authorized to use the equipment in its experiment mode (8.2, 170).

$\begin{axdef}$
		no_operator: OPERATOR
		operators, physicists: $\power$ OPERATOR

	$\where$

		physicists $\subseteq$ operators
	$\end{axdef}$

Session

In this section we model those aspects of the treatment session that are related to the prescription database. In section [sect:compose], we will combine the operations defined here with user interface operations described in section [sect:ui].

Session state

The Session state is determined by the treatment mode, the operator on duty, the currently selected patient and field, the accessible names (patients or studies), and the accessible prescribed fields and their counters. We first define SessionVars which declares all the state variables and provides predicates to ensure that the operator is authorized for the mode, and the names are consistent with the mode.

MODE ::= therapy | experiment

$\begin{schema}{$		SessionVars



		mode: MODE
		operator: OPERATOR
		patient: PATIENT
		field: FIELD
		names: $\power$ PATIENT
		fields: FIELD $\pfun$ PRESCRIPTION
		counters: FIELD $\pfun$ ACCUMULATION

	$\where$

		operator = no_operator $\lor$ operator $\in$ operators
		mode = experiment $\implies$ operator $\in$ physicists
		names = if mode = therapy then patients else studies

	$\end{schema}$

Next, we define two cases. When no patient is selected, no prescribed fields are accessible; no field can be selected.

$\begin{schema}{$		NoPatient



		SessionVars

	$\where$

		patient = no_patient
		field = no_field
		fields = $\emptyset$
		counters = $\emptyset$

	$\end{schema}$

When a patient is selected, that patient's fields are accessible. If a field is selected, it must be one of these.

$\begin{schema}{$		PrescribedPatient



		SessionVars

	$\where$

		patient $\neq$ no_patient
		patient $\in$ names
		field = no_field $\lor$ field $\in$ dom fields
		fields = if mode = therapy then Prescribed patient else Preset patient
		mode = therapy $\implies$ counters = Accumulated patient

	$\end{schema}$

Session $\defs$ PrescribedPatient $\lor$ NoPatient

The Session subsystem starts up in therapy mode with no operator and no patient.

$\begin{schema}{$		InitSession



		NoPatient

	$\where$

		mode = therapy
		operator = no_operator

	$\end{schema}$

None of the Session state variables are sensor inputs; all are under program control.

Operations on Session

In the following subsections we model the operations on Session. We will put together the operations defined in different states in section [sect:compose], below.

Experiment mode

Physicists can toggle the session from therapy mode to experiment mode and back (This is a change from the original requirements in [jacky90d], where Experiment Mode switches to experiment mode but Select Patient switches back to therapy mode.). The user interface ensures that only physicists can invoke this operation, so there is no need here to define a total operation that describes what happens when an operator who is not a physicist attempts this operation. After switching modes, no patient (study) and no field are selected (8.9.6, 190 -- 191).

$\begin{schema}{$		ExptModeS



		$\Delta$ Session

	$\where$

		operator $\in$ physicists
		NoPatient'
		(mode',names') = if mode = therapy then (experiment,studies)
		else (therapy,patients)
		operator' = operator

	$\end{schema}$

Store Field

Store Field (8.9.5, 189 -- 188) accepts a new field name, which becomes the selected field and is also added to the list of fields (The prose [jacky92] also requires that the new field be added to the prescription database for the current patient. We do not model this formally (in fact we model the prescription database as a constant). The precondition patient no_patient is not explicit in the prose.).

$\begin{schema}{$		StoreFieldS



		$\Delta$ Session
		field?: FIELD
		prescribed': PRESCRIPTION
		accumulated': ACCUMULATION

	$\where$

		patient $\neq$ no_patient
		field' = field?
		fields' = fields $\cup$ { field' $\mapsto$ prescribed' }
		mode = therapy $\implies$ counters' = counters $\cup$ { field' $\mapsto$ accumulated' }

		mode' = mode
		operator' = operator
		patient' = patient
		names' = names

	$\end{schema}$

Here prescribed' and accumulated' are just place holders; their values are defined in the corresponding Field operation StoreFieldF.

Login (2.5.2, 17 -- 20; 8.9.1, 183) accepts a new operator?. The user interface ensures that the new operator is authorized.

$\begin{schema}{$		NewOperator



		$\Delta$ Session
		operator?: OPERATOR

	$\where$

		operator' = operator?
		operator' $\in$ operators

	$\end{schema}$

There are two variations. Usually the new operator is sufficiently privileged to keep the same mode. Otherwise the session reverts to therapy mode with no patient and no field (8.9.6, 190).

$\begin{schema}{$		Privileged



		NewOperator

	$\where$

		mode = therapy $\lor$ operator' $\in$ physicists

		mode' = mode
		patient' = patient
		names' = names
		field' = field
		fields' = fields
		counters' = counters

	$\end{schema}$

$\begin{schema}{$		Unprivileged



		NewOperator

	$\where$

		mode = experiment
		operator $\notin$ physicists
		mode' = therapy
		NoPatient'

	$\end{schema}$

LoginS $\defs$ Privileged $\lor$ Unprivileged

Select Patient

In Select Patient (8.9.3, 184 -- 185) the patient's prescribed fields are loaded, but no field is selected (The prose [jacky90d] says that if the patient list is selected in experiment mode, the session reverts to therapy mode (8.9.3, 184 last paragraph). We have dropped this requirement.). The user interface ensures that the new patient is in the prescription database.

$\begin{schema}{$		SelectPatientS



		$\Delta$ Session
		patient?: PATIENT

	$\where$

		patient? $\in$ names
		patient' = patient?
		field' = no_field
		fields' = if mode = therapy then Prescribed patient' else Preset patient'
		mode = therapy $\implies$ counters' = Accumulated patient'

		mode' = mode
		operator' = operator
		names' = names

	$\end{schema}$

Select Field

Select Field (8.9.4, 186 -- 189) changes the current field. The user interface ensures this operation cannot occur if there is no patient, and ensures that the new field is prescribed.

$\begin{schema}{$		SelectFieldS



		$\Delta$ Session
		field?: FIELD

	$\where$

		patient $\neq$ no_patient
		field? $\in$ dom fields
		field' = field?

		operator' = operator
		mode' = mode
		patient' = patient
		fields' = fields
		counters' = counters

	$\end{schema}$

Field

In this section, we look inside the machine state and deal with particular machine settings. We model operations that involve the many settings that characterize a single field.

Field state

The Field schema includes the state variables that represent settings for the currently selected field and mode. Sensors report measured setting values. Prescribed setting values are read from the prescription database.

Computed and calibrated item values are entered by the operator or calculated from prescribed settings and calibration constants; these are stored in registers. Certain calibration constants are stored in files (8.9.13, 213 first full paragraph; 215 last paragraph). Counters hold setting values that are accumulated over successive runs. For example, the dose prescribed for a single fraction may be have to be delivered in two or more treatment runs.

Some settings that do not match their prescribed values can be overridden by the operator (8.4, 175 second paragraph; 8.8.1, 181). It is necessary to store the value of each setting when it is overridden (see the requirement in the last paragraph under ``override'' on p. 181). Only settings that are prescribed can be overridden.

$\begin{axdef}$
		cal_factor: cal_const $\fun$ VALUE
	$\end{axdef}$

$\begin{schema}{$		Field



		prescribed: PRESCRIPTION
		accumulated: ACCUMULATION
		measured: sensor $\fun$ VALUE
		overridden: prescr $\pfun$ VALUE
		computed, calibrated: dose_reg $\fun$ VALUE

	$\end{schema}$

The measured settings are read from sensors so here we cannot write any predicates that constrain them.

Relation to Session state

A few operations on Field read the mode and field state variables declared in Session. In therapy mode, the prescribed settings in the Field state are those from the prescription database entry for the currently selected mode and field in the Session state. (In experiment mode the prescribed settings are also loaded from the prescription database but may be changed subsequently. In therapy mode the counters are loaded from the prescription database when the field is selected but may be changed subsequently. See section [sect:sel-field-f]).

$\begin{schema}{$		PrescribedField



		Field
		Session

	$\where$

		field $\neq$ no_field
		mode = therapy $\implies$ prescribed = fields field

	$\end{schema}$

When no field has been selected, prescribed settings and counters have no values and the computed settings dose and time indicate no dose. (8.9.7, 192, second paragraph after the bullets). No settings are overridden (8.9.8, 194; 8.9.9, 196; 8.9.10, 198).

no_prescrip == ( $\lambda$ p: prescrip

blank)

no_counter == ( $\lambda$ c: counter

blank)

no_dose_reg == ( $\lambda$ d: dose_reg

blank)

no_dose == { p_dose $\mapsto$ blank, p_time $\mapsto$ blank }

$\begin{schema}{$		NoFieldF



		Field

	$\where$

		prescribed = no_prescrip
		accumulated = no_counter
		no_dose $\subseteq$ computed
		overridden = $\emptyset$

	$\end{schema}$

NoFieldS $\defs$ [ Session | field = no_field ]

NoField $\defs$ NoFieldF $\land$ NoFieldS

FieldSession $\defs$ PrescribedField $\lor$ NoField

Initialization

Field begins with no field. The calibration factors are initialized with the constants on file (8.9.13, 213, second paragraph after bullets) and the other registers hold no values.

$\begin{schema}{$		InitField



		NoFieldF

	$\where$

		computed = calibrated = no_dose_reg $\oplus$ cal_factor

	$\end{schema}$

Operations on Field

In the following subsections we model the operations on Field. We will put together the operations defined in different states in section [sect:compose], below.

Select Patient

SelectPatient also affects Field: when a patient is first selected, there is no field.

$\begin{schema}{$		SelectPatientF



		$\Delta$ Field

	$\where$

		NoFieldF'
		computed' = computed $\oplus$ no_dose

		calibrated' = calibrated

	$\end{schema}$

Select Field

When a new field is selected, its prescribed settings are loaded and no settings are overridden. This operation requires read-only access to the fields state variable in the Session schema.

$\begin{schema}{$		NewFieldF



		$\Delta$ FieldSession

	$\where$

		prescribed' = fields field'
		overridden' = $\emptyset$

	$\end{schema}$

There are two variants of SelectField. Experiment mode is much simpler because there is no prescribed dose. The prescribed settings are loaded. The dose and time do not change (8.9.11, 202, second paragraph from bottom).

$\begin{schema}{$		SelectExptFieldF



		NewFieldF

	$\where$

		mode = experiment
		computed' = computed
		calibrated' = calibrated

	$\end{schema}$

Selecting rectangular fields in experimental mode (8.9.4, 188 -- 189) is not modelled formally.

In therapy mode, the dose for the treatment run and the treatment backup time are calculated. Treatment backup time is calculated from the dose and two calibration factors, the machine's nominal dose rate computed d_rate and the treatment time factor computed t_fac (8.9.11, 200, last paragraph; 202, second paragraph; 8.9.13, 213, first two paragraphs after bullets) (The backup time is given by t_backup = factor * dose / rate. For example with prescribed dose 100.0 MU, dose rate 50.0 MU/min and factor 1.50 the backup time is 3.00 minutes. We do not attempt to model this floating-point calculation in Z.).

DOSE == VALUE; RATE == VALUE; FACTOR == VALUE; TIME == VALUE

$\begin{axdef}$
		t_backup: (DOSE $\cross$ RATE $\cross$ FACTOR) $\pfun$ TIME

	$\where$

		$\forall$ d: valid dose; r: valid d_rate; f: valid t_fac
		(d,r,f) $\in$ dom t_backup $\land$ t_backup(d,r,f) $\in$ valid p_time
	$\end{axdef}$

We keep track of the number of monitor units delivered since the beginning of the day accumulated dose. When the prescribed field settings are loaded, the computed dose is adjusted to deliver the remaining daily dose. This makes it easy to set up another treatment run for the same field if the earlier attempts had to be interrupted for any reason, or were used to make a port film. The treatment backup time is calculated from this adjusted dose, not the prescribed dose.

The adjusted dose and corresponding backup time are stored in computed p_dose and calibrated p_time (computed p_dose may differ from prescribed dose). There is also a register computed p_time where the user may optionally enter a backup time different than calibrated p_time (section [sect:editf], below) (8.9.11, Fig. 8.8, 199; Fig. 8.9, 203; Fig 8.10, 207; Fig. 8.11, 208).

$\begin{schema}{$		DoseTime



		$\Delta$ Field

	$\where$

		(let t == t_backup(computed' p_dose,computed' d_rate,computed' t_fac)
		calibrated' = calibrated $\oplus$ { p_time $\mapsto$ t })
		computed' p_time = calibrated' p_time
		{ p_dose, p_time } $\ndres$ computed' = { p_dose, p_time } $\ndres$ computed

	$\end{schema}$

$\begin{schema}{$		NewTherapyField



		NewFieldF
		DoseTime

	$\where$

		mode = therapy
		accumulated' = counters field'

	$\end{schema}$

There are two cases. The normal case occurs when the user interface confirms that the prescribed fractional dose, total dose and number of fractions are not yet exceeded. The dose is read from the prescription, and no settings are overridden (8.9.4, 187).

$\begin{schema}{$		SelectTherapyFieldF



		NewTherapyField

	$\where$

		computed' p_dose = prescribed dose - accumulated dose
		overridden' = $\emptyset$

	$\end{schema}$

SelectSimpleFieldF $\defs$ SelectExptFieldF $\lor$ SelectTherapyFieldF

The other case occurs when the user interface acquires the preset dose from the operator (often when one or more of the counter settings is exceeded. If this differs from the prescribed dose then dose is overridden, and any exceeded settings are also overridden (8.9.4, 188).

$\begin{schema}{$		SelectComplexFieldF



		NewTherapyField
		dose?: VALUE

	$\where$

		computed' p_dose = dose?
		(let ovr ==
		( $\lambda$ c: counter \| accumulated' c $\geq$ prescribed' c accumulated c)
		overridden' = if dose? = prescribed' dose
		then ovr else ovr $\cup$ { dose $\mapsto$ dose? })

	$\end{schema}$

Here we have made a few small changes from the prose requirements. According to the prose (8.9.4, 187 -- 188), the Select Field operation includes a dialog with the operator to enter a new dose or treatment time in some cases. In our formal specification it is necessary for the operator to explicitly select the Edit operation after Select Field in order to enter a new dose or treatment time. These minor adjustments achieve the intent of the prose and simplify the program. As required by the prose, our SelectComplexFieldF overrides exceeded settings (after operator confirmation, enforced by the user interface) (We also considered the slightly simpler alternative of omitting the operator confirmation and leaving overridden = in the exceeded case. In that alternative, the Intlk subsystem (section [sect:intlk]) would make the offending settings not_ready to prevent the field being delivered unless the operator explicitly edits or overrides those settings.).

Edit setting

$\begin{schema}{$		EditF



		$\Delta$ Field
		item?: ITEM
		value?: VALUE

	$\where$

		accumulated' = accumulated
		calibrated' = calibrated

	$\end{schema}$

The prose actually describes four Edit operations. Some features are common to all. The first variation is for preset settings; the user interface ensures this can be invoked in experiment mode only (8.8.1, 180). The prescribed value is changed, and that setting is no longer overridden.

$\begin{schema}{$		EditPresetF



		EditF

	$\where$

		item? $\in$ preset
		prescribed' = prescribed $\oplus$ { item? $\mapsto$ value? }
		overridden' = { item? } $\ndres$ overridden

		computed' = computed

	$\end{schema}$

The second variation is for calibration factors; again, the user interface only provides this in experiment mode (8.9.3, 215). Calibration factors that users can edit are modelled as computed settings in registers. Calibration factors are never considered overridden.

$\begin{schema}{$		EditCalF



		EditF

	$\where$

		item? $\in$ dose_reg \ { p_dose, p_time }
		computed' = computed $\oplus$ { item? $\mapsto$ value? }

		prescribed' = prescribed
		overridden' = overridden

	$\end{schema}$

The third variation is for dose (8.9.11, 201--202). The computed (not prescribed) value is changed, and the dose is considered overridden (8.9.4, 188; 8.9.11, 202). The treatment times are recalculated.

$\begin{schema}{$		EditDoseF



		EditF
		DoseTime

	$\where$

		item? = p_dose
		computed' p_dose = value?
		overridden' = overridden $\oplus$ { dose $\mapsto$ value? }

		prescribed' = prescribed

	$\end{schema}$

The fourth and last variation is treatment backup time, which can be edited in both modes (8.9.11, 202). Here again the computed value is changed; time is not a prescribed setting, so it cannot be overridden.

$\begin{schema}{$		EditTimeF



		EditF

	$\where$

		item? = p_time
		computed' = computed $\oplus$ { p_time $\mapsto$ value? }

		prescribed' = prescribed
		overridden' = overridden

	$\end{schema}$

EditSettingF $\defs$

EditCalF $\lor$ EditPresetF $\lor$ EditDoseF $\lor$ EditTimeF

EditSettingF is not a total operation (it does not handle all possible values of ITEM) but the user interface ensures that its preconditions are always satisfied.

We now provide the EditDoseF and EditTimeF operations instead of the dialog after Select Field proposed in [jacky92] (8.9.4, 187 -- 188).

Override

$\begin{schema}{$		OverF



		$\Delta$ Field
		item?: ITEM

	$\where$

		prescribed' = prescribed
		accumulated' = accumulated
		computed' = computed
		calibrated' = calibrated

	$\end{schema}$

We add a newly overridden setting and its currently measured value to the overridden function (8.4, 175 second paragraph; 8.8.1, 181). If the setting is already overridden, the override is cancelled.

$\begin{schema}{$		OverrideSetting



		OverF

	$\where$

		item? $\in$ prescr
		overridden' =
		if item? $\notin$ dom overridden
		then overridden $\oplus$ { item? $\mapsto$ measured item? }
		else { item? } $\ndres$ overridden

	$\end{schema}$

Dose and time are special cases; overriding either makes dose overridden with its accumulated (not measured) value as the overridden value. The counters total dose dose_tot and number of fractions nfrac can only be overridden (after operator confirmation) as part of the SelectFieldF operation.

$\begin{schema}{$		OverrideDose



		OverF

	$\where$

		item? $\in$ { p_dose, p_time }
		overridden' =
		if dose $\notin$ dom overridden
		then overridden $\oplus$ { dose $\mapsto$ accumulated dose }
		else { dose } $\ndres$ overridden

	$\end{schema}$

OverrideF $\defs$ OverrideSetting $\lor$ OverrideDose

Store Field

This operation (8.9.5, 189 -- 190) makes the prescribed settings equal to the actual machine settings, except there is no prescribed dose and the number of fractions is set to one. The accumulators are reset to zero.

zero_counter == ( $\lambda$ c: counter

$\begin{schema}{$		StoreFieldF



		$\Delta$ FieldSession

	$\where$

		computed' = computed $\oplus$ no_dose
		prescribed' = prescribed $\oplus$ (prescrip $\dres$ measured)
		$\oplus$ no_counter $\oplus$ { nfrac $\mapsto$ 1 }
		accumulated' = zero_counter
		overridden' = $\emptyset$

		calibrated' = calibrated

	$\end{schema}$

Experiment Mode

This operation toggles modes with no field. There are no dose and time (8.9.11, 202, second paragraph from bottom).

$\begin{schema}{$		ExptModeF



		$\Delta$ Field

	$\where$

		NoFieldF'
		computed' = computed $\oplus$ no_dose

		calibrated' = calibrated

	$\end{schema}$

Calibration factors

Dosimetry calibration

Dosimetry calibration factors, including the dose rate and treatment time factor used to calculate the backup time, appear on the Dosimetry Calibration display (8.9.13, 213 -- 214) (Called Cal Factors in [jacky92], since renamed to distinguish it from the forthcoming LCC Calibration etc.). The calibrated values in the left column are read from files or measured by sensors, while the computed values in the right column are computed by the control program or entered by the operator using the EditCalF operation.

The pressure-temperature correction factors are used to adjust the standard calibration voltages for the dosimetry system (8.9.13, 213 -- 215). The calibrated calvolt1 and calibrated calvolt2 represent the standard calibration voltages on file (8.9.13, 213, second paragraph from bottom), while computed calvolt1 (etc.) represent the calibration voltages actually in effect, which are obtained by adusting the standard calibration voltage by a barometric pressure/temperature correction factor (8.9.13, 213 bottom paragraph, 214 top paragraph) (The pressure-temperature factor is given by pt_factor = (press/1013) \times (295/(temp+273)), where press and temp are in mbar and deg. C, respectively. We do not attempt to model this floating-point calculation in Z.).

PRESSURE == VALUE; TEMPERATURE == VALUE

$\begin{axdef}$
		pt_formula: (PRESSURE $\cross$ TEMPERATURE) $\pfun$ FACTOR

	$\where$

		$\forall$ p: valid press; t: valid temp
		(p,t) $\in$ dom pt_formula $\land$ pt_formula(p,t) $\in$ valid pt_factor
	$\end{axdef}$

The computed press and computed temp are the pressure and temperature entered by the operator, and while calibrated temp and calibrated press are measured continously by sensors. The computed pt_factor stores the barometric pressure/temperature correction factor of the day calculated from the readings entered by the operator (8.9.13, 214, third paragraph), while calibrated pt_factor stores the automatic pressure/temperature correction factor calculated from sensor readings (8.9.13, 214, fourth paragraph). The pressure-temperature interlock (section [sect:intlk]) accounts for the possibility that the pressure or temperature values might be invalid or expired.

The operator sets computed pt_mode = automatic to use the automatic pressure/temperature correction factor, and computed pt_mode = manual to use the correction factor that is based on the manually entered values (8.9.13, 214, fifth paragraph).

$\begin{axdef}$
		automatic, manual: VALUE
	$\end{axdef}$

The ScanPT operation computes the correction factors and updates the registers with the new values.

$\begin{schema}{$		ScanPT



		$\Delta$ Field

	$\where$

		calibrated' pt_factor = pt_formula(calibrated press,calibrated temp)
		computed' pt_factor = pt_formula(computed press,computed temp)

		(let pt_corr == if computed pt_mode = automatic
		then calibrated' pt_factor else computed' pt_factor
		computed' calvolt1 = pt_corr * calibrated calvolt1 $\land$
		computed' calvolt2 = pt_corr * calibrated calvolt2)

		{ pt_factor } $\ndres$ calibrated' = { pt_factor } $\ndres$ calibrated
		{ pt_factor, calvolt1, calvolt2 } $\ndres$ computed' = { pt_factor, calvolt1, calvolt2 } $\ndres$ computed

		prescribed' = prescribed
		accumulated' = accumulated
		overridden' = overridden

	$\end{schema}$

ScanPT is scheduled by the control program itself; it is not invoked by the user.

Software interlocks and status flags

User interface

The user may provide input at the workstation at any time (by typing, pressing function keys or cursor arrow keys --- in our implementation we do not use the mouse). We model each keystroke and the actions it invokes as an Event that accepts an input? that may change the Console state.

$\begin{schema}{$		Event



		$\Delta$ Console
		input?: INPUT

	$\end{schema}$

We do not attempt to formalize any ``look and feel'' aspects of the user interface, such as the appearance of the display. They are already described in sufficient detail in [jacky92], chapters 2 and 8.

INPUT is the set of inputs (keypresses) the user can provide (In the implementation, inputs are X window system events and the values of INPUT correspond to X keysyms [nye88].). Here is the list of inputs at this writing.

left_arrow | right_arrow | up_arrow | down_arrow | ignored

Many operations are invoked by pressing keys, so it is often convenient to identify operations with the corresponding input. Therefore we assign them to the same type. Here is the list of operations at this writing.

$\begin{axdef}$
		OP: $\power$ INPUT

	$\where$

		OP = { filter_wedge, leaf_collim, dose_intlk, gantry_psa, dose_cal,
		startup, help, messages, select_patient, select_field, field_summary,
		login, edit_setting, edit_dose_reg, log_message, store_field, override_cmd,
		cancel_run, password,auto_setup, expt_mode, cancel, refresh, shutdown, select )
	$\end{axdef}$

The user interface shows many displays, for example the login display (Fig 8.1, 178), the patient list display (Fig. 8.2, 185), the leaf collimator display (Fig. 8.7, 197) etc. The operator can choose any display by pressing a key, so we can identify displays with these operations.

$\begin{axdef}$
		DISPLAY: $\power$ OP

	$\where$

		DISPLAY = { filter_wedge, leaf_collim, dose_intlk, gantry_psa, dose_cal,
		startup, help, messages, select_patient, select_field,
		field_summary, login )
	$\end{axdef}$

Console state

The first variable indicates the mode of interaction. If no interaction is in progress the console is available, or there may be a dialog in progress where the user is typing text into a dialog box, or there may be a menu displayed, or the user may be asked to confirm some operation by providing a yes/no answer (this mode can also be used to present informational messages).

INTERACTION ::= available | dialog | menu | confirm

The op variable keeps track of which top-level operation (described in [jacky92]) is underway.