Studentenvorträge zu Projekt- und Abschlussarbeiten:

-------------------------------------------------------

Isabella Cortrie: Formal Modelling of a Bandwidth Sharing Mechanism

Bachelorarbeit - betreut von Prof. Mirco Tribastone und Dipl.-Math. Max Tschaikowski

Stochastic process algebra like PEPA are used for a formal modelling of systems of interacting agents. In general, either all agents synchronise or work in parallel. In order to cover synchronisations of subsets of potentially available agents, an extension of PEPA, called GenPEPA, was introduced.

In this thesis, the GenPEPA models of a 2-out-of-3 and 2-out-of-4 communication are veri fied against a number of P2P protocols implemented in Java. Several confi gurations of those are discussed with an emphasis on bandwidths and waiting times. For this experiments, GenPEPA allows for fair performance predictions.

-------------------------------------------------------

Michael Mirwaldt: A lightweight runtime-verification framework for application-specific, state-based protocols in Java with AspectJ

Diplomarbeit - betreut von Dipl.-Inf. Christian Kroiß

Object-oriented programming has evolved in the last decades. Programs in OOP consist of objects that collaborate with one other to solve a problem. They interact with one other much as a team works on a project. As communication between people can fail, inter-object communication can be flawed as well. People, as opposed to computers, have experience and intuition, so that they can elucidate misunderstandings with questions. In contrast, only strict protocols enable computers to detect communication errors. Stateful objects can have methods which may be called only according to a protocol. A common solution for enforcing such protocols uses error-detecting code. This code checks the object state when a method was called and throws an exception if the protocol was violated. This is one possible working solution but it can be flawed and ineffective. The protocol definition is interspersed among all methods which makes maintaining difficult. Moreover, features such as timeouts can hardly be supported. Let us call objects, that observe systems to detect and to indicate protocol violations if they occur, 'protocol checkers'. The use of 'protocol checkers' allows the central definition based on state machines and support special features such as timeouts. Protocol checkers can be configured and customized. Protocol violation information does not tell only what has happened but also details debug information. Protocol checkers can help in testing and maintaining systems and developing fault-tolerant systems. They can improve the code quality and the design.