Zur Rolle von Nichtdeterminismus und Verfeinerung in der modellgetriebenen Top-Down-Entwicklung von Softwaresystemen

Large-scale software systems need to be accurately planned and designed. This includes the determination of requirements, the definition of specifications, and the development of models conforming to specifications. These models are expressed in modeling languages like process algebras, the Unified Modeling Language (UML), or variants of state diagrams (e.g. UML state machines or Harel's statecharts). Such modeling languages are usually underspecified, since they only express certain aspects of the system to be designed, leaving out implementation details. The process of refining such abstract descriptions in a stepwise fashion, until finally the concrete, executable implementation is reached, is called (model-driven) top-down development. Finding bugs as early as possible in this process often saves considerable development costs. This thesis considers methods for proven-to-be-correct top-down development, with specification conformance being guaranteed at all levels of abstraction, either by applying model checking techniques or by employing pre-defined refinement patterns that are already proven to be sound. In order to apply formal proof methods, models on all levels of abstraction, e.g. presented as process algebra terms or state diagrams, need to be given a precise semantics in some semantic domain, usually based on (extensions of) labeled transition systems. We call semantic domains that support underspecification refinement settings. One of the contributions of this thesis is a new kind of comparison of a dozen such settings proposed in the literature with respect to their expressible sets of implementations. This comparison is done by providing transformations that not only establish the implementation-based expressiveness hierarchy of the most commonly used refinement settings, but can also be employed to convert models between the settings, thus enabling tool reuse. Some kinds of abstract models require a setting as semantic domain that not only features resolvable nondetermism expressing underspecification, but also persistent nondeterminism that is not to be resolved in refinements, as characterized by bisimulation equivalence on labeled transition systems. We show that such a setting is needed for process algebras if they specify concurrent systems, because concurrency may introduce resolvable nondeterminism which is resolved by the scheduler of the operating system, and the choice operator, which is common to process algebras, may correspond to persistent nondeterminism. This is the first work in the literature making this observation. A simple process algebra of this kind is given an operational semantics, using the refinement setting of mu-automata, as well as a sound and complete axiomatic semantics. Sometimes state diagrams, such as UML state machines or Harel's statecharts, also require a refinement setting with both kinds of nondeterminism, because (i) they are underspecified and (ii) the underlying action language may contain operators exhibiting persistent nondeterministic behavior. This thesis is the first publication presenting a state diagram semantics with both kinds of nondeterminism. In this context, existing refinement settings like mu-automata lead to unnecessarily complex semantic models. Therefore, we develop a new and in this context more succinct refinement setting, called nu-automata, and give a semantic mapping for a simple state diagram variant, as well as a general transformation that can be applied when extending existing semantics by persistent nondeterminism. Thus, we make state diagrams accessible to persistent nondeterminism. Support for both kinds of nondeterminism, however, does not necessarily imply the practical feasibility of top-down development in state diagrams. In existing state diagram variants, expressing resolvable nondeterminism is only possible to a certain degree, because the notations for underspecification (i) often have no precise semantics, and (ii) are not expressive enough to reflect the requirements of the top-down development process, such as starting with interface definitions and subsequent parallel development of mostly independent modules. Therefore, we develop a new variant of state diagrams that allows more explicit and more expressive modeling of underspecification than existing variants. This variant is given a semantics in a newly developed semantic setting that distinguishes between input and output events. A set of refinement patterns is then provided that enables proven-to-be-correct stepwise refinement without the need to re-check correctness after each refinement step. Consequently, we deliver the formal foundations for the development of a state-diagram-based design tool that ensures correctness at all stages of the development process. Große Softwaresysteme bedürfen sorgfältiger Planung und Entwicklung, einschließlich einer Anforderungsanalyse, dem Aufstellen von Spezifikationen und der Entwicklung von Modellen, die die Spezifikation einhalten. Solche Modelle werden in Modellierungssprachen wie Prozessalgebren, der Unified Modeling Language (UML) oder Varianten von Zustandsdiagrammen (z.B. UML state machines oder Harel's statecharts) ausgedrückt. Diese Modellierungssprachen sind üblicherweise unterspezifiziert, d.h. sie beschreiben nur bestimmte Aspekte des zu entwickelten Systems und lassen Implementationsdetails weg. Der Prozess, solche abstrakten Beschreibungen schrittweise zu verfeinern, bis schließlich die konkrete, ausführbare Implementation erreicht ist, wird (modellgetriebene) Top-Down-Entwicklung genannt. Es spart oft beachtliche Entwicklungskosten, wenn Programmierfehler so früh wie möglich in diesem Prozess gefunden werden. Die vorliegende Arbeit betrachtet Methoden für per-Konstruktion-korrekte Top-Down-Entwicklung, für die Spezifikationstreue auf allen Abstraktionsstufen gewährleistet ist, entweder durch die Anwendung von Modelchecking-Techniken oder durch die Verwendung von vordefinierten Verfeinerungsmustern, deren Korrektheit bereits bewiesen ist. Um formale Methoden anwenden zu können, muss den Modellen auf allen Abstraktionsstufen, ausgedrückt etwa in Prozessalgebren oder Zustandsdiagrammen, eine präzise Semantik gegeben werden. Solche Semantiken werden üblicherweise mittels (Erweiterungen von) Transitionssystemen ausgedrückt. Wir nennen solche semantischen Formalismen, die Unterspezifikation unterstützen, Verfeinerungsformalismen. Einer der Beiträge dieser Arbeit ist eine neue Art von Vergleich von einem Dutzend solcher Formalismen, in Hinblick auf ihre ausdrückbaren Mengen von Implementationen. Dieser Vergleich erfolgt durch die Angabe von Transformationen, die nicht nur die implementationsbasierte Ausdrucksstärkenhierarchie der meistbenutzten Verfeinerungsformalismen begründen, sondern auch dafür verwendet werden können, Modelle zwischen Formalismen zu konvertieren und damit die Wiederverwendung von Werkzeugen zu ermöglichen. Einige abstrakte Modelle benötigen einen semantischen Formalismus, der nicht nur auflösbaren Nichtdeterminismus für das Ausdrücken von Unterspezifikation, sondern auch persistenten Nichtdeterminismus enthält. Letzterer soll nicht in Verfeinerungen aufgelöst werden, wie es durch Bisimulationsäquivalenz auf Transitionssystemen charakterisiert wird. Wir zeigen, dass ein solches Modell für Prozessalgebren im Kontext nebenläufiger Systeme benötigt wird, weil Nebenläufigkeit auflösbaren Nichtdeterminismus einführen kann, der vom Scheduler des Betriebssystems aufgelöst wird, und der Choice-Operator, welcher in Prozessalgebren üblich ist, persistentem Nichtdeterminismus entsprechen kann. Dieses ist die erste publizierte Arbeit, die diese Beobachtung macht. Wir geben für eine einfache Prozessalgebra eine operationelle Semantik mittels mu-Automaten, sowie eine korrekte und vollständige axiomatische Semantik an. Auch Zustandsdiagramme wie UML state machines oder Harel's statecharts benötigen manchmal semantische Formalismen mit beiden Arten von Nichtdeterminismus, weil Zustandsdiagramme (i) unterspezifiziert sind und (ii) die zugrundeliegende Aktionssprache Operatoren enthalten kann, die persistent-nichtdeterministisches Verhalten zeigen. Die vorliegende Arbeit ist die erste, die eine Zustandsdiagramm-Semantik mit beiden Arten von Nichtdeterminismus vorstellt. In diesem Kontext würden existierende semantische Modelle wie mu-Automaten zu unnötig komplexen semantischen Modellen führen. Daher entwickeln wir einen neuen, in diesem Kontext bündigeren Verfeinerungsformalismus, nämlich nu-Automaten, und geben eine semantische Abbildung für eine einfache Zustandsdiagrammvariante, sowie eine allgemeine Transformation an, die auf existierende Semantiken, die um persistenten Nichtdeterminismus erweitert werden sollen, angewendet werden kann. Wir machen also Zustandsdiagramme im Allgemeinen für persistenten Nichtdeterminismus zugänglich. Die Unterstützung von beiden Arten von Nichtdeterminismus impliziert jedoch nicht notwendigerweise die praktische Umsetzbarkeit von Top-Down-Entwicklung in Zustandsdiagrammen. In existierenden Zustandsdiagrammvarianten ist das Ausdrücken von auflösbarem Nichtdeterminismus nur zu einem gewissen Grade möglich, weil die Notationen für Unterspezifikation (i) oft keine präzise Semantik haben, und (ii) nicht ausdrucksstark genug sind, um die Anforderungen des Top-down-Entwicklungsprozesses widerzuspiegeln, wie das Starten mit der Definition von Schnittstellen und nachfolgende parallele Entwicklung größtenteils unabhängiger Module. Daher entwickeln wir eine neue Zustandsdiagrammvariante, die expliziteres und ausdrucksstärkeres Modellieren von Unterspezifikation als existente Varianten unterstützt. Ihre Semantik wird in einem neu entwickelten semantischen Formalismus gegeben, der zwischen Eingabe- und Ausgabeereignissen unterscheidet. Eine Kollektion von gegebenen Verfeinerungsmustern erlaubt korrekt-bewiesene schrittweise Verfeinerung, ohne dass die Korrektheit nach jedem Verfeinerungsschritt erneut bewiesen werden muss. Wir liefern also die formale Basis für die Entwicklung eines zustandsdiagrammbasierten Entwicklungswerkzeugs, welches Korrektheit in allen Stadien des Entwicklungsprozesses sicherstellt.