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

Sujets

• Informatik

Informations

• Publié par: universitat_des_saarlandes
• Publié le: 01 janvier 2006
• Nombre de lectures: 5
• Langue: English
• Poids de l'ouvrage: 2 Mo

Extrait

Transformations of
Specifications and Proofs
to Support an
Evolutionary Formal Software
Development
AxelSchairer
Dissertation
zurErlangungdesGradesdes
DoktorsderIngenieurwissenschaften
derNaturwissenschaftlich-Technischen
Fakulta¨tender
Universita¨tdesSaarlandes
Saarbru¨cken,2005Vero¨ffentlichtimShakerVerlag,Aachen,2006
www.shaker.de
TagdesKolloquiums 21.07.2006
Dekan Prof.Dr.-Ing.ThorstenHerfet
Pru¨fungsausschuss:
Vorsitzender Prof.Dr.GertSmolka
AkademischerMitarbeiter Dr.DieterHutter
Gutachter Prof.Dr.Jo¨rg H.Siekmann
Universita¨tdesSaarlandes
Prof.Dr.BerndKrieg-Bru¨ckner
Universita¨tBremen
Dr.AlanSmaill
UniversityofEdinburgh,Scotland,UKAbstract
Likeothersoftwareengineeringactivities,formalmodellingneedstodeal
with change: bugs and omissions needto be corrected, and changes from
theoutsideneedtobedealtwith. Inthecontextofaxiomaticspecifications
and (partly) interactive proofs, the main obstacle is that changes invali-
date 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 pre-
conceivedtransformations. Thesetransformationsareoperationallymoti-
vated: howwouldonepatchtheproofsonpapergivenaconsistenttrans-
formation for the specification? Theyare formulated interms of the spec-
ification and logic language, so as to be usable for several application do-
mains.
In order to make the approach compatible with the architecture of ex-
istingsupportsystems,developmentgraphsareaddedasanintermediate
concept between specification and proof obligations, and the transforma-
tionsareextendedtoworkinthepresenceoftheindirection. Thisleadsto
aseparationofaframeworkfor propagating transformations through de-
velopment graphs and a reference instantiation that commits to concrete
languagesandproofrepresentation. Thereferenceinstantiationworksfor
many practically relevant scenarios. Other instantiations can be based on
theframework.
iiiZusammenfassung
Wie bei allen anderen Software Engineering-Aktivita¨ten muss es auch bei
¨der formalen Modellierung mo¨glich sein, Anderungen vorzunehmen. So
ko¨nnen Modellierungsfehler korrigiert, Unvollsta¨ndigkeiten erga¨nzt und
¨externe AnderungenindasModelleingearbeitetwerden.Fu¨raxiomatische
Spezifikationenund(zumindestteilweise)interaktiveBeweiseistdasgro¨ß-
¨te Hindernis dabei, dass Anderungen die Beweise ungu¨ltig machen. Diese
mu¨ssendannerneutkonstruiertwerden,waseinenunverantwortbarhohen
EinsatzvonRessourcenerfordert.
Diese Arbeit schla¨gt vor, dieses Problem dadurch zu lo¨sen, dass eine
formale Entwicklung bestehend aus einer (mo¨glicherweise fehlerhaften)
Spezifikationund(mo¨glicherweiseunvollsta¨ndigen)BeweisenalseineEin-
heit betrachtet und nach vorgegebenen Regeln transformiert wird. Diese
Regeln werden Transformationen genannt und sind operational motiviert:
Wie wu¨rde ein Mensch intuitiv die Beweise anpassen, wenn eine in sich
konsistente Transformation auf die Spezifikation angewendet wird? Die
Transformationensindunabha¨ngigvonderAnwendungsdoma¨neanwend-
bar.UmdenAnsatzmitdemAufbauexistierenderWerkzeugevereinbarzu
machen,fu¨hrenwireinzusa¨tzlichesKonzeptalsMittlerzwischenSpezifika-
tionundBeweisverpflichtungenein,sogenannteDevelopmentGraphs.Das
fu¨hrt zu einer Trennung zwischen einemRahmenwerk, das Transformatio-
nen u¨ber generische Development Graphs hinweg propagiert, und einer
Referenzinstantiierung, die sich auf konkrete Sprachen und eine konkrete
Repra¨sentation der Beweise festlegt. Die Referenzinstanz erlaubt die Be-
handlung von vielen in der Praxis vorkommenden Szenarien. Andere In-
stanzenko¨nnenausdemRahmenwerkabgeleitetwerden.
vAusfu¨ hrliche Zusammenfassung
Eswirdheuteallgemeinakzeptiert,dasseinreinwasserfallartigerSoftware-
Entwicklungsprozess nicht angemessen ist. Wiebeiallenanderen Software
Engineering-Aktivita¨tenauchmussesdaherbeiderformalenModellierung
¨mo¨glich sein, Anderungen vorzunehmen. So ko¨nnen Modellierungsfehler
¨korrigiert, Unvollsta¨ndigkeiten verbessert und externe Anderungen in das
Modell eingearbeitet werden. Gerade das Entdecken und Eliminieren von
Fehlern in einem fru¨hen Stadium ist einer der Hauptvorteile der formalen
ModellierungundEntwicklung.
Fu¨r axiomatische Spezifikationen und (zumindest teilweise) interaktive
¨Beweise ist das gro¨ßte Hindernis dabei, dass Anderungen die vorher
konstruierten Beweise potentiell ungu¨ltig machen. Diese mu¨ssen dann
erneut konstruiert werden, was einen unverantwortbar hohen Einsatz von
Ressourcen erfordert. Gerade gegen Ende einer Entwicklung wird so das
Projektrisiko immergro¨ßer.
¨Diese Beobachtung beruht auf der Annahme, dass Anderungen an den
Spezifikationen zuerst unabha¨ngig von den Beweisen durchgefu¨hrt wer-
den, und dass dann in einem zweiten Schritt die Beweise nachgefu¨hrt
oder neu konstruiert werden. Wir schlagen deswegen vor, dieses Problem
dadurch zu lo¨sen, dass eine formale Entwicklung bestehend aus einer
(mo¨glicherweise fehlerhaften) Spezifikation und (mo¨glicherweise unvoll-
sta¨ndigen) Beweisen als eine Einheit betrachtet wird und nach vorgegebe-
nen Regeln transformiert wird. Diese Regeln werden Development Trans-
formationsgenanntundsindoperationalmotiviert: Wiewu¨rdeeinMensch
intuitivdieBeweiseanpassen,wenneineinsichkonsistenteTransformation
aufdieSpezifikationangewendetwird? DieTransformationen sindaufder
Ebene der Spezifikations- und Logiksprache formuliert. Damit werden sie
unabha¨ngigvonderAnwendungsdoma¨neanwendbar.
Um den Ansatz mit dem Aufbau existierender Werkzeuge, wie zum
BeispieldieinunsererGruppeentwickeltenSoftwaretoolsVSEoderINKA/
MAYA, vereinbar zu machen, fu¨hren wir ein dort zusa¨tzlich vorhandenes
Konzept als Mittler zwischen Spezifikation und Beweisverpflichtungen
ein, so genannte Development Graphs. Development Graphs dienen einer
logischen Strukturierung der Spezifikationen und der davon abgeleiteten
Beweisverpflichtungen. Die Transformationen werden so erweitert, dass
sie die zusa¨tzlich eingefu¨hrten Development Graphs beru¨cksichtigen. Das
fu¨hrtzueinerTrennungzwischeneinemRahmenwerk,dasdieTransforma-
tionenu¨bergenerischeDevelopmentGraphshinwegpropagiert, undeiner
viiReferenzinstantiierung, die sich auf konkrete Sprachen und eine konkrete
Repra¨sentation der Beweise festlegt. Die Referenzinstanz erlaubt die Be-
handlung von vielen in der Praxis vorkommenden Szenarien. Andere In-
stanzenko¨nnenausdemRahmenwerkabgeleitetwerden.
Wirentwickelneine konkrete Instanzdesvorgestellten Rahmenwerkes.
In einer prototypischen Implementierung mechanisieren wir Transforma-
tionendervorgestellten Instanz.Soweisenwirnach,dassdievorgestellten
Konzepte praktisch anwendbar sind, und Korrekturen und Erga¨nzungen
derSpezifikationundderBeweisemitvertretbaremAufwandmo¨glichwer-
den.
viiiAcknowledgements
Thisthesiswouldnothavebeenwrittenwithoutthehelpandsupportthat
Ireceived. Inparticular,IamindebtedtoProfessorJo¨rgH.Siekmannwho
letmebeamemberofhisgroupinSaarbru¨ckenandprovidedaninspiring
environment in which to work, and to Professor AlanBundy who hosted
me as a visiting researcher in Edinburgh for a year. My work was sub-
stantially influencedby my stay in Edinburgh, and I am very grateful for
the fundingofthe GermanAcademicExchange Service (DAAD).Iwould
alsoliketo thankProfessor BerndKrieg-Bru¨ckner andDr.AlanSmaillfor
agreeing to serve as my examiners and for the feedback and encourage-
mentthattheyprovided.
I am particularly grateful for the support that my supervisor Dieter
Hutter has provided over all those years. He has always been available
to discuss ideas, provide feedback and offer advice whenever I needed
it. I would also like to thank Dieter for the time and energy he spent on
commentingnumerousnotesanddraftsofthisthesis. Iguessheisatleast
ashappyasIamthatthisisthefinaliteration.
I wouldlike to thank TillMossakowski for invaluable discussions and
comments. In particular I am very grateful for the helpful feedback he
provided on numerous notes that would eventually become the frame-
work part of my thesis, andfor his comments on the near-final version of
therelevantchapter.
My thanks are due to the members of our group at the DFKI in Saar-
bru¨cken and the DReaM group in Edinburgh, both for input and for the
positiveandencouragingatmosphere. Inparticular,SergeAutexier,Heiko
Mantel,WernerStephan,TobyWalshandAndreasWolpershaveprovided
helpfuldiscussionsandvaluableinsights.
Perhaps the most important source of help over all those years, how-
ever,wasthesupportthatJuliaandmyparentsprovided. Ifitwasnotfor
them,Iwouldnotbewritingthesewords now.
AThisthesiswassetinPalatinoandHelveticausingLT X,MakotoTatsuta’sproofpackageE
andPaulTaylor’scommutativediagramspackage.
ix