Using behavioural specifications to support model-checking

Safety-critical interactive systems provide many benefits for human daily life, but erroneous safety-critical interactive systems can lead to serious consequences to the users. Thus building these systems requires that we ensure a high level of correctness. Formal models can be used to ensure that safetycritical systems are developed correctly. However, when models of the systems are being built, there is no guarantee that the modelled system fully satisfies the user requirements. If the systems are not what business stakeholders truly desire, new errors can be made. Behaviour-Driven-Development is often applied to ensure the requirements of thesystemareproperlyunderstoodandmaintainedbyusingBehaviouralSpecifications. These specifications use natural language, and so, are well suited for expressing user requirements. They can be used as the basis for test generation but do not provide the guarantees of correctness that formal methods can provide. In this work, we develop an approach that takes advantage of the expressivity of behaviour specifications and combines it with the use of formal methods. We use Behavioural Specifications to create First-Order-Logic predicates of the requirements. These predicates can be used with formal methods, either to support the creation of the formal models or to ensure the user requirements and specifications are consistent