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.
Translation of the title:
null
(German)
Translation of the abstract:
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.
(German)
Additional information:
Das Dokument wird vom Publikationsserver der Universitätsbibliothek Mannheim bereitgestellt.
![[img]](https://madoc.bib.uni-mannheim.de/style/images/fileicons/application_pdf.png)
Search Authors in