Non-functional properties such as termination or fault tolerance play an important role in the design of distributed algorithms. Static analyses support the design process by automatically determining interesting properties. Which properties can be automatically inferred greatly depends on the specification language and its paradigms. This thesis investigates the suitability of an event-driven specification language regarding its analyzability for certain non-functional properties, where we focus on termination. In an event-driven setting, the interesting aspect of termination is the possibility of control flow loops through communication. In practice, however, it is often difficult to spot the possible communication behaviour of an algorithm at a glance. With a static analysis, the design process can be supported by visualizing possible flow of messages and give hints on possible sources of non-termination. The goal of this work is to describe a specification language for asynchronous distributed algorithms which allows for static termination analysis. At the same time, the language should be easy to use and have prospects of being suitable for the analyses on further non-functional properties. We present a termination analysis which considers the global communication behaviour of an algorithm. From its textual representation, we construct an algorithm’s message flow graph which approximates possible communication. We prove that acyclicity of that graph implies termination. We then discuss the termination criterion’s precision and how it can be improved. Apart from the incorporation of static analysis for sequential programs, we identify cases where cycles are no possible source of non-termination, which eventually allows us to infer termination for a ring algorithm. Furthermore we take a look at expressivity and usability of the language and propose two extensions. The first integrates timers as a way of expressing the detection of failures. The second simplifies the formulation of protocols, also with regard to timeouts. We show that both extensions are compatible with the termination analysis. The work is practically evaluated with the implementation of a termination analysis tool as well as a compiler for a Java-based programming language, producing executable Java bytecode.
Nichtfunktionale Eigenschaften wie Terminierung oder Fehlertoleranz spielen eine bedeutende Rolle beim Design verteilter Algorithmen. Statische Analysen erlauben die Betrachtung solcher Eigenschaften schon während des Entwicklungsprozesses. Inwieweit bestimmte Analyseziele erreicht werden können, hängt bedeutend von der verwendeten Spezifikationssprache ab. Das Ziel dieser Arbeit ist die Beschreibung einer Spezifikationssprache für verteilte Algorithmen, welche sich für statische Analysen auf nichtfunktionale Eigenschaften eignet. Der Fokus liegt dabei auf Terminierung.
Non-functional requirements such as termination or fault tolerance play an important role in the design of distributed algorithms. Static analyses allow the consideration of such properties early on in the design process. To what extent certain analysis goals can be reached largely depends on the specification language in use. The goal of this work is to describe a specification language for distributed algorithms which allows for static analyses of non-functional properties, where the focus is on termination.
Nutzung und Vervielfältigung:
Alle Rechte vorbehalten