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 short version of the paper (published in the LNCS book):

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

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

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

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

  3. p. 6: 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 basic relations between constants are missing:
    1. 0 =< M1< M2 =< C
    2. S < I
  5. p. 7, error should be cleaner defined: error is in the range [0 . . . #pumps] instead [0 ... pr_new]
  6. p.10: min_steam_water(sr) is wrong defined:

    7. Lemma 3.1 is consequentally (whenever used in the described proofs):

    M2> wl + P * (pumps * S + #pumps * (I - S)) - min_steam_water(sr) or stopmode = true

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

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

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

  10. p.14: Lemma 12 should be:

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

  11. p.14: Lemma 13 should be:

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

  12. p.14, Consequentially, the proof to Theorem 2 changes. Its detail can be found in the correction to the full version. Moreover, Theorem 2 needs following additional information:

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

  13. p.16, 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.
  14. p.16, In the sensor action wl_ok’ and sr_ok’ should be wl_ok and sr_ok since they are not changed.

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