[CSUSB]>> [CNS]>> [CSE]>> [R J Botting]>> biba.php

Bibliographic Item (1.0)

Jacky95

  1. Jonathon Jacky
  2. Specifying a Safety-Critical Control System in Z
  3. IEEE Trans on Software Eng VSE-21n2(Feb 1995)pp99-106 CR9605-0354 D.2.1
      p105: "We have already found the formal texts to be useful as descriptive documentation. We hope that their brevity will help us build an econmical implementation. The possiblity that they might also support safety amalyses and formal development of the implementation is an additional bonus".

      p105: "User attempt operations that are interlocked... Users may select operations in any sequence they wish, subject only to the sequencing constraints imposed by the preconditions. There is no 'flow of control'". Interlock Preconditions Some safety conditions need special treament because they depend on variables(sensor inputs) that are inputs and so not under constraint - and so not constrained in a precondion (or post-condition).

      Op=Safe_Op or Invariant(System).

    1. Safe_Op::= Dangerous_Op and Pre_Safe_Condition_for_Op.
    2. Pre_Safe_Condition_for_Op::= for some State'( Dangerous_Op & Invariant(Sensors)).
    3. For S, Invariant(S)::=(S'=S). Notice that Invariant(Sensors) do not appear directly in the Ops, only inconjunction with them, and then hidden in a quantifier.

      May need to add extra interlocks on transitions that are not in raw requirements.

      Did not need an OO version of Z. Defined classes of components all sharing a common schmer and separted by their identifiying names.

      Useful Idioms: promotion, multiple comp ops,



Search for bibliographic items containing a matching string.


(Search uses POSIX regular expressions and ignores case)

Search for a specific bibliographic item by name.



To see the complete bibliography (1Mb+) select:[Bibliography]