Formal verification of μ-charts

Author

Goldson, Doug

Author_Institution

Sch. of ITEE, Queensland Univ., Qld., Australia

fYear

2002

fDate

2002

Firstpage

129

Lastpage

136

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.

Keywords

communicating sequential processes; formal specification; formal verification; specification languages; visual languages; CSP; FDR; Statechart-like language; chart refinement; experiment; formal verification; instantaneous communication; model-checker; motor vehicle central locking system; mu charts; reactive system design; refinement theory; semantic metalanguage; trace refinement; visual specification language; Automata; Clocks; Computer industry; Electronics industry; Formal verification; Refining; Signal design; Specification languages; State feedback; Vehicles;

fLanguage

English

Publisher

ieee

Conference_Titel

Software Engineering Conference, 2002. Ninth Asia-Pacific

ISSN

1530-1362

Print_ISBN

0-7695-1850-8

Type

conf

DOI

10.1109/APSEC.2002.1182982

Filename

1182982