Please use this identifier to cite or link to this item: http://dx.doi.org/10.14279/depositonce-834
Main Title: Characterization and Comparison of Formal Refinement and Development Relations for Software Modeling Techniques
Translated Title: Charakterisierung und Vergleich von formalen Refinement und Development Relationen für Softwaremodellierungstechniken
Author(s): Schröter, Gunnar
Advisor(s): Große-Rhode, Martin
Granting Institution: Technische Universität Berlin, Fakultät IV - Elektrotechnik und Informatik
Type: Doctoral Thesis
Language: English
Language Code: en
Abstract: Refinement ist ein Eckstein der formalen Ansätze der Software Modellierung und Refinement- und formale Development-Relationen wurden für verschiedenste formale und semiformale Spezifikationstechniken, sowie verschiedene Arten von Semantiken entwickelt. Ziel dieser Doktorarbeit ist es eigenschaftsbasierte Refinement- und Development-Relationen aus verschiedenen Bereichen in systematischer und formaler Art und Weise zu klassifizieren, zu charakterisieren und zu vergleichen. Im Rahmen dieser Arbeit werden untersucht Programm-Refinement, Data-Refinement, Forward-Simulation und Backward-Simulation aus dem Bereich der zustandsorientierten Modellierungen, Trace-Refinement, Trace-Äquivalenz, Reduction, Extension, Test-Äquivalenz sowie starke und schwache Bisimulation aus dem Bereich der verhaltensorientierten Modelierungskonzept und Reynolds Methode aus dem Bereich der imperativen Programmierung. Die Klassifikation basiert auf einem vereinheitlichendem abstrakten Framework für Development-Relationen. Hier werden Development-Relationen als Relationen über Modellen definiert, welche eine spezifische Klasse von Modelleigenschaften bewahren. Im Falle von Refinement wird eine spezielle Teilklasse von Eigenschaften als vom Kontext der Modelle beobachtbar interpretiert. Eine Refinement-Relation kann klassifiziert werden, als eine bewahrende Refinement-Relation, falls sie die Klasse der beobachtbaren Eigenschaften bewahrt, eine reflektierende Refinement-Relation, falls sie die Klasse der beobachtbaren Eigenschaften reflektiert, oder als eine Refinement-Äquivalenz, falls sie die Klasse der beobachtbaren Eigenschaften sowohl bewahrt, als auch reflektiert. Neben einer Development-Relation kann ein Development-Konzept auch eine regel-basierte Charakterisierung dieser Relation beinhalten. Eine solche regel-basierte Charakterisierung ist eine Menge von Development-Regeln, welche im Hinblick auf die charakterisierte Development-Relation korrekt und vollständig sein muß. Um die verschiedenen Development-Relationen in einer vollständigen und formalen Art und Weise vergleichen zu können, wird jede Development-Relation im Transformations-System Framework charakterisiert, daß heißt, die Development-Relation wird in die Transformations-Systeme und wird durch die Development-Regeln des Frameworks charakterisiert.
Refinement is a cornerstones of formal approaches for software modeling. Thus refinement and formal development relations have been developed for several specification techniques and for different kinds of semantics. The aim of this phd-thesis is to classify, characterize and compare property-based refinement and development relations from different backgrounds in a systematical and formal manner. The thesis pays special attention to Program-Refinement, Data-Refinement, Forward-Simulation and Backward-Simulation from the area of state-oriented models, Trace-Refinement, Trace-Equivalence, Reduction, Extension, Test-Equivalence and Strong and Weak Bisimulation from the area of behavior-oriented modeling concepts and Reynold's Method from the area of imperative programming. The classification is based on a unifying abstract framework for development relations. Here a development relation is defined as a relation over a class of models that preserve a specific class of properties. In the case of refinement a special subclass of properties is interpreted as observable from the context of the models. A refinement relation can be classified as a preserving refinement if it preserves the class of observable properties, a reflecting refinement if it reflects the class of observable properties, i.e. if it preserves the class of negations of observable properties, or as refinement equivalence if it preserves and reflects the class of observable properties. Beside a development relation a development concept can provide a rule-based characterization of the development relation. A rule-based characterization is a set of development rules which is sound and complete with respect to the characterized development relation. To be able to compare the different development relations in a complete and formal manner each development relation is characterized in the transformation system framework, i.e. the development relation is embedded into transformation systems and the embedded relation is characterized by development rules for transformation systems.
URI: urn:nbn:de:kobv:83-opus-7354
http://depositonce.tu-berlin.de/handle/11303/1131
http://dx.doi.org/10.14279/depositonce-834
Exam Date: 19-Nov-2004
Issue Date: 11-Apr-2005
Date Available: 11-Apr-2005
DDC Class: 004 Datenverarbeitung; Informatik
Subject(s): Charakterisierung
Development-Relation
Formale Softwaremodellierung
Refinemt-Relation
Vergleich
Characterization
Comparison
Development Relation
Formal Software Modelling
Refinement Relation
Usage rights: Terms of German Copyright Law
Appears in Collections:Technische Universität Berlin » Fakultäten & Zentralinstitute » Fakultät 4 Elektrotechnik und Informatik » Publications

Files in This Item:
File Description SizeFormat 
Dokument_41.pdf1.21 MBAdobe PDFThumbnail
View/Open


Items in DepositOnce are protected by copyright, with all rights reserved, unless otherwise indicated.