Zur Seitenansicht
 

Titelaufnahme

Titel
Generische Refactoring-Spezifikation für Korrektheitsbeweise in mehrsichtigen Modellsprachen
AutorRuhroth, Thomas In der Gemeinsamen Normdatei der DNB nachschlagen
PrüferWehrheim, Heike In der Gemeinsamen Normdatei der DNB nachschlagen ; Becker, Steffen In der Gemeinsamen Normdatei der DNB nachschlagen
Erschienen2011
HochschulschriftPaderborn, Univ., Diss., 2011
Anmerkung
Tag der Verteidigung: 16.06.2011
SpracheDeutsch
DokumenttypDissertation
URNurn:nbn:de:hbz:466:2-8971 Persistent Identifier (URN)
Dateien
Generische Refactoring-Spezifikation für Korrektheitsbeweise in mehrsichtigen Modellsprachen [2.61 mb]
Links
Nachweis
Klassifikation
Zusammenfassung (Deutsch)

In der Softwareentwicklung sollen Code und Modelle wartbar sein. Refactorings sind ein bewährtes Hilfsmittel der Codeentwicklung, um die innere Qualität von Code zu verbessern. Refactorings sind Änderungen am Code, wobei das sichtbare Verhalten unverändert bleibt. Diese Verbesserungen sind auch für formale Modelle erstrebenswert. Modelle sind im Gegensatz zu Programmen meist nicht ausführbar, daher ist es notwendig die verwendeten Refactoringtechniken anzupassen. Beispielsweise muss eine brauchbare Definition der Verhaltenserhaltung gefunden werden, da ein Modell nicht ausführbar ist. Häufig werden mehrere Sichten in Modellen eingesetzt, um verschiedene Aspekte eines Modells abzubilden. Um mehrere Sichten unterstützen zu können, müssen bestehende Techniken weiter angepasst werden.Ziel dieser Arbeit ist die Darstellung von mehrsichtigen Refactorings und die Sicherstellung der Verhaltenserhaltung der Refactorings für formale Modelle. Es wird die Sprachfamilie ReL (Refactoring Language) genutzt, um Refactorings von einer einfachen imperativen Programmiersprache (FWHILE) und einer integrierten formalen Methode (CSP-OZ) zu beschreiben. ReL ermöglicht durch seine Struktur, dass die Verhaltenserhaltung direkt bewiesen werden kann, ohne auf eine andere Darstellung zurückgreifen zu müssen. Für die Beschreibung wird die Sprachfamilie ReL genutzt, die Refactorings anhand des Codezustandes vor und nach dem Refactoring beschreibt. Dies wird durch Templates beschrieben, deren Subtemplates Refactorings mehrsichtiger Modelle unterstützen. Die Struktur von ReL erlaubt sowohl die Ausführung eines Refactorings in einer Entwicklungsumgebung als auch die formale Analyse.

Zusammenfassung (Englisch)

In software development it is necessary that program code and models can be maintained. Refactoring is a best practice in code development which can be used to improve the internal quality of given code. Refactoring means modifying code without changing its behaviour. It is also desirable to improve the internal quality of formal models. Unlike programs most models are not executable. Thus, refactoring techniques need to be adapted. For example, a suitable definition of behaviour preservation is needed. A technique often used in the context of models is the usage of multiple views on one model, e.g. to specify several aspects using different diagrams. This also implies the need to adapt existing refactoring techniques.The aim of this work is to describe refactorings of formal models and to ensure the behaviour preservation of these refactorings. The language family ReL (Refactoring Language) is used to describe refactorings of simple imperative programs (FWHILE) and specifications given in an integrated formal method (CSP-OZ). In particular, the structure of ReL allows proving behaviour preservation without transferring the refactoring to a different representation.ReL uses templates to describe the state of the code before and after the refactoring. These templates are divided into subtemplates. These subtemplates can be used in different views and therefore provide the possibility to describe multi-view refactorings. Also the structure of ReL allows a refactoring to be applied to a model as well as the formal analysis. ReL is derived using techniques of Domain Specivic Languages. Thus, ReL depends on the syntax definition of the language to be refactored. This process allows ReL to derive a ReL-Instance for all languages that be described as Backus-Naur Form (BNF). The application is therefore not restricted to formal model languages, but can also be applied to programming languages.