Retrenchment, with its capacity to distinguish well behaved from exceptional cases, is ideally suited to formalise various kinds of safety analyses in a uniform and mutually compatible way. The details of this have been worked out for fault tree analysis, and a half day tutorial on this work can be accessed below.
The tutorial is presented in two ways. The first way is as a single pdf file (together with a 4-up printable version, without overlays, alongside). Since some of the pdf was generated from Powerpoint and is consequently bulky, and slow on less powerful machines, the tutorial is also presented a second way, in three pieces: the first and third pieces being Powerpoint, and the middle piece being pdf.
The Mechanical Generation of Fault Trees for State Transition Systems ..................... 4-up printable: pdf
The Mechanical Generation of Fault Trees for Reactive Systems
via Retrenchment I: Combinational Circuits.
R. Banach, M. Bozzano
Form. Asp. Comp., (to appear),
Preprint: Retrench.FT.ReaSys.I.Comb.ps.gz .......... Retrench.FT.ReaSys.I.Comb.pdf
(Does what it says on the tin for combinational circuits.)
The Mechanical Generation of Fault Trees for Reactive Systems
via Retrenchment II: Clocked and Feedback Circuits.
R. Banach, M. Bozzano
Form. Asp. Comp., (to appear),
Preprint: Retrench.FT.ReaSys.II.TimCy.ps.gz .......... Retrench.FT.ReaSys.II.TimCy.pdf
(Does what it says on the tin for clocked and cyclic digital circuits.)