Verification in the Hierarchical Development of Reactive Systems


Salger, Frank


[img]
Preview
PDF
31_1.pdf - Published

Download (895kB)

URL: http://ub-madoc.bib.uni-mannheim.de/31
URN: urn:nbn:de:bsz:180-madoc-312
Document Type: Doctoral dissertation
Year of publication: 2001
Publishing house: Universität Mannheim
Evaluator: Majster-Cederbaum, Mila
Date of oral examination: 21 May 2001
Publication language: English
Institution: School of Business Informatics and Mathematics > Praktische Informatik II (Majster-Cederbaum Em)
Subject: 004 Computer science, internet
Subject headings (SWD): Prozessalgebra , Verfeinerung , Verifikation , Modallogik
Keywords (English): 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.




+ Citation Example and Export

Salger, Frank (2001) Verification in the Hierarchical Development of Reactive Systems. Open Access [Doctoral dissertation]
[img]
Preview


+ Search Authors in

BASE: Salger, Frank

Google Scholar: Salger, Frank

+ Download Statistics

Downloads per month over past year

View more statistics



You have found an error? Please let us know about your desired correction here: E-Mail


Actions (login required)

Show item Show item