Generic tools via general refinement

Simple item page
dc.contributor.authorReeves, Steve
dc.contributor.authorStreader, David
dc.date.accessioned2013-11-20T21:52:25Z
dc.date.available2013-11-20T21:52:25Z
dc.date.copyright2008-04
dc.date.issued2008
dc.description.abstractTools have become essential in the formal model-driven development of software but are very time consuming to build and often restricted to a particular semantic interpretation of a particular syntax. This is regrettable since there is large amount in common between tools, even if they do “implement” different syntaxes and different semantics. We propose splitting tools into front- and back-ends where an operational semantics acts as the link between the two. We will not have much to say about the front-end and the link in this paper since it is theoretically straightforward. Instead, we concentrate on the second part and provide a well-motivated, general, mathematical framework to form the underlying theory that gives great flexibility to the back-end of a tool which is concerned with developing software via stepwise refinement. From a general model of refinement between two entities, where the refinement is parameterised on contexts and observations, we build logical theories which have refinement as implication. Further, we consider what can be expected of a guarantee concerning the behaviour of an implementation relative to a specification. Then by fixing the contexts and observations in suitable ways, and so getting particular, special models of refinement, we give a formal interpretation of a guarantee. To this we add theory morphisms between special models, where a theory morphism can change the contexts and observations we can make in controlled and useful ways, mainly by preserving a refinement relation between entities even as we change them. We show how the generality brought about by the parameterisation allows an example from the literature, which seems formally not to be a refinement, to be captured as a refinement, in accordance with our intuitions about the example. In this way we show the flexibility of our theory for a refinement tool back-end. From this it follows that the effort put into building a tool based on our theory will be well-spent—a single tool should be parameterised (just as our theory is) to deal with the many different notions of refinement found in the literature. Thus we make a contribution to the problem of ensuring correctness and dependability of software using formal methods and tools of modelling, design, verification and validation.en_NZ
dc.identifier.citationReeves, S., & Streader, D. (2008). Generic tools via general refinement. Electronic Notes in Theoretical Computer Science, 207, 187-202.en_NZ
dc.identifier.doi10.1016/j.entcs.2008.03.093en_NZ
dc.identifier.urihttps://hdl.handle.net/10289/8202
dc.language.isoenen_NZ
dc.publisherElsevier B.V.en_NZ
dc.relation.isPartOfElectronic Notes in Theoretical Computer Scienceen_NZ
dc.relation.ispartofElectronic Notes in Theoretical Computer Science
dc.relation.urihttp://www.sciencedirect.com/science/article/pii/S1571066108001989#en_NZ
dc.subjectbasis for toolsen_NZ
dc.subjectrefinementen_NZ
dc.subjecttheory morphismen_NZ
dc.subjectflexible refinementen_NZ
dc.titleGeneric tools via general refinementen_NZ
dc.typeJournal Articleen_NZ
pubs.begin-page187en_NZ
pubs.elements-id32909
pubs.end-page202en_NZ
pubs.issueCen_NZ
pubs.volume207en_NZ
uow.identifier.article-noCen_NZ
Files
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
1.71 KB
Format:
Item-specific license agreed upon to submission
Description:
Name: license.txt
Size: 1.71 KB
Kind: License
Collections
Computing and Mathematical Sciences Papers