Erratum

In Section 19.1.1, it is claimed that failures-divergences refinement and relational refinement are identical. This is not the case: the (only) difference is in the upwards applicability rule, which in the relational case is

$$\forall CState;i:I \exists AState \dot T \wedge \cdots$$

but for failures-divergences (and according to Josephs [134]) is

$$\forall CState \exists AState \dot T \wedge \forall i:I \dot \cdots$$