Show simple item record  

dc.contributor.advisorReeves, Steve
dc.contributor.authorReeve, Greg
dc.date.accessioned2019-12-01T22:58:02Z
dc.date.available2019-12-01T22:58:02Z
dc.date.issued2005
dc.identifier.citationReeve, 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/13204en
dc.identifier.urihttps://hdl.handle.net/10289/13204
dc.description.abstractThe 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.mimetypeapplication/pdf
dc.language.isoen
dc.publisherThe University of Waikato
dc.rightsAll 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.titleA refinement theory for μ∼Charts
dc.typeThesis
thesis.degree.grantorThe University of Waikato
thesis.degree.levelDoctoral
thesis.degree.nameDoctor of Philosophy (PhD)
dc.date.updated2019-10-04T00:45:36Z
pubs.place-of-publicationHamilton, New Zealanden_NZ


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record