Formale Modelle der Softwareentwicklung Model-Checking, Verifikation, Analyse und Simulation

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 Mode...

Full description

Bibliographic Details
Main Author: Kleuker, Stephan
Format: eBook
Language:German
Published: Wiesbaden Vieweg+Teubner Verlag 2009, 2009
Edition:1st ed. 2009
Subjects:
Online Access:
Collection: Springer eBooks 2005- - Collection details see MPG.ReNa
LEADER 02686nmm a2200289 u 4500
001 EB000394185
003 EBX01000000000000000247238
005 00000000000000.0
007 cr|||||||||||||||||||||
008 130626 ||| ger
020 |a 9783834895950 
100 1 |a Kleuker, Stephan 
245 0 0 |a Formale Modelle der Softwareentwicklung  |h Elektronische Ressource  |b Model-Checking, Verifikation, Analyse und Simulation  |c von Stephan Kleuker 
250 |a 1st ed. 2009 
260 |a Wiesbaden  |b Vieweg+Teubner Verlag  |c 2009, 2009 
300 |a X, 301 S. 206 Abb  |b online resource 
505 0 |a Motivation von Formalen Modellen -- Modelchecking mit PROMELA und SPIN -- Modelchecking mit Timed Automata und Uppaal -- Petrinetze -- Programmverifikation -- Installationsbeschreibungen -- Kurzeinführung in Java 
653 |a Computer Science Logic and Foundations of Programming 
653 |a Software engineering 
653 |a Computer science 
653 |a Software Engineering 
041 0 7 |a ger  |2 ISO 639-2 
989 |b Springer  |a Springer eBooks 2005- 
028 5 0 |a 10.1007/978-3-8348-9595-0 
856 4 0 |u https://doi.org/10.1007/978-3-8348-9595-0?nosfx=y  |x Verlag  |3 Volltext 
082 0 |a 004.0151 
520 |a 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