Behaviour-driven development and formal methods have been shown to be effective techniques for different parts of the interactive system development process. However, when the different parts of an interactive system are combined, issues may arise due to the different focuses of the techniques. For a safety-critical interactive system, where safety is particularly emphasised, using either technique individually does not cover all aspects of the system. Thus a complementary approach of integrating behaviour-driven development and formal methods, would be better suited for developing safety-critical interactive systems. This thesis presents an investigation into a method that integrates formal methods and behavioural specifications. This method enables the identification of any inconsistencies between the behavioural specification and the Z specification, allowing potential problems to be found and fixed earlier. We also demonstrate how our method supports ensuring consistency after refinement of the Z specification.