This paper describes an experiment in the formal verification of /spl mu/-charts, a Statechart-like language with instantaneous communication. Properties of /spl mu/-charts are verified using a theory of chart refinement. By modelling /spl mu/-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.
%0 Conference Paper
%1 goldson_02_formal
%A Goldson, Doug
%D 2002
%J Software Engineering Conference, 2002. Ninth Asia-Pacific
%K mu-charts _hardcopy refinement semantics 2002 statecharts csp
%P 129--136
%R 10.1109/APSEC.2002.1182982
%T Formal verification of ^Aµ-charts
%U http://dx.doi.org/10.1109/APSEC.2002.1182982
%X This paper describes an experiment in the formal verification of /spl mu/-charts, a Statechart-like language with instantaneous communication. Properties of /spl mu/-charts are verified using a theory of chart refinement. By modelling /spl mu/-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.
@inproceedings{goldson_02_formal,
abstract = {This paper describes an experiment in the formal verification of /spl mu/-charts, a Statechart-like language with instantaneous communication. Properties of /spl mu/-charts are verified using a theory of chart refinement. By modelling /spl mu/-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.},
added-at = {2009-02-11T22:26:04.000+0100},
author = {Goldson, Doug},
biburl = {https://www.bibsonomy.org/bibtex/26e34497122cffec420149276bfce8142/leonardo},
citeulike-article-id = {890480},
doi = {10.1109/APSEC.2002.1182982},
interhash = {2609b353e3d3b55902d17188e4938287},
intrahash = {6e34497122cffec420149276bfce8142},
journal = {Software Engineering Conference, 2002. Ninth Asia-Pacific},
keywords = {mu-charts _hardcopy refinement semantics 2002 statecharts csp},
pages = {129--136},
posted-at = {2006-10-09 22:50:51},
priority = {5},
timestamp = {2009-02-11T22:26:04.000+0100},
title = {Formal verification of ^{A}µ-charts},
url = {http://dx.doi.org/10.1109/APSEC.2002.1182982},
year = 2002
}