Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

 
 
DownloadE-Mail
  Abstrakte Übergangsrelationen als Mittel zur Verifikation von Programmeigenschaften

Schäf, M. (2006). Abstrakte Übergangsrelationen als Mittel zur Verifikation von Programmeigenschaften. Master Thesis, Universität des Saarlandes, Saarbrücken.

Item is

Basisdaten

einblenden: ausblenden:
Genre: Hochschulschrift
Latex : {Abstrakte \"Ubergangsrelationen als Mittel zur Verifikation von Programmeigenschaften}

Dateien

einblenden: Dateien
ausblenden: Dateien
:
masterthesis.pdf (beliebiger Volltext), 238KB
 
Datei-Permalink:
-
Name:
masterthesis.pdf
Beschreibung:
-
OA-Status:
Sichtbarkeit:
Privat
MIME-Typ / Prüfsumme:
application/pdf
Technische Metadaten:
Copyright Datum:
-
Copyright Info:
-
Lizenz:
-

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
Schäf, Martin1, Autor           
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: 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

Details

einblenden:
ausblenden:
Sprache(n): deu - German
 Datum: 20062006
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: Saarbrücken : Universität des Saarlandes
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: eDoc: 314601
BibTex Citekey: Schaef2005
Anderer: Local-ID: C1256104005ECAFC-9A16D39FBB0ADE2EC12571450044FF2C-Schaef2005
 Art des Abschluß: Master

Veranstaltung

einblenden:

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle

einblenden: