Here is the rationale for this Z specification.

Created from this LaTeX source with the Z2HTML translator.

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

#### Formal specification of control software for a radiation therapy machine

Jonathan Jacky, Michael Patrick and Jonathan Unger

January, 1997

Abstract

This report presents a formal (mathematical) specification for the operator's console of a computer-controlled radiation therapy machine equipped with a multileaf collimator. This formal specification, rather than the prose specification, serves as the primary reference source for programming and test planning.

Specified functions include selecting treatment setups from a database of stored prescriptions, setting up prescriptions on the treatment machine manually or semi-automatically, checking that the setup conforms to the prescription (with provision for overriding certain settings, with operator confirmation), safety interlocking and essential user interface features. The specification supports physics and experimental procedures as well as normal patient treatments.

The specification is expressed in the Z notation. It formalizes the requirements in a thorough informal (English prose) specification. Its organization suggests a detailed design.

## Introduction

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.

 TherapyControl Session Field Intlk ... Console

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

 ITEM ::= nfrac | dose_tot | dose | wedge | w_rot | filter | leaf0 | leaf39 | gantry | collim | turnt | lat | longit | height | doseB | top | pt_mode | pt_factor | press | temp | d_rate | t_fac | 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.).

 setting, dose_reg: ITEM

At this writing

 setting, dose_reg 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.

 scale, selection, counter: ITEM

At this writing

 selection, scale, counter 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 {wedge, w_rot, filter } motion == preset { gantry, collim, turnt, lat, longit, height } prescrip == motion counter prescr == prescrip \ { lat, longit, height } sensor == setting \ { nfrac, dose_tot } cal_const == { d_rate, t_fac, calvolt1, calvolt2 }

### Values

The value of every item can be represented by a number.

 VALUE ==

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.

 blank: VALUE tol: scale VALUE valid: ITEM 1 VALUE s: ITEM blank valid s

## 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.).

We distinguish a special value to indicate that no name has been selected.

 no_name: NAME

 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.

 studies,patients: PATIENT no_patient studies no_patient patients

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 VALUE PRESCRIPTION == prescrip VALUE

 Preset: studies (FIELD PRESCRIPTION) Prescribed: patients (FIELD PRESCRIPTION) Accumulated: patients (FIELD ACCUMULATION) s: studies no_field dom (Preset s) p: patients no_field dom (Prescribed p) dom (Prescribed p) = dom (Accumulated p)

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

 exceeded _ : ACCUMULATION PRESCRIPTION counters: ACCUMULATION; fields: PRESCRIPTION exceeded(counters,fields) ( c: counter counters c fields c)

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).

 [OPERATOR]

 no_operator: OPERATOR operators, physicists: OPERATOR physicists operators

## 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

 SessionVars mode: MODE operator: OPERATOR patient: PATIENT field: FIELD names: PATIENT fields: FIELD PRESCRIPTION counters: FIELD ACCUMULATION operator = no_operator operator operators mode = experiment operator physicists names = if mode = therapy then patients else studies

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

 NoPatient SessionVars patient = no_patient field = no_field fields = counters =

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

 PrescribedPatient SessionVars patient no_patient patient names field = no_field field dom fields fields = if mode = therapy then Prescribed patient else Preset patient mode = therapy counters = Accumulated patient

Together these define the Session state.

 Session PrescribedPatient NoPatient

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

 InitSession NoPatient mode = therapy operator = no_operator

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).

 ExptModeS Session operator physicists NoPatient' (mode',names') = if mode = therapy then (experiment,studies) else (therapy,patients) operator' = operator

#### 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.).

 StoreFieldS Session field?: FIELD prescribed': PRESCRIPTION accumulated': ACCUMULATION patient no_patient field' = field? fields' = fields { field' prescribed' } mode = therapy counters' = counters { field' accumulated' } mode' = mode operator' = operator patient' = patient names' = names

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.

 NewOperator Session operator?: OPERATOR operator' = operator? operator' operators

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).

 Privileged NewOperator mode = therapy operator' physicists mode' = mode patient' = patient names' = names field' = field fields' = fields counters' = counters

 Unprivileged NewOperator mode = experiment operator physicists mode' = therapy NoPatient'

#### 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.

 SelectPatientS Session patient?: PATIENT patient? names patient' = patient? field' = no_field fields' = if mode = therapy then Prescribed patient' else Preset patient' mode = therapy counters' = Accumulated patient' mode' = mode operator' = operator names' = names

