Logo des Repositoriums
 
Textdokument

Specification and verification of mobile real-time systems

Lade...
Vorschaubild

Volltext URI

Dokumententyp

Zusatzinformation

Datum

2007

Zeitschriftentitel

ISSN der Zeitschrift

Bandtitel

Verlag

Gesellschaft für Informatik

Zusammenfassung

In dieser Arbeit wird eine formale Methode, die Logik Shape Calculus, zur Beschreibung und Verifikation von Systemen vorgestellt, deren Beschreibung sowohl Aussagen über den zeitlichen Ablauf als auch die räumliche Konfiguration der Komponenten erfordert. Es wird gezeigt, dass die Logik im Allgemeinen unentscheidbar ist. Es werden zwei entscheidbare Teilklassen angeben. Eine Teilklasse wird durch Einschränkung auf endliche diskrete Räume gewonnen. Die zweite Teilklasse durch syntaktische Einschränkung der Formelklasse. Für die erste Teilklasse existiert ein automatisches Verifikationswerkzeug. Die Anwendung dieses Werkzeugs wird anhand eines Fallbeispiels demonstriert, das mit Methoden, die nur die zeitlichen Aspekte betrachten nicht untersucht werden kann.

Beschreibung

Schäfer, Andreas (2007): Specification and verification of mobile real-time systems. Ausgezeichnete Informatikdissertationen 2006. Bonn: Gesellschaft für Informatik. PISSN: 1617-5468. ISBN: 978-3-88579-411-0. pp. 169-178

Schlagwörter

Zitierform

DOI

Tags