Verification in the Hierarchical Development of Reactive Systems


Salger, Frank


[img]
Vorschau
PDF
31_1.pdf - Veröffentlichte Version

Download (895kB)

URL: http://ub-madoc.bib.uni-mannheim.de/31
URN: urn:nbn:de:bsz:180-madoc-312
Dokumenttyp: Dissertation
Erscheinungsjahr: 2001
Titel einer Zeitschrift oder einer Reihe: None
Verlag: Universität Mannheim
Gutachter: Majster-Cederbaum, Mila
Datum der mündl. Prüfung: 21 Mai 2001
Sprache der Veröffentlichung: Englisch
Einrichtung: Fakultät für Wirtschaftsinformatik und Wirtschaftsmathematik > Praktische Informatik II (Majster-Cederbaum -2005, Em)
Fachgebiet: 004 Informatik
Normierte Schlagwörter (SWD): Prozessalgebra , Verfeinerung , Verifikation , Modallogik
Freie Schlagwörter (Englisch): process algebra , refinement , verification , modal logic
Abstract: In many approaches to the verification of reactive systems, operational semantics are used to model systems whereas specifications are expressed in temporal logics. Most approaches however fail to handle changes of the specification but assume, that the initial specification is indeed the intended one. Changing the specification thus necessitates to find an accordingly adapted system and to carry out the verification from scratch. During a systems life cycle however, changes of the requirements and resources necessitate repeated adaptations of specifications. We here propose a method that supports syntactic action refinement (in the process algebra TCSP and the Modal Mu-Calculus) and allows to automatically obtain (a priori) correct reactive systems by hierarchically adding details to the according specifications.
Übersetzter Titel: null (Deutsch)
Übersetzung des Abstracts: Die intensiv untersuchte Methode der syntaktischen Aktionsverfeinerung erlaubt den formalen und hierarchischen Entwurf reaktiver Systeme in (prozess-) algebraischen Entwicklungssprachen: Mit Hilfe der syntaktischen Aktionsverfeinerung werden (atomare) Aktionen eines abstrakten Systementwurfs durch komplexe (nicht-atomare) Prozesse beschrieben. Eigenschaften von Systemen werden oft in Temporaler Logik spezifiziert. Eine besonders ausdrucksstarke Temporale Logik ist der Modale Mu-Kalkuel. Unter der Verifikation eines Systementwurfs wird der mathematische Nachweis bestimmter Eigenschaften des Systementwurfs verstanden. Diese Arbeit befasst sich mit der Integration konventioneller Verifikationstechniken in den hierarchischen, auf der syntaktischen Aktionsverfeinerung basierenden, Entwurf reaktiver Systeme. In diesem Rahmen wird eine bereits existierende Methode zur syntaktischen Aktionsverfeinerung in der Prozess-Algebra TCSP vorgestellt und unseren Zwecken entsprechend erweitert. Daraufhin definieren wir eine Methode zur syntaktischen Aktionsverfeinerung in dem Modalen Mu-Kalkuel. Es wird nachgewiesen, dass die Methode zur syntaktischen Aktionsverfeinerung in dem Modalen Mu-Kalkuel in kanonischer Weise zu der Methode zur syntaktischen Aktionsverfeinerung in TCSP passt. Dies ergibt eine Methode, welche die hierarchische und (a priori) korrekte Entwicklung von Reaktiven Systemen erlaubt. (Deutsch)
Zusätzliche Informationen:




Das Dokument wird vom Publikationsserver der Universitätsbibliothek Mannheim bereitgestellt.




Metadaten-Export


Zitation


+ Suche Autoren in

BASE: Salger, Frank

Google Scholar: Salger, Frank

+ Download-Statistik

Downloads im letzten Jahr

Detaillierte Angaben



Sie haben einen Fehler gefunden? Teilen Sie uns Ihren Korrekturwunsch bitte hier mit: E-Mail


Actions (login required)

Eintrag anzeigen Eintrag anzeigen