Correction Sheet

After our paper "Proving Safety Properties of the Steam Boiler Controller" went already to print, Myla Archer and Constance Heitmeyer verified the lengthy lemmas and theorems with the theorem prover PVS. Unfortunately, several errors were found in the proofs. No major changes were done to the model. An updated version of both papers is available under http://groups.csail.mit.edu/tds/papers/Leeb/boiler.html.

Following are the corrections to these errors and some typing errors for the full version of the paper (on the LNCS CD-ROM):

  1. p. 7: Lemma 1.2 is incorrect. It should be:

    2. Consequent changes in the proofs which use this information are straight forward. The information is used only in Lemma 13 and Theorem 2

  2. p. 7: Lemma 1.3 is imprecise. It should be:

    3. Consequent changes in the proofs which use this information are straight forward. Only slight modifications to the simulation proof are necessary.

  3. p. 7: Disregard Lemma 1.7: W-U1 should be W-U1*I and requires W >= U1*I but this lemma is never used by any of the proofs.
  4. p. 7, Some relations are missing between constants:
    1. 0 =< M1< M2 =< C
    2. S < I
  5. p. 8, error should be cleaner defined: error in the range [0 . . . #pumps] instead [0 ... pr_new]
  6. p.12: min_steam_water(sr) is wrong defined:

  7. p.12, We introduce min_steam_water_est(sr) used in the fault-tolerant controller:

  8. p. 13, The inital state of stopmode is true so that Lemma 3 is correct in the initial state.
  9. p. 13 & p.15, In the sensor action

    10. if sr' <= W - U1 * I or ... should be if >= sr' W - U1 * I or ...

  10. p.15, In the activate action: error should be error'
  11. p.19: Lemma 12 should be:

    12. if do_output = false then
    if set = read - I +S then
    M1 < q + P*pumps*(set-now) - (v * (read-now) + U1*(read-now)2/2) or stop = true
    else M1 < q - (v * (read-now) + U1*(read-now)2/2) or stop = true

  12. p.20: Lemma 13 should be:

    13. if do_output = false then
    if set = read - I + S then
    M2 > q + P*(pumps*(set-now) + #pumps*(I-S)) - steam or stop = true
    else M2 > q + P*#pumps*(read - now) - steam or stop = true

  13. p.21, Consequentially, the proof to Theorem 2 changes. Its detail can be found in the full version of the paper. Moreover, Theorem 2 needs following additional information:

    14. d(u) >= min(0, d(S)) for S >= u >= 0, d(u) = A*u - B*u2 with A real and B positive real

  14. p.24, The estimated water level in the sensor action should be more precise:
    Use min_water_level_est(srl') instead (max(0, srl' - U1*I/2))*I.
  15. p.24, In the sensor action wl_ok’ and sr_ok’ should be wl_ok and sr_ok since they are not changed.
  16. p.26ff. The simulation proof require slight modifications to accommodate changes in Lemma 1.3 and the introduction of min_water_level_est.

We want to excuse for these errors and to thank Myla Archer and Constance Heitmayer for their help in identifying most of them.