Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

Publications Master Template :: Thesis :: Schäf, Martin


Publications Master Template
Show all entries of:this year (2019)last year (2018)two years ago (2017)Open in Notes
Action:login to update

Thesis - Master's thesis | @MastersThesis | Masterarbeit


Author
Author(s)*:Schäf, Martin
BibTeX citekey*:Schaef2005
Language:German

Title, School
Title*:Abstrakte Übergangsrelationen als Mittel zur Verifikation von Programmeigenschaften
School:Universität des Saarlandes
Type of Thesis*:Master's thesis
Month:April
Year:2006


Note, Abstract, Copyright
LaTeX Abstract:Die Entwicklung von Software ist ein fehleranf¨alliger Prozess. Allein die Tatsache,

dass ein Programm ausf¨uhrbar ist und dass f¨ur eine begrenzte Menge
von Testf¨allen keine Fehler in der Ausf¨uhrung des Programms auftritt, sagt
nicht aus, dass ein Programm fehlerfrei ist. Vor allem in Bereichen, in denen
Software nicht einfach im Fall eines Versagens abgeschaltet und repariert
werden kann ist es wichtig beweisen zu k¨onnen, dass Software fehlerfrei
ist. Es existieren verschiedene Methoden diesen Beweis zu erbringen. Die
g¨angigste Methode ist deduktive Verifikation, in der die Software von Hand
verifiziert wird. Dieser Vorgang ist allerdings teuer und fehleranf¨allig.
Formale Verifikation ist eine j¨ungere Methode die vor allem f¨ur die Verifikation
von Hardware verwendet wird. Mit formaler Verifikation k¨onnen
Systeme mit endlicher Zustandsmenge automatisch bewiesen werden. Um
die Methode auf Software anzuwenden, muss diese abstrahiert werden, da
die Zustandsmenge eines Programms unendlich gross sein kann. Das U¨ berpr
¨ufen von Programmeigenschaften auf einem abstrakten Modell wird auch
Model Checking genannt.
Es existieren verschiedene Ans¨atze um durch Model Checking Programmeigenschaften
zu beweisen. In [esp] wird ein Ansatz vorgestellt tempor¨are
Sicherheitseigenschaften eines Programms automatisch zu Beweisen. [tin]
stellt eine M¨oglichkeit vor durch Model Checking Terminierung und Fairness
zu beweisen.
Diese Ans¨atze arbeiten immer auf dem gesamten Programm. In dieser Arbeit
wird eine Methode hergeleitet, ein Programm oder einen Teil eines Programms
in eine abstrakte U¨ bergangsrelation zu u¨bersetzen und durch diese,
Annahmen ¨uber das Verhalten der Programmvariablen zu beweisen. Der Vorteil
dieser Methode ist die Wiederverwendbarkeit von U¨ bergangsrelationen.
Da diese unabh¨angig vom Kontrollfluss sind, gen¨ugt es, f¨ur einen Programmteil
einmalig die U¨ bergangsrelation zu berechnen, egal wie oft dieser Teil verwendet
wird. Diese Eigenschaft bietet es an, dieses Verfahren in den Prozess
der Softwareentwicklung einzubeziehen um die Fehlersuche zu erleichtern,
oder Fehler fr¨uhzeitig zu erkennen.
4

Keywords:Verification
Download Access Level:Public
Download File(s):View attachments here:

Referees, Status, Dates
1. Referee:Prof. Dr. Andreas Podelski
2. Referee:Prof. Dr. Bernd Finkbeiner
Supervisor:Andreas Podelski
Status:Completed
Date Kolloquium:3 April 2006

Correlation
MPG Unit:Max-Planck-Institut für Informatik
MPG Subunit:Programming Logics Group
Audience:Expert
Appearance:MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort


BibTeX Entry:
@MASTERSTHESIS{Schaef2005,
AUTHOR = {Sch{\"a}f, Martin},
TITLE = {Abstrakte {\"U}bergangsrelationen als Mittel zur Verifikation von Programmeigenschaften},
SCHOOL = {Universit{\"a}t des Saarlandes},
YEAR = {2006},
TYPE = {Master's thesis}
MONTH = {April},
}


Hide details for Attachment SectionAttachment Section
masterthesis.pdf
View attachments here:




Entry last modified by Veronika Weinand, 01/28/2008
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Veronika Weinand
Created
04/03/2006 02:33:37 PM
Revisions
5.
4.
3.
2.
1.
Editor(s)
Veronika Weinand
Uwe Brahm
Veronika Weinand
Veronika Weinand
Veronika Weinand
Edit Dates
29.11.2006 10:47:32
05-04-2006 12:44:12
03.04.2006 16:01:24
03.04.2006 16:01:10
03.04.2006 15:00:52