%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 }