A refinement theory for μ∼Charts

Reeve, Greg

A refinement theory for μ∼Charts

dc.contributor.advisor	Reeves, Steve
dc.contributor.author	Reeve, Greg
dc.date.accessioned	2019-12-01T22:58:02Z
dc.date.available	2019-12-01T22:58:02Z
dc.date.issued	2005
dc.date.updated	2019-10-04T00:45:36Z
dc.description.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.
dc.format.mimetype	application/pdf
dc.identifier.citation	Reeve, G. (2005). A refinement theory for μ∼Charts (Thesis, Doctor of Philosophy (PhD)). The University of Waikato, Hamilton, New Zealand. Retrieved from https://hdl.handle.net/10289/13204	en
dc.identifier.uri	https://hdl.handle.net/10289/13204
dc.language.iso	en
dc.publisher	The University of Waikato
dc.rights	All items in Research Commons are provided for private study and research purposes and are protected by copyright with all rights reserved unless otherwise indicated.
dc.title	A refinement theory for μ∼Charts
dc.type	Thesis
pubs.place-of-publication	Hamilton, New Zealand	en_NZ
thesis.degree.grantor	The University of Waikato
thesis.degree.level	Doctoral
thesis.degree.name	Doctor of Philosophy (PhD)