Safety-critical interactive systems pose design and evaluation challenges that go beyond usability. The safety of the system (i.e. the guarantee that it does not reach an undesirable or incorrect state) is also a relevant consideration. Traditional user-centred approaches (UCD) lack the rigour and thoroughness needed to address safety, and formal verification arises as a possible solution. Applying formal verification to a safety-critical interactive system design encompasses developing a model, expressing and verifying properties, and analysing the verification results. In the case of model checking, properties are typically expressed in temporal logic. This creates a gap between the languages used in UCD and the languages used for formal verification. Creating temporal logic properties manually requires expertise in formal methods and can be both time-consuming and error-prone. This paper explores how a patterns-based approach can be used to support the specification of properties in a natural language-based style. A prototype implementation of the approach is evaluated through a user study, and the results of this evaluation are discussed.