Editorial Cuvillier

Publicaciones, tesis doctorales, capacitaciónes para acceder a una cátedra de universidad & prospectos.
Su editorial internacional especializado en ciencias y economia

Editorial Cuvillier

De En Es
Komposition temporallogischer Spezifikationen

Impresion
EUR 36,00 EUR 34,20

E-Book
EUR 25,20

Komposition temporallogischer Spezifikationen (Tienda española)

Spezifikation und Verifikation von Systemen mit Temporal Logic of Distributed Actions

Adrianna Alexander (Autor)

Previo

Indice, Datei (50 KB)
Lectura de prueba, Datei (150 KB)

ISBN-10 (Impresion) 3865378137
ISBN-13 (Impresion) 9783865378132
ISBN-13 (E-Book) 9783736918139
Idioma Deutsch
Numero de paginas 278
Edicion 1
Volumen 0
Lugar de publicacion Göttingen
Lugar de la disertacion Berlin
Fecha de publicacion 01.03.2006
Clasificacion simple Tesis doctoral
Area Ingeniería eléctrica
Descripcion

In dieser Arbeit entwickeln wir eine neue Temporale Logik, die Temporal Logic of Distributed Actions, kurz TLDA genannt. TLDA dient zur kompositionalen Spezifikation und Verifikation verteilter Systeme. Syntaktisch stammt TLDA von einer bereits etablierten Temporalen Logik, TLA, ab. Im Gegenteil zu TLA und anderen bekannten kompositionalen Temporalen Logiken basiert aber TLDA auf einer halbgeordneten semantischen Struktur, einem verteilten Ablauf. Dadurch werden, im Vergleich zu TLA, die Ausdrucksmöglichkeiten der Logik erweitert. Sowohl das System als auch seine Eigenschaften werden in einem Formalismus beschrieben: Beide werden jeweils als eine Menge von verteilten Abläufen repräsentiert und durch eine temporallogische Formel in TLDA spezifiziert. Somit reduziert sich die Verifikation eines Systems auf den Nachweis, dass die Systemspezifikation die Eigenschaftenspezifikation impliziert. Dafür stellen wir eine Reihe von Beweisregeln zur Verfügung. Wir zeigen, dass die Komposition von Systemen als Konjunktion der Spezifikationen der Komponenten und, in der Regel, der Spezifikation der Interaktion zwischen den Komponenten spezifiziert wird. Folglich kann die Spezifikation eines komponierten Systems aus den Spezifikationen seiner Komponenten gewonnen werden. Die Eigenschaften der Komponenten bleiben im komponierten System erhalten. Demzufolge kann ein zusammengesetztes System komponentenweise verifiziert werden, was eine Aufwandsersparnis bringt. Angepasst an verteilte Abläufe entwickeln wir ein semantisches Kriterium für TLDA-Formeln, die Umgebungsinvarianz, und zeigen, dass Formeln, die das Kriterium erfüllen, insbesondere zur Spezifikation der Komponenten eines Systems geeignet sind. Wir weisen nach, dass die umgebungsinvarianten Formeln aufgrund ihrer Eigenschaften eine schrittweise kompositionale Spezifikation ermöglichen.