Logic and Refinement for Charts

Reeve, G. and Reeves, S.

We introduce a logic for reasoning about and constructing refinements for ?-Charts, a rational simplification and reconstruction of Statecharts. The method of derivation of the logic is that a semantics for the language is constructed in Z and the existing logic and refinement calculus of Z is then used to induce the logic and refinement calculus of ?-Charts, proceeding by a series of definitions and conservative extensions and hence generating a sound logic for ?-Charts, given that the soundness of the Z logic has already been established.

Cite as: Reeve, G. and Reeves, S. (2006). Logic and Refinement for Charts. In Proc. Twenty-Ninth Australasian Computer Science Conference (ACSC 2006), Hobart, Australia. CRPIT, 48. Estivill-Castro, V. and Dobbie, G., Eds. ACS. 13-23.

(from crpit.com) (local if available)