Transformations of specifications and proofs to support an evolutionary formal software development [Elektronische Ressource] / Axel Schairer

Transformations ofSpecifications and Proofsto Support anEvolutionary Formal SoftwareDevelopmentAxelSchairerDissertationzurErlangungdesGradesdesDoktorsderIngenieurwissenschaftenderNaturwissenschaftlich-TechnischenFakulta¨tenderUniversita¨tdesSaarlandesSaarbru¨cken,2005Vero¨ffentlichtimShakerVerlag,Aachen,2006www.shaker.deTagdesKolloquiums 21.07.2006Dekan Prof.Dr.-Ing.ThorstenHerfetPru¨fungsausschuss:Vorsitzender Prof.Dr.GertSmolkaAkademischerMitarbeiter Dr.DieterHutterGutachter Prof.Dr.Jo¨rg H.SiekmannUniversita¨tdesSaarlandesProf.Dr.BerndKrieg-Bru¨cknerUniversita¨tBremenDr.AlanSmaillUniversityofEdinburgh,Scotland,UKAbstractLikeothersoftwareengineeringactivities,formalmodellingneedstodealwith change: bugs and omissions needto be corrected, and changes fromtheoutsideneedtobedealtwith. Inthecontextofaxiomaticspecificationsand (partly) interactive proofs, the main obstacle is that changes invali-date proofs, which then need to be rebuilt using an inhibitive amount ofresources.This thesis proposes to solve the problem by considering the state ofa formal development consisting of (potentially buggy) specification and(potentially partial) proofs as one entity and transforming it using pre-conceivedtransformations. Thesetransformationsareoperationallymoti-vated: howwouldonepatchtheproofsonpapergivenaconsistenttrans-formation for the specification?