#### 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.

 SelectFieldS Session field?: FIELD patient no_patient field? dom fields field' = field? operator' = operator mode' = mode patient' = patient fields' = fields counters' = counters

## 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.

 cal_factor: cal_const VALUE

 Field prescribed: PRESCRIPTION accumulated: ACCUMULATION measured: sensor VALUE overridden: prescr VALUE computed, calibrated: dose_reg VALUE

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]).

 PrescribedField Field Session field no_field mode = therapy prescribed = fields field

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 == ( p: prescrip blank) no_counter == ( c: counter blank) no_dose_reg == ( d: dose_reg blank) no_dose == { p_dose blank, p_time blank }

 NoFieldF Field prescribed = no_prescrip accumulated = no_counter no_dose computed overridden =

 NoFieldS [ Session | field = no_field ] NoField NoFieldF NoFieldS

FieldSession expresses the combined invariant:

 FieldSession PrescribedField 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.

 InitField NoFieldF computed = calibrated = no_dose_reg cal_factor

### 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.

 SelectPatientF Field NoFieldF' computed' = computed no_dose calibrated' = calibrated

#### 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.

 NewFieldF FieldSession prescribed' = fields field' overridden' =

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).

 SelectExptFieldF NewFieldF mode = experiment computed' = computed calibrated' = calibrated

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

 t_backup: (DOSE RATE FACTOR) TIME d: valid dose; r: valid d_rate; f: valid t_fac (d,r,f) dom t_backup t_backup(d,r,f) valid p_time

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).

 DoseTime Field (let t == t_backup(computed' p_dose,computed' d_rate,computed' t_fac) calibrated' = calibrated {  p_time t }) computed' p_time = calibrated' p_time { p_dose, p_time } computed' = { p_dose, p_time } computed

 NewTherapyField NewFieldF DoseTime mode = therapy accumulated' = counters field'

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).

 SelectTherapyFieldF NewTherapyField computed' p_dose = prescribed dose - accumulated dose overridden' =

Together these make the simple case

 SelectSimpleFieldF SelectExptFieldF 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).

 SelectComplexFieldF NewTherapyField dose?: VALUE computed' p_dose = dose? (let ovr == ( c: counter | accumulated' c prescribed' c accumulated c) overridden' = if dose? = prescribed' dose then ovr else ovr { dose dose? })

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

The edit operation updates a prescribed or computed item value.

 EditF Field item?: ITEM value?: VALUE accumulated' = accumulated calibrated' = calibrated

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.

 EditPresetF EditF item? preset prescribed' = prescribed { item? value? } overridden' = { item? } overridden computed' = computed

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.

 EditCalF EditF item? dose_reg \ { p_dose, p_time } computed' = computed { item? value? } prescribed' = prescribed overridden' = overridden

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.

 EditDoseF EditF DoseTime item? = p_dose computed' p_dose = value? overridden' = overridden { dose value? } prescribed' = prescribed

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.

 EditTimeF EditF item? = p_time computed' = computed { p_time value? } prescribed' = prescribed overridden' = overridden

Here is the combined operation:

 EditSettingF EditCalF EditPresetF EditDoseF 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

Certain items can be overridden.

 OverF Field item?: ITEM prescribed' = prescribed accumulated' = accumulated computed' = computed calibrated' = calibrated

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.

 OverrideSetting OverF item? prescr overridden' = if item? dom overridden then overridden { item? measured item? } else { item? } overridden

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.

 OverrideDose OverF item? { p_dose, p_time } overridden' = if dose dom overridden then overridden { dose accumulated dose } else { dose } overridden

 OverrideF OverrideSetting 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 == ( c: counter 0)

 StoreFieldF FieldSession computed' = computed no_dose prescribed' = prescribed (prescrip measured) no_counter { nfrac 1 } accumulated' = zero_counter overridden' = calibrated' = calibrated

#### Experiment Mode

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

 ExptModeF Field NoFieldF' computed' = computed no_dose calibrated' = calibrated

### 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

 pt_formula: (PRESSURE TEMPERATURE) FACTOR p: valid press; t: valid temp (p,t) dom pt_formula pt_formula(p,t) valid pt_factor

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).

 automatic, manual: VALUE

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

 ScanPT Field 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 computed' calvolt2 = pt_corr * calibrated calvolt2) { pt_factor } calibrated' = { pt_factor } calibrated { pt_factor, calvolt1, calvolt2 } computed' = { pt_factor, calvolt1, calvolt2 } computed prescribed' = prescribed accumulated' = accumulated overridden' = overridden

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

## Software interlocks and status flags

(See the full report.)

## 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.

 Event Console input?: INPUT

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.

 INPUT ::= 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 | ret | character | backspace | delete_key | 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.

 OP: INPUT 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 )

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.

 DISPLAY: OP DISPLAY = { filter_wedge, leaf_collim, dose_intlk, gantry_psa, dose_cal, startup, help, messages, select_patient, select_field, field_summary, login )

### Console state

This section describes the variables in the 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.

The display variable indicates which of the screen designs pictured in the informal specification is currently visible on the display. The display variable determines which items appear and helps determine which operations are available.

The item state variable holds the item which the operator has selected from a tabular display, for example the setting which the operator is editing.

The nlist state variable holds the list of names (of patients or fields) that appear on a list display, and list_item indicates the currently selected name.

The menu_item state variable holds the index of the current menu selection (a small integer).

 nmax:

 SELECTION == { i: | i nmax }

The buffer state variable models the (possibly incomplete) string that the user edits in dialog mode.

 [STRING]

 empty: STRING

The keyswitch must be unlocked to allow the console to be used (8.7, 179).

 KEYSWITCH ::= locked | unlocked

Some operations are available only when a treatment is being set up, and are locked out while a treatment run is in progress (8.8.2, 183).

 RUN ::= setup | running

The keyswitch and run variables depend on sensor inputs; they are not constrained here.

Together, these variables describe the state of the user interaction.

 Console keyswitch: KEYSWITCH run: RUN display: DISPLAY op: OP interaction: INTERACTION item: ITEM nlist: NAME list_item: NAME menu_item: SELECTION buffer: STRING

When the control program starts up, the login process begins (section [sect:login-console]) (When the implementation starts up, the startup screen appears first. The login process does not begin until the various Init... conditions are established. We do not model this formally.).

 InitConsole Console op = login display = login interaction = dialog buffer = empty

### Elements of user interaction

All user interactions are built up from a few elements. In this section we define the constants, states and operations that serve as building blocks.

The caption type models messages or other output to the operator that appear temporarily at the console (in dialog boxes or perhaps even from the speaker, see 2.2.3, 9). Captions are distinguished from log messages which appear in a different location on the console and are also stored in log files along with timestamps other information (2.2.4, 9).

 [CAPTION, MESSAGE]

Ignore is the default do-nothing operation that is invoked when a key is pressed but the preconditions for the associated operation are not satisfied. Ignore does not change the state, but issues an alert (such as sounding the workstation bell) to notify the user that the input was received but the operation is not enabled.

 Ignore Event Console caption!: CAPTION caption! = alert

The keyswitch must be unlocked for any operation to occur. When the keyswitch is locked, input is ignored:

 Unlocked [  Console | keyswitch = unlocked  ] EventUnlocked Event Unlocked

Many operations are invoked by pressing the select key.

 Select [  EventUnlocked | input? = select  ]

It is convenient to describe the operations that can occur in each of the interaction modes. Each mode is described in a following subsection.

#### Available

Most of the top-level operations described in [jacky92] can only be selected when the console is available.

 Available [  Console | interaction = available  ]

 Op EventUnlocked Available input? OP

Certain operations have stronger preconditions: they cannot occur when a run is in progress (8.8.2, 183). A few operations occur only when a run is in progress (8.9.11, 209-210).

 Setup [  Available | run = setup  ] Running [  Available | run = running  ]

When the console is available, the user may select a new display. The console remains available.

 SelectDisplay Op input? DISPLAY display' = input? op' = display' Available'

SelectDisplay operations may change item and list_item (see below) but do not change other state variables (for brevity we omit the x' = x nothing changes'' predicates).

When an interaction is in progress, the console is Engaged. The Done operation schema describes what happens when an interaction completes: the console returns to the Available state, and op returns to its value when the display was selected.

 Engaged [ Console | interaction available ]

 Done EventUnlocked Engaged op' = display display' = display Available'

The Cancel operation is used to end an interaction without making permanent changes to the underlying machine state.

 Cancel [ Done | input? = cancel ]

#### Lists

Certain displays show a list of names (patients or fields). When a list display is selected, nlist is loaded, and the default list_item is assigned. If the list is not empty, the List state results (the patient list might be empty if there are no patients on file; the field list is always empty when there is no patient, and may be empty if there are no fields on file for the selected patient).

 list: DISPLAY default_name: 1 NAME NAME list: 1 NAME default_name list list

 List [  Available | display list nlist list_item nlist  ]

 SelectList SelectDisplay input? list ((nlist = list_item' = no_name) (List' list_item' = default_name nlist'))

Here display list nlist distinguishes the List state, and this test occurs explicitly in the implementation. In contrast, list_item nlist is an invariant. It need not be coded as an explicit test but it must be maintained or else the implementation might abort (because list_item is used as an index into nlist).

The console indicates list_item (for example by placing a highlight or cursor over that name in the list). Subsequently the user can choose a new name from the list by using the up and down-arrow keys. The function aname calculates the new name by dead reckoning'' from the old name, the list, and the arrow key (it is not necessary for the program to poll the console for the cursor position). The list remains visible.

 v_arrow == { up_arrow, down_arrow }

 aname: (v_arrow NAME 1 NAME) NAME a: v_arrow; n: NAME; list: 1 NAME aname(a,n,list) list

 Continue [  Console | interaction' = interaction op' = op display' = display  ]

 GetListArrow EventUnlocked List input? v_arrow list_item' = aname(input?,list_item,nlist) Continue

This is a Continue operation that does not change interaction, op, or display. Here list_item is the only state variable that changes. We do not completely specify default_name and aname; we leave that to the implementation. Here we merely provide the predicates needed to ensure that the implementation does not abort.

The user presses the select key to choose the current list_item for some purpose. The selection is logged; nmessage converts the name to a log message.

 selected_msg: NAME MESSAGE

 SelectName Select name!: NAME message!: MESSAGE List name! = list_item message! = selected_msg name!

GetListArrow and SelectName are not total operations; they do not handle the case where nlist = . The latter case is handled by a default do-nothing operation, IgnoreOthers, which includes Ignore. We do not define the precondition of this operation explicitly; we code the implementation so control reaches IgnoreOthers when no other operations are enabled.

#### Tables

Certain displays show a table of items (settings for one subsystem, calibration factors etc.). The constant table_items tells which items on each table can be selected for editing or overriding (additional items may be displayed as well). When a tabular display is selected, the default item is assigned, and the Table state results.

 table: DISPLAY

 default_item: table ITEM table_items: table 1 ITEM d: table default_item d table_items d

 Table [  Available | display table item table_items display  ]

 SelectTable SelectDisplay input? table item' = default_item display' Table'

Subsequently the user can indicate a new item on the table by using all four arrow keys.

 arrow == { right_arrow, left_arrow } v_arrow

 asetting: (arrow ITEM table) ITEM a: arrow; s: ITEM; d: table asetting(a,s,d) table_items d

 GetSettingArrow EventUnlocked Table input? arrow item' = asetting(input?,item,display) Continue

Here item is the only state variable that changes.

Items can be selected from tabular displays for editing or overriding. Editing or overriding is only enabled in the Setup state (when a treatment run is not in progress, see 8.8.2, 183). Pressing the select key when certain tabular displays are present invokes an editing operation: edit_setting if the selected item is a setting and edit_dose_reg if it is a dose_reg (notice that here op' is not the same as input?). Therefore it is necessary to separate setting and dose_reg items on different tables (Because the implementation cannot distinguish setting from dose_reg based on item alone; item values are just C enum values (integers).).

 setting_table, dose_reg_table: table d: setting_table table_items d setting d: dose_reg_table table_items d dose_reg

 SelectItem Select Setup Table item' = item (op' = edit_dose_reg display dose_reg_table op' = edit_setting display setting_table)

The postcondition here implies Editing, the invariant of the editing state (The implementation uses op to determine whether item is an index into setting or dose_reg.).

 Editing Console interaction { dialog, menu } (op = edit_dose_reg item dose_reg op = edit_setting item setting)

The Setup precondition of SelectItem prevents the console entering the Editing state when a run is in progress. Other mechanisms prevent the machine from beginning a run while in the Editing state.

#### Confirm

Confirm interactions present a query (Are you sure ... ?'') and wait for the user to provide a yes/no answer, indicated by the select or cancel keys (for example see 8.9.11, 210). Each Confirm operation presents a confirmation box (a sort of dialog box) with a caption that identifies the operation, and the query. The display under the confirmation box does not change.

 Confirm [  Console | interaction = confirm  ]

 ocaption: OP CAPTION

 ConfirmOp Op caption!, query!: CAPTION caption! = ocaption op' display' = display Confirm'

 AcceptConfirm Confirm Select Done

When the console is Available the user can invoke a menu, then make a selection from the menu. Each menu includes a caption and a list of menu entries. The display does not change.

 default_selection: SELECTION

Here op also changes; the other state variables retain the same values.

Menus are used to choose new values for selection items; valid selection values are small integers. Combining MenuOp with SelectItem yields the MenuEdit operation. The menu shows the item name and a sequence of descriptive strings indexed by the corresponding item values. Here again, the Editing postcondition of SelectItem guarantees that op can be used to help look up selection_values item.

 setting_info_name: ITEM CAPTION setting_value: selection iseq CAPTION s: selection dom (setting_value s) = valid s

There are functions to return the default menu selection and the new selection after each up or down-arrow keypress.

 amenu: (v_arrow SELECTION selection) SELECTION s: selection (let n == # (valid s) a: v_arrow; i: SELECTION default_selection n amenu(a,i,s) n)

Here item is the only variable that changes.

The user presses select to accept the current menu item and the console becomes available again.

#### Dialog

When the console is Available the user can begin a dialog, then type and edit text in a dialog box. The dialog box contains a caption and a prompt that may include the values of other state variables. The display under the dialog box does not change.

 Dialog [  Console | interaction = dialog  ]

 DialogOp Op caption!, prompt!: CAPTION caption! = ocaption op' display' = display Dialog'

Here only interaction, buffer, and op change. The buffer may be emptied, or may be filled with a convenient default value. We'll describe changes to op later, with each dialog operation.

The console remains in Dialog while the user types and edits. The GetChar operation gets a single character and updates the buffer as described by the modify function (append printing characters to the end of buffer, and do the appropriate things with editing characters).

 CHAR: INPUT

 modify: (STRING CHAR) STRING

Here buffer is the only variable that changes.

When a dialog is done, the dialog box disappears and the console becomes available again. At any time the user can cancel the dialog and discard the input. To submit the input, the user presses a terminator key; the program can Accept the input or Reprompt (the user may also Cancel the dialog).

 terminator: INPUT

Here again, buffer is the only variable that changes.

Dialogs are frequently used to edit item values. Combining DialogOp with SelectItem yields the DialogEdit operation. Dialog box editing begins if the selected item is not a selection (does not have just a few discrete values). The program captions the dialog box with the item name and the minimum and maximum valid item values (The dialog box caption also includes the units, but we do not model this formally.).

 MIN == VALUE; MAX == VALUE

 setting_info: ITEM MIN MAX CAPTION

 DialogEdit DialogOp SelectItem item selection prompt! = (let v == valid item setting_info(item, min v, max v))

The implementation uses the value of op guaranteed by the Editing postcondition of SelectItem to look up valid item; there are separate valid arrays for dose_reg and setting.

When the user presses a terminator key, the program attempts to convert the buffer contents to a (numeric) value (non-numeric strings are always converted to an out-of-range value). If the conversion succeeds and the value is valid for the item, the dialog ends and the item and its value are reported; otherwise, the program reprompts.

 sval: STRING VALUE

 EditSettingC Accept item!: ITEM value!: VALUE Editing item! = item (let v == sval buffer v valid item value! = v)

 InvalidSetting [  Reprompt | Editing sval buffer valid item  ]

In the implementation it is convenient to combine these two operations (In EditOrInvalidSetting, the two outputs item! and value! are not used in the Invalid case.).

 EditOrInvalidSetting EditSettingC InvalidSetting

### Therapy console operations

In this subsection we present the operations described in [jacky92]. Several building block operations require no further elaboration: SelectDisplay, SelectTable, GetListArrow, GetSettingArrow, Cancel, GetMenuArrow, MenuSettingC, GetChar, and EditOrInvalidSetting and are already complete. Others require further specialization in the following subsections.

#### Relation to Session state

A few Console operations read (but do not change) variables from the Session state (section [sect:session]). When the Console shows the patient or field list, its nlist state variable holds the patients or fields from the Session state. This is expressed by the ConsoleSession invariant:

 ConsoleSession Console Session display = select_patient nlist = names display = select_field nlist = dom fields

#### Op operations

Several operations are based only on Op. They are Continue operations because they do not involve any ongoing interaction, just a single keypress.

 SimpleOp Op Continue

Experiment Mode (8.9.6, 190):

 ExptModeC SimpleOp Session ConsoleSession Setup input? = expt_mode operator physicists

Auto Setup (8.8.1, 181):

 auto_setup_display == { field_summary, filter_wedge, leaf_collim, dose_intlk }

 AutoSetupC SimpleOp ConsoleSession subsystem!: auto_setup_display Setup field no_field display auto_setup_display input? = auto_setup subsystem! = display

#### SelectDisplay operations

There are a few simple displays that provide no selections or interactive editing, Field Summary (8.9.7, 191) and the help display (not discussed in [jacky92]

 simple_display == { field_summary, help }

#### SelectList operations

The specializations of SelectList are Select Patient (8.9.3, 184) and Select Field (8.9.4, 186). The latter operation only makes sense when a patient has been selected:

 list = { select_patient, select_field }

 SelectPatientList SelectList Session ConsoleSession input? = select_patient nlist' = names

 SelectFieldList SelectList Session ConsoleSession patient no_patient input? = select_field nlist' = dom fields

#### SelectTable operations

The table displays are Gantry/PSA (8.9.8, 193), Filter/Wedge (8.9.9, 194), Leaf Collimator (8.9.10, 196), Dosimetry/Therapy Interlocks (8.9.11, 199) and Calibration Factors (8.9.13, 213):

 table = { gantry_psa,filter_wedge,leaf_collim,dose_intlk,dose_cal }

The constant table_items tells which items on each table can be selected for editing or overriding (additional items may be displayed as well).

 table_items  = { gantry_psa { gantry, collim, turnt }, filter_wedge { filter, wedge, w_rot }, leaf_collim leaves, dose_intlk { p_dose, p_time }, dose_cal { pt_mode,press,temp,d_rate,t_fac } }

It is necessary to separate setting and dose_reg items on different tables:

 setting_table = { gantry_psa,filter_wedge,leaf_collim } dose_reg_table = { dose_intlk, dose_cal }

Now that these constants are defined, the previously defined SelectTable operation requires no further specialization.

#### ConfirmOp operations

To begin Cancel Run (8.9.11, 209 -- 210):

 cancel_run_query: CAPTION

 SelectCancelRun ConfirmOp Running input? = cancel_run op' = input? query! = cancel_run_query

The complementary AcceptConfirm operation is CancelRunC (below).

At this writing there are no simple MenuOp operations, only MenuEdit operations (under Setup, below).

#### DialogOp operations

 type_message_prompt, store_field_prompt: CAPTION

To begin Write Log Message (2.5.1, 17):

 TypeMessage DialogOp input? = log_message op' = input? prompt! = type_message_prompt

To begin Store Field (8.9.5, 189 -- 188):

 EditField DialogOp Setup input? = store_field op' = input? prompt! = store_field_prompt

These two operations are completed by the complementary Accept operations, WriteMessageC and StoreFieldC (below).

#### Setup operations

Under Setup, there are SelectName, SelectItem, MenuEdit and DialogEdit operations.

Select Patient (8.9.3, 184 -- 185):

 SelectPatientC SelectName Setup display = select_patient Continue

At this writing, SelectPatient is a Continue operation; the patient list remains on the screen (We also considered establishing display' = select_field in SelectPatientC. It would not be difficult to adopt this alternative later.).

SelectField (8.9.4, 186 -- 189): There are three cases. The simplest case occurs during experiment mode, or when the chosen field has not yet been delivered today and the prescribed total dose and number of fractions has not yet been exceeded (8.9.4, 187).

 NewFieldC SelectName ConsoleSession Setup display = select_field

 SelectSimpleFieldC NewFieldC mode = experiment (counters name! dose = 0 exceeded(fields name!, counters name!)) Continue

The more complicated cases arise in therapy mode when the operator must be warned of some unusual condition (8.9.4, 187-188). These are DialogOp operations. The name of the new field must be stored during the dialog. The operator may enter a preset dose or cancel the dialog (so no new field is selected).

 Console1 ConsoleSession new_field: FIELD new_field dom fields

 DoseDialogOp NewFieldC DialogOp Console1 op' = select_field new_field' = name! mode = therapy

There are two such cases. The first arises when the same field has already been delivered on the same day but the prescribed daily dose has not yet been reached; the remaining dose is offered as the default (8.9.4, 187):

 sprintf: VALUE STRING delivered_prompt: NAME VALUE VALUE VALUE CAPTION

 SelectDeliveredField DoseDialogOp counters new_field' dose > 0 exceeded(fields new_field', counters new_field') (let d == fields new_field' dose; c == counters new_field' dose (let default_dose == d-c buffer' = sprintf default_dose prompt! = delivered_prompt(new_field', d, c, default_dose)))

The other case arises when the daily dose, the total dose or the number of fractions has been exceeded (8.9.4, 188). No default dose is provided.

 exceeded_prompt: NAME ACCUMULATION ACCUMULATION CAPTION

 SelectExceededField DoseDialogOp exceeded(fields new_field', counters new_field') prompt! = exceeded_prompt(new_field', fields new_field', counters new_field') buffer' = empty

The complete operation is composed of all these cases.

 SelectFieldC SelectSimpleFieldC SelectDeliveredField SelectExceededField

After SelectSimpleFieldC, nothing more need be done. SelectExceededField and SelectDeliveredField are succeeded by the SelectFieldOp state, which is handled by the SelectComplexFieldS operation.

 SelectFieldOp Console1 Dialog op = select_field

Override (8.4, 175; 8.8.1, 181; 8.8.2, 183) is also a ConfirmOp operation, enabled only when a field has been selected. The name of the item that the operator selected is echoed in the confirmation dialog. To begin Override:

 override_table == { filter_wedge, leaf_collim, gantry_psa, dose_intlk }

 override_query: CAPTION CAPTION

 SelectOverride ConfirmOp SelectItem Session field no_field display override_table input? = override_cmd op' = input? query! = override_query(setting_info_name item)

The complementary AcceptConfirm operations is OverrideC (below).

Edit: There are three cases. Calibration factors can be edited in experiment mode (8.9.13, 215), preset dose and time can be edited in both modes when a field is selected (8.9.11, 201--202), and other preset items can be edited in experiment mode when a field is selected (8.8.1, 180--181; 8.9.8, 194; 8.9.9, 196; 8.9.10, 198).

 cal_table == { dose_cal } dose_table == { dose_intlk } preset_table == { filter_wedge, leaf_collim }

 CalTable [  ConsoleSession | mode = experiment display cal_table  ]

The precondition field no_field occurs elsewhere so it is convenient to collect two cases together.

 SettingTable ConsoleSession display dose_table (mode = experiment display preset_table)

Finally

The complementary operations are EditSettingC and MenuSettingC (section [sect:gui-elts], above).

#### Cancel operations

There is a special cancel operation for the login process (below) so we have to strengthen the preconditions on Cancel:

 LoggedIn [ Console | op { login, password } ] CancelOp LoggedIn Cancel

#### AcceptConfirm operations

To complete Override (8.4, 175; 8.8.1, 181; 8.8.2, 183):

 OverrideC AcceptConfirm item!: ITEM op = override_cmd item! = item

To complete Cancel Run (8.9.11, 209 -- 210):

 CancelRunC [  AcceptConfirm | op = cancel_run  ]

#### Accept operations

To complete Write Log Message (2.5.1, 17). The smessage function turns a string into a log message by prepending the timestamp and other information.

 log_msg: STRING MESSAGE

 WriteMessageC Accept message!: MESSAGE op = log_message message! = log_msg buffer

To complete Store Field (8.9.5, 189 -- 188) (The message! output from StoreFieldC is not mentioned in [jacky92]; here we correct the omission.).

 sname: STRING NAME store_msg: NAME MESSAGE

 StoreFieldC Accept field!: NAME message!: MESSAGE op = store_field field! = sname buffer message! = store_msg field!

The complex variants of Select Field (8.9.4, 187--188) are handled by SelectComplexFieldC, which is similar to EditSettingC:

 SelectComplexFieldC Console1 Accept field!: FIELD dose!: VALUE SelectFieldOp field! = new_field (let d == sval buffer d valid dose dose! = d)

We have to make the operation total

 InvalidDose [  Reprompt; Console1 | SelectFieldOp sval buffer valid dose  ]

 ComplexOrInvalidField SelectComplexFieldC InvalidDose

The Login process (Fig. 2.6, 19) can be seen as editing the value of operator. Messages are logged at logout and login. Logout (2.5.2, 17 -- 18; 8.9.2, 184) is is similar to SelectDisplay and DialogOp; it reads Session for the operator's ID in the logout message.

 o_msg, lo_msg: OPERATOR MESSAGE

 Logout Op Session message!: MESSAGE Setup input? = login display' = input? op' = display' buffer' = empty message! = lo_msg operator Dialog'

A successful Login (2.5.2, 17 -- 20; 8.9.1, 183) occurs when a user enters a valid operator identification. The process of logging back in is broken into two steps. In the first step, the user types their username into the buffer. When the user types a terminator the username is saved in another buffer; the Console1 state is Console with this buffer added (The password is also typed into buffer so the GetChar operation can be used.). The console remains logged out after this step. This EnterUsername operation is similar to Accept and Continue.

In the second step, the user enters their password. If their username, password pair is found in operator database, the user is logged in, the help screen is displayed, and the console becomes available. This LoginC operation is similar to Accept and SelectDisplay.

The operator authorization file is modelled by Z global constants operators and physicists (physicists are authorized to use the equipment in its experiment mode, see 8.2, 170). Values of OPERATOR include the operator's password in addition to the operator's printed name.

 LoginC Console2 EventUnlocked operator!: OPERATOR message!: MESSAGE op = password soper(username, buffer) operators input? terminator display' = help op' = display operator! = soper(username,buffer) message! = o_msg operator! Available'

#### Other operations

Several operations not described in [jacky92] are included for development purposes (Shutdown will not be included in production versions.). They are always enabled.

 Refresh [  Event | input? = refresh  ] Shutdown [  Event | input? = shutdown  ]

This concludes our presention of the states and operations in the user interface.

## Combining the subsystems

In this section we combine related operations from the Console, Session and Field subsystems. In cases where no data is transferred between subsystems, we can simply conjoin the separate operations:

 ExptMode ExptModeC ExptModeS ExptModeF

Here the conjunction just expresses that the named operations in all three subsystems are triggered by the expt_mode input at the console. In this report both ExptModeC and ExptModeS contain the precondition operator physicists, but this predicate only needs to appear once; we include it in both schemas for clarity (In our implementation, we observe the convention that preconditions of combined operations are always tested in the Console operations. For example operator physicists is tested by code in zconsole.c, not zsession.c.).

In other cases, data is transferred. For example, in the Override operation, the item! output from the Console subsystem is consumed by the item? input in the Field subsystem (the Session subsystem does not participate in this operation). We wish to express

 Override OverrideC OverrideF item! = item?

This can be expressed more concisely using the Z pipe operator >>, which has the effect of connecting corresponding input and output variables ([spivey92], p. 78) (The Z pipe operator also hides the piped variables.).

 Override OverrideC >> OverrideF

In Login, the new operator name operator!/operator? is the piped variable.

In EditSetting, both the item name item!/item? and the new setting value value!/value? are piped:

 EditSetting EditSettingC >> EditSettingF

Sometimes the output from the Console subsystem is piped to inputs in both the Session and Field subsystems. In StoreField, the new field name field! / field? is the piped variable:

 StoreField StoreFieldC >> (StoreFieldS StoreFieldF)

Here the conjunction StoreFieldS StoreFieldF ensures that prescribed' in fields' = fields { field' prescribed' } from StoreFieldS is the same as prescribed' in prescribed' = prescribed measured ... from StoreFieldF.

In SelectPatient, the new patient name patient!/patient? is the piped variable (patient? does not appear in SelectPatientF).

 SelectPatient SelectPatientC >> (SelectPatientS SelectPatientF)

There are two variations of SelectField. In both variants field!/field? is piped from the SelectFieldC variant to SelectFieldS. In the complex variant, dose!/dose? is piped from SelectComplexFieldS to SelectComplexFieldF.

 SelectSimpleField SelectSimpleFieldC >> (SelectFieldS SelectSimpleFieldF) SelectComplexField SelectComplexFieldC >> (SelectFieldS SelectComplexFieldF)