|
Verification in the Hierarchical Development of Reactive Systems
Salger, Frank
|
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. |
 Suche Autoren in
Sie haben einen Fehler gefunden? Teilen Sie uns Ihren Korrekturwunsch bitte hier mit: E-Mail
Actions (login required)
 |
Eintrag anzeigen |
|
|
![[img]](https://madoc.bib.uni-mannheim.de/style/images/fileicons/application_pdf.png)