Formal verification of μ-charts

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.