A refinement theory for μ∼Charts

Abstract

The language μ-Charts is one of many Statechart-like languages, a family of visual languages that are used for designing reactive systems. We introduce a logic for reasoning about and constructing refinements for μ-Charts. The logic itself is interesting and important because it allows reasoning about μ-charts in terms of partial relations rather than the more traditional traces approach. The method of derivation of the logic is also worthy of report. AZ-based model for the language μ-Charts is constructed and the existing logic and refinement calculus of Z is used as the basis for the logic of μ-Charts. As well as describing the logic we introduce some of the ways such a logic can be used to reason about properties of μ-Charts and the refinement of abstract specifications into concrete realisations of reactive systems. A refinement theory for Statechart-like languages is an important contribution because it allows us to formally investigate and reason about properties of the object language μ-Charts. In particular, we can conjecture and prove general properties required of the object language. This allows us to contrast possible language design decisions and comment on their consequences with respect to the design of Statechart-like languages. This thesis gives a comprehensive description of the μ-Charts language and details the development of a partial relations based logic and refinement calculus for the language. The logic and refinement calculus are presented as natural deduction style proof rules that allow us to give formal proofs of language properties and provide the basis for a formal program development framework. The notion of refinement that is encoded by the refinement rules is also extensively investigated.