Please use this identifier to cite or link to this item: doi:10.22028/D291-25851
Title: Transformations of specifications and proofs to support an evolutionary formal software development
Author(s): Schairer, Axel
Language: English
Year of Publication: 2006
OPUS Source: Zugl. im Buchhandel: Herzogenrath : Shaker, 2006. - ISBN 3-8322-5380-7
SWD key words: Softwareentwicklung
Free key words: software engineering
software specification
development graph
DDC notations: 004 Computer science, internet
Publikation type: Dissertation
Abstract: Like other software engineering activities, formal modelling needs to deal with change: bugs and omissions need to be corrected, and changes from the outside need to be dealtwith. In the context of axiomatic specifications and (partly) interactive proofs, the main obstacle is that changes invalidate proofs, which then need to be rebuilt using an inhibitive amount of resources. This thesis proposes to solve the problem by considering the state of a formal development consisting of (potentially buggy) specification and (potentially partial) proofs as one entity and transforming it using preconceived transformations. These transformations are operationally motivated: how would one patch the proofs on paper given a consistent transformation for the specification? They are formulated in terms of the specification and logic language, so as to be usable for several application domains. In order to make the approach compatible with the architecture of existing support systems, development graphs are added as an intermediate concept between specification and proof obligations, and the transformations are extended to work in the presence of the indirection. This leads to a separation of a framework for propagating transformations through development graphs and a reference instantiation that commits to concrete languages and proof representation. The reference instantiation works for many practically relevant scenarios. Other instantiations can be based on the framework.
Link to this record: urn:nbn:de:bsz:291-scidok-6659
Advisor: Siekmann, Jörg
Date of oral examination: 21-Jul-2006
Date of registration: 7-Sep-2006
Faculty: MI - Fakultät für Mathematik und Informatik
Department: MI - Informatik
Collections:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Files for this record:
File Description SizeFormat 
Dissertation_5084_Scha_Axel_2005.pdf2,37 MBAdobe PDFView/Open

Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.