Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top

2016 | Book

Einleitung Read chapter Read first chapter

Verteilte Laufzeitverifikation auf eingebetteten Systemen

Logiken und Monitorkonstruktionen für asynchrone Prozesse

Author: Malte Schmitz

Publisher: Springer Fachmedien Wiesbaden

Book Series : BestMasters

Part of: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Login to get access
insite
SEARCH

About this book

In seiner Arbeit betrachtet Malte Schmitz, wie die Korrektheit von verteilten Systemen zur Laufzeit überwacht werden kann. Dazu untersucht und entwickelt er verschiedene Varianten der linearen Temporallogik (LTL) und zugehörige Monitorkonstruktionen für den Einsatz zur Laufzeitverifikation verteilter, asynchroner, eingebetteter Systeme. Als Fallstudie dient dabei die sichere und korrekte Steuerung von Industrieanlagen mithilfe von innovativen Überwachungskonzepten zur Laufzeit. Der Autor hat sein Projekt modellhaft realisiert, um die verschiedenen Monitorkonstruktionen und die Monitorinjektion durch Programmtransformation im praktischen Einsatz zu evaluieren.

Table of Contents

Frontmatter
1. Einleitung
Zusammenfassung
Eingebettete Systeme steuern heutzutage neben vielen Geräten, die wir im Alltag verwenden, zunehmend auch sicherheitskritische Anlagen. Der Branchenverband BITKOM nennt in [44] unter anderem die Anwendungsbereiche Energietechnik, industrielle Anwendungen und Medizintechnik. Dabei werden die einzelnen Komponenten immer öfter zu verteilten Systemen vernetzt. Auf diese Weise muss nicht ein zentrales System die gesamte Steuerung übernehmen, sondern viele kleine Komponenten übernehmen dezentral die Steuerung einer größeren Anlage. Diese Ansätze sind preiswerter, leichter zu warten und ausfallsicherer. Bei der Entwicklung von Software muss allerdings die Verteilung der Anwendung auf mehrere Geräte berücksichtigt werden.
Malte Schmitz
2. Logiken
Zusammenfassung
In diesem Kapitel werden die in dieser Arbeit verwendeten Logiken betrachtet. Dazu werden zunächst einige Grundlagen definiert und Schreibweisen festgelegt, um dann die Lineare Temporallogik (LTL) einführen zu können. Im Zusammenhang mit der Monitorbarkeit von temporallogischen Eigenschaften wird dann LTL3 als dreiwertige Variante von LTL betrachtet, die für die Laufzeitverifikation besser geeignet ist. Im wichtigsten Abschnitt dieses Kapitels wird eine allgemeine verteilte Temporallogik vorgestellt, die sich auf die bereits betrachteten Logiken bezieht. Um auch LTL3 in dieser neuen Logik verwenden zu können, wird LTL3 im Folgenden auf dreiwertige Propositionen erweitert. Schließlich wird mit fSDTL das Konzept von Synchronisationsaktionen vorgestellt, mit deren Hilfe die Menge der monitorbaren Eigenschaften auf verteilten Systemen weiter vergrößert werden kann.
Malte Schmitz
3. Monitore
Zusammenfassung
In diesem Kapitel werden Monitorkonstruktionen für die im letzten Kapitel betrachteten Logiken angegeben. Dabei ist das Ziel, für eine Formel in DTL entsprechende Monitore für die jeweiligen Agenten zu generieren und die Kommunikation dieser Monitore anzugeben. Wir werden dazu zunächst Monitorkonstruktionen für ptLTL und LTL3 betrachten, um darauf aufbauend Monitore für DTL-Formeln zu generieren.
Malte Schmitz
4. Implementierung
Zusammenfassung
Im Rahmen dieser Arbeit wurde DTL mit fDTL und ptLTL für LEGO Mindstorms NXT implementiert. Die Firmware der NXTs erlaubt eine einfache Verwendung von Aktoren und Sensoren und stellt Bluetooth-Kommunikation zwischen den Agenten zur Verfügung. An jeden Agenten können 4 Sensoren und drei Aktoren (Motoren oder Lichter) angeschlossen werden. Die Sensoren werden in der Firmware mit 1 bis 4 und die Aktoren mit A bis C bezeichnet.
Malte Schmitz
5. Zusammenfassung und Ausblick
Zusammenfassung
In dieser Arbeit wurden Logiken und Monitore für die Laufzeitverifikation von verteilten asynchronen Systemen entwickelt, untersucht und implementiert. Die neu entwickelte verteilte Temporallogik DTL erweitert vorhandene Logiken um den @-Operator, der angibt, dass Teilformeln auf entfernten Agenten ausgewertet werden. In DTL können dazu durch die entwickelte Projektion bestehende lokale Temporallogiken weiterverwendet werden. Die aktuelle Ausgabe von entfernten Teilformeln wird dabei als Belegung für eine entsprechende Proposition verwendet. So kann zum Beispiel die ptLTL-Semantik mit temporalen Vergangenheitsoperatoren direkt in DTL verwendet werden, sodass sich die Semantik von ptDTL aus [38] ergibt.
Malte Schmitz
Backmatter
Metadata
Title
Verteilte Laufzeitverifikation auf eingebetteten Systemen
Author
Malte Schmitz
Copyright Year
2016
Electronic ISBN
978-3-658-12852-4
Print ISBN
978-3-658-12851-7
DOI
https://doi.org/10.1007/978-3-658-12852-4

Premium Partner

    Image Credits