| Abstract |
|
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.
|
 Additional Information
|
Index Terms- formal verification, µ-charts, refinement,
CSP.
Citation:
Doug Goldson,
"Formal Verification of µ-Charts,"
apsec,
p. 129,
Ninth Asia-Pacific Software Engineering Conference (APSEC'02),
2002
|
