This paper describes an experiment in the formal verification of ?-charts, a Statechart-like language with instantaneous communication. Properties of ?-charts are verified using a theory of chart refinement. By modelling ?-charts in the language of CSP, used here as a semantic metalanguage, chart refinement is reduced to CSP trace refinement, which allows verification to be executed automatically using the model-checker FDR. A detailed verification of a motor vehicle central locking system is used to illustrate this approach. Results so far are promising, with the augmentation of a Statechart-like language with a refinement theory offering a more integrated method of reactive system design.