Advertisement

Formale Modelle der Softwareentwicklung

Model-Checking, Verifikation, Analyse und Simulation

  • Authors
  • Stephan Kleuker

Table of contents

  1. Front Matter
    Pages I-X
  2. Stephan Kleuker
    Pages 1-11
  3. Stephan Kleuker
    Pages 13-116
  4. Stephan Kleuker
    Pages 117-162
  5. Stephan Kleuker
    Pages 163-200
  6. Stephan Kleuker
    Pages 201-273
  7. Stephan Kleuker
    Pages 275-279
  8. Stephan Kleuker
    Pages 281-291
  9. Back Matter
    Pages 293-301

About this book

Introduction

Software muss funktionieren, um von Kunden akzeptiert zu werden. Doch wie stellt man sicher, dass die Steuerung eines Raumschiffs, eines Herzschrittmachers oder einer Aktienverwaltung korrekt funktioniert? Neben den klassischen Testansätzen spielen für den Korrektheitsnachweis zunehmend formale Modelle eine zentrale Rolle. Ein Modell erlaubt es, ein beliebiges sequenzielles oder verteiltes System zu analysieren und zu simulieren. Dadurch, dass Korrektheitsanforderungen präzise definiert werden, kann man sogar verifizieren, dass die Anforderungen erfüllt sind. Dieses Buch stellt unterschiedliche formale Modelle mit ihren Einsatzmöglichkeiten und Werkzeugen vor. Dabei steht bewusst die Anwendung der Modelle und nicht die Theorie dahinter im Vordergrund.

Der Inhalt:
Motivation von formalen Modellen – Model Checking mit Promela und Spin – Timed Automata – Petrinetze – Semantik und Verifikation sequenzieller und paralleler Programme

Die Zielgruppe:
- Informatik-Studierende ab 4. Semester
- Studierende in Informatik-orientierten Master-Studiengängen
- Entwickler kritischer Software-Systeme
- An Qualitätssicherung Interessierte

Der Autor:
Prof. Dr. Stephan Kleuker hat im Themengebiet "formale Methoden" promoviert und lehrt seit mehreren Jahren Software-Engineering an den Fachhochschulen in Osnabrück und Wiesbaden. Er hat mehrjährige Praxiserfahrung als Systemanalytiker sowie als Berater bei der Erstellung komplexer Software-Systeme.

Keywords

Automat Automaten Java Modellprüfung PROMELA SPIN Simulation Verifikation

Bibliographic information

Industry Sectors
Electronics
IT & Software
Aerospace