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

نرم افزار باید کار کند تا توسط مشتریان پذیرفته شود. اما چگونه می توان اطمینان حاصل کرد که کنترل یک سفینه فضایی، یک ضربان ساز یا یک سیستم مدیریت انبار به درستی کار می کند؟ علاوه بر رویکردهای آزمون کلاسیک، مدل های رسمی به طور فزاینده ای نقش اصلی را در اثبات صحت بازی می کنند. یک مدل اجازه می دهد تا هر سیستم متوالی یا توزیع شده را تجزیه و تحلیل و شبیه سازی کند. با تعریف دقیق الزامات صحت، حتی می توان تأیید کرد که الزامات برآورده شده اند. این کتاب مدل‌های رسمی مختلف را با کاربردها و ابزارهای ممکن ارائه می‌کند. کاربرد مدل ها و نه تئوری پشت آن ها آگاهانه در پیش زمینه است.

محتوا:
انگیزه مدل های رسمی - بررسی مدل با پروملا و اسپین - اتوماتای ​​زمان بندی شده - شبکه های پتری - معناشناسی و تایید برنامه های متوالی و موازی

گروه هدف:
- دانشجویان علوم کامپیوتر از ترم 4
- دانشجویان دوره های کارشناسی ارشد علوم کامپیوتر گرایش
- توسعه دهندگان سیستم های نرم افزاری حیاتی
- علاقه مندان به تضمین کیفیت< br
نویسنده:
پروفسور دکتر. استفان کلوکر دکترای خود را در زمینه "روش های رسمی" گذرانده است و چندین سال است که در دانشگاه های علوم کاربردی در Osnabrück و Wiesbaden به تدریس مهندسی نرم افزار می پردازد. او سالها تجربه عملی به عنوان تحلیلگر سیستم و مشاور در ایجاد سیستم های نرم افزاری پیچیده دارد.

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.