Using B and RSDS for Reactive System Design

We use examples of reactive system specifications to demonstrate how the invariant-based specification approach of RSDS connects to safety analysis and to design and verification using the B method. Animation of specifications in B is introduced as a validation technique.