Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-25851
Titel: Transformations of specifications and proofs to support an evolutionary formal software development
VerfasserIn: Schairer, Axel
Sprache: Englisch
Erscheinungsjahr: 2006
Quelle: Zugl. im Buchhandel: Herzogenrath : Shaker, 2006. - ISBN 3-8322-5380-7
Kontrollierte Schlagwörter: Softwareentwicklung
Transformation
Softwarespezifikation
Freie Schlagwörter: software engineering
transformation
software specification
development graph
DDC-Sachgruppe: 004 Informatik
Dokumenttyp: 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 zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-6659
hdl:20.500.11880/25907
http://dx.doi.org/10.22028/D291-25851
Erstgutachter: Siekmann, Jörg
Tag der mündlichen Prüfung: 21-Jul-2006
Datum des Eintrags: 7-Sep-2006
Fakultät: MI - Fakultät für Mathematik und Informatik
Fachrichtung: MI - Informatik
Sammlung:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Dateien zu diesem Datensatz:
Datei Beschreibung GrößeFormat 
Dissertation_5084_Scha_Axel_2005.pdf2,37 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.