Enhancing the Fusion Method to FusionB -- Requirements Engineering and Formal Specification --
Bittner, Margot
Basierend auf einer bereits vorhandenen Software Engineering Methode (Fusion/UML) versucht die vorliegende Arbeit erkannte methodische Mängel durch Modifizierung und Erweiterung zu beseitigen. Einige der Hauptmängel sind: - Es fehlen Konzepte zur Unterstützung des Anforderungsanalyseprozesses. - Fehlende Möglichkeiten zur Zusammenführung der Systemmodelle, die verschiedene Sichtweisen des Systems berücksichtigen. - Unbefriedigende Konsistenzregeln um die Korrektheit zwischen Modellen zu überprüfen. Unsere Vorschläge zur Beseitigung dieser Mängel sind: - Unterstützung des Anforderungsanalyseprozesses durch den Subprozess Requirements Determination. - Aufnahme eines neuen Modells und neue Modellierungselemente in die Notation. - Hinzufügen von neuen Konsistenzregeln. - Ableitung einer einheitlichen formalen Spezifikation aus den bereits vorhanden Modellen. - Aufnahme von Teilen der Anforderungen in die formale Spezifikation. - Modifizierung einzelner Modelle der Methode. Ziel in dieser Arbeit ist es, zu zeigen, dass es machbar ist, Teile des Anforderungsanalyseprozesses und der formalen Spezifikation in FusionB zu integrieren. Anforderungsbeschreibung und formale Beschreibung werden in die vorhandene objektorientierte Methode eingebunden Dazu werden neue Modelle und Modellierungselemente entwickelt und in die Notation von FusionB aufgenommen. Die erste Erweiterung beschäftigt sich mit der Sammlung, Klassifizierung und Formalisierung von Anforderungen an das zu entwickelnde System. Der Prozess zur Anforderungsbestimmung wird be schrieben. Dabei wird der Schwerpunkt gelegt auf die Identifizierung von Domänen in dem Anwen dungsgebiet, daraus Anforderungen und nichtrelevanten Aussagen (non-responsible statements) von diesen Domänen extrahiert, Anforderungen klassifiziert und wenn möglich formalisiert. Die bereits am Anfang der Analyse in einer logischen Sprache ausgedrückten Anforderungen haben auf einige Modelle (z.B. Operationsmodel, Objektinteraktionsmodel) der Methode besonderen Einfluss. Die Konsistenzüberpüfung zwischen den Modellen wird durch das Einfügen der Anforde rungen erweitert. Präzise Definitionen der Anforderungen aus der Problembeschreibung und das Ein betten dieser Informationen haben einen positiven Einfluss auf die Methode und alle Informationen der Pro blembeschreibung werden dadurch teil der Methode. Da bereits bei der Anforderungsanalyse Akteure , Use Cases und ihre Kommunikation untereinander erkennbar sind, erleichtert dies die Erstellung des Use Case Modells erheblich. Ausserdem können die Anforderungen zum Zwecke des Tracings mit anderen Modellen der Methode verknüpft werden. Modellierungselemente vorhandener Modelle müssen für das Vorwärts- und Rückwärts-Tracing ange passt werden. Die beiden wichtigsten Modelle in Fusion, welche den Systemzustand beschreiben, sind das Operationsmodell und das Objektinteraktionsmodell. Sie konzentrieren sich auf die Struktur des Systems. Kein anderes Modell der Methode leistet dieses. Das Operationsmodell beschreibt formal die Zu- standsänderung des Systems, die durch die Umgebung ausgelöst wird. Das Objektinteraktionsmodell hingegen beschreibt die Zustandsänderung durch die Modellierung des Nachrichtenflusses zwischen den Objekten des Systems. Das Operationsmodell liefert eine Konsistenz für den zu entwickelnden Entwurf: systematische Übersetzung der beiden Hauptergebnisse des Prozesses in die formalen Beschreibungen in Object-Z. Wir konnten zeigen, dass eine mechanische und systematische Übersetzung möglich ist. Die pragmatische Herangehensweise verlangt jedoch mehr theoretische Arbeit um zu einer genaueren Verifikation der Systemeigenschaften zu gelangen. Das Ergebnis der Übersetzung in Object-Z Klassen ermöglich die Klassen mit Init Operationen und Klasseninvarianten, zu erweitern. Der Vorteil die Klasseninvarianten aus der Anforderungsbeschreibung auszuwählen, besteht darin, dass Aussagen der Anforderungen in der gleichen Sprache formalisiert werden können wie das Operationsmodell und die Object-Z Klassen.
Starting from an existing software engineering method, the thesis looks at ways of eliminating what have been recognized as the method's deficiencies by modifying and extending it. Our aim in this thesis has been to show that it is feasible to integrate parts of requirements engineering and formal specification into FusionB, and that it is possible to incorporate the requirements description and the formal description into an existing object-oriented development method. New model and modelling elements are designed and integrated into the notation of FusionB. The first extension to Fusion/UML deals with gathering, classifying and formalizing requirements for the system that is to be built. Formalizing requirements in a logical language at this early stage of analysis also has an impact on the other models of the method. The two most important models in Fusion/UML for describing the system state are the Operation Model and Object Interaction Model. These two models are the ones that focus on the structure of the system. No other model in the method does this. The Operation Model describes the change state of the system which is triggered by the environment in a formal way. The Object Interaction Model describes the change of state of the system by modelling the method flow between the objects of the system. It provides a consistency for the developed design: systematic translation of the two main results of the process, the Operation Model and the Object Interaction Model, into the formal description using Object-Z. We have shown that a mechanical and systematic translation is possible. Here, we have demonstrated a specific aspect of formalization. It is a pragmatic approach that requires more theoretical work in order to be generalized and to enable a more rigorous verification of system properties. The extensions made to the method have been evaluated in two case studies.
