Autoren: Jochen Messner

An algorithm is presented solving the factor problem in trace monoids. Given two traces represented by words, the algorithm determines in linear time whether the first trace is a factor of the second one. The space used for this task is linear in the length of the first word. Similar to the Knuth-Morris-Pratt Algorithm for the factor problem on words, the algorithm simulates a finite automaton determined by the first word on the second word. To develop the algorithm, we examine overlaps of two traces, and show that they form a lattice. Finally we investigate the lattice of extensible trace pairs (which represent still extensible prefixes of a searched factor appearing in some other trace), because of their close relations to the structures used by the algorithm.

PDF

Autoren: Wolfgang Lindner, Rainer Schuler

PDF

Autoren: Thomas Bauer, Peter Dadam

If the number of users within a workflow management system (WFMS) increases, a central workflow server (WF-server) and a single local area network (LAN) may become overloaded. The approach describes an execution environment which is able to manage a growing number of users by adding new servers and subnets. The basic idea is to decompose processes into parts which are controlled by different WF-servers. That is, during execution of a workflow instance its execution (step) control may migrate from one WF-server to another. By selecting the appropriate physical servers (for hosting the WF-servers) in the appropriate LANs, communication costs and individual WF-server workload can be reduced significantly.

PDF

Autoren: Christian Heinlein, Peter Dadam

Current workflow management technology does not provide adequate means for describing and implementing workflow ensembles, i.\,e., dynamically evolving collections of more or less independent workflows which have to synchronize only now and then. Interaction expressions are proposed as a simple yet powerful formalism to remedy this shortcoming. Besides operators for sequential composition, iteration, and selection, which are well-known from regular expressions, they provide parallel composition and iteration, conjunction, and several advanced features like parametric expressions, multipliers, and quantifiers. The paper introduces interaction expressions semi-formally, gives examples of their typical use, and describes their implementation and integration with state-of-the-art workflow technology. Major design principles, such as orthogonality and implicit and predictive choice, are discussed and compared with several related approaches.

PDF

Autoren: Vikraman Arvind, Johannes Köbler

In this paper we extend a key result of Nisan and Wigderson to the nondeterministic setting: for all alpha>0 we show that if there is a language in E=DTIME(2^{O(n)

PDF

Autoren: Gerhard Partsch

Der europäische Mobilfunkstandard DECT1 wird zur Zeit noch fast ausschließlich zur Sprachkommunikation eingesetzt. In dem vorliegenden Bericht werden Konzepte und prototypische Implementierungen vorgestellt, die DECT-Systeme auch für die Datenkommunikation und den LAN2 -Betrieb nutzbar machen. Die wichtigsten Ergebnisse dieses Berichtes lassen sich in folgenden Punkten zusammenfassen: - Basis für die in diesem Bericht vorgestellten DECT-basierenden Datenkommunikationslösungen sind Punkt-zu-Punkt- und Mehrpunkt-Verbindungen. - Die entwickelten DECT/LAN-Netzwerktreiber unterscheiden sich bezüglich ihrer Software-Schnittstellen (zum Betriebssystem und zu den Transportprotokollen) nicht von klassischen Netzwerktreibern wie Ethernet oder Token-Ring. Daraus folgt, daß sind über die in diesem Bericht entwickelten DECT/LAN-Netzwerktreiber alle am Markt verfügbaren Netzwerkarchitekturen (z.B. Microsofts LAN-Manager, Novells Netware oder der TCP/IP-Protocolstack) und LAN-Applikationen ohne Modifikationen betreiben lassen, d.h. es ist volle Software-Kompatibilität gegeben - Die Kopplung mehrerer DECT-basierender LANs untereinander und mit klassischen LAN-Lösungen wie z.B. Ethernet oder Token-Ring ist möglich, d.h. die in diesem Bericht vorgestellten DECT/LAN-Lösungen stellen keine Insellösung dar.

PDF

Autoren: Manfred Reichert, Peter Dadam

Current process-oriented workflow technology is only applicable in a secure and reliable manner if the business process (BP) to be supported is well-structured and there is no need for dynamic extensions or ad hoc deviations at runtime. As only few BPs are statically in this sense, this limits the applicability of today's workflow management systems (WFMSs) significantly. On the other hand, to support deviations from the premodeled task sequences at runtime should not mean that the responsibility for the avoidance of consistency problems (e.g., unintended lost updates) or even runtime errors (e.g., program crashes due to the invocation of task modules with invalid or missing parameters) is now completely shifted to the (naive) end user. Instead, a formal foundation must be established that allows the runtime system to decide whether an intended deviation can be handled in a proper and secure manner. In this paper we present a conceptual and operational framework for the support of dynamic structural changes of workflows (WFs) in WFMSs. Based upon a simple WF model (ADEPT) we define a complete and minimal set of change operations (ADEPTflex) that support users in modifying the structure of WFs at runtime, while maintaining their correctness and consistency. Correctness properties defined by the ADEPT model are used to determine whether a specific change can be applied to a given WF or not. If these properties are violated the change is either rejected or the correctness must be restored by handling the exceptions resulting from the change. Further, we discuss basic issues with respect to the management of changes and the undoing of temporary changes when backward operations are applied. The change facilities presented in this paper will form a key part of process flexibility in future WFMSs.

PDF

Autoren: Hans Braxmeier, Dietmar Ernst, Andrea Mößle, Heiko Vogler

This paper presents the functional programming language NoName and its development environment. NoName has been developed in order to test evaluation and transformation strategies. A great advantage of NoName is the fact that special recursive program schemes and a call-by-value as well as a call-by-name evaluation of functions are supported explicitely. The main part of the NoName development environment is a syntax driven editor which is enriched by several user-friendly features, e.g., an online help. Also some transformations are integrated which may improve the programs efficiency.

PDF

Autoren: Christian Heinlein

Dieser Bericht stellt eine umfassende Einführungin die Grundlagen von Interaktionsausdrücken dar und dient damit gleichermaßen als ,,Tutorium`` und als ,,Referenzhandbuch´´ zu diesem Formalismus.Obwohl Interaktionsausdrücke primär mit der Zielsetzung entwickelt wurden, einen geeigneten Formalismus zur Beschreibung (und Implementierung) von Inter-Workflow-Abhängigkeiten zur Verfügung zu stellen, ist ihre Anwendbarkeit nicht auf dieses spezielle Gebiet beschränkt. Vielmehr stellen sie einen sehr allgemeinen Formalismus zur Beschreibung (und damit zur Lösung) nahezu beliebiger Synchronisationsprobleme dar. Aus diesem Grund werden Interaktionsausdrücke in diesem Bericht unabhängig von der speziellen Anwendungsdomäne Inter-Workflow-Abhängigkeiten eingeführt und mit Beispielen aus ganz unterschiedlichen Bereichen veranschaulicht.

PDF

Autoren: Christian Heinlein

Dieser Bericht stellt eine einfache graphische Notation für Interaktionsausdrücke vor, wie sie in den Berichten ''Grundlagen von Interaktionsausdrücken'' (UIB 97-09) und ''Interaction Expressions -- A Powerful Formalism for Describing Inter-Workflow Dependencies'' (UIB 97-04) beschrieben sind.

PDF

Autoren: Christian Heinlein

Dieser Bericht definiert Interaktionsausdrücke, wie sie in den Berichten ''Grundlagen von Interaktionsausdrücken'' (UIB 97-09) und ''Interaction Expressions -- A Powerful Formalism for Describing Inter-Workflow Dependencies'' (UIB 97-04) beschrieben sind, mittels ihrer sprachtheoretischen Semantik.

PDF

Autoren: Gerhard Schellhorn, Wolfgang Reif

The paper describes a problem set for automated theorem provers taken from a KIV case study in software verification. The goal is to prove 45 consequences of the axioms specifying the data type of finite enumerations. We present a structured algebraic specification of finite enumerations with 102 axioms. 52 theorems are given, 45 of which can be proved without induction (some of them rely on the 7 inductive consequences). Results for the 5 automated theorem provers Otter, Protein, Setheo, Spass and 3TAP are given for two versions, with and without an axiom reduction preprocessing step. Test files are available for each of the provers and also in the common syntax of the DFG-Schwerpunkt "Deduktion".

PDF

Autoren: Dietmar Ernst, Frank Houdek, Wolfram Schulte, Thilo Schwinn

Methoden der Softwareprüfung gliedern sich in dynamische und statische Verfahren. Diese Arbeit präsentiert einige Ergebnisse eines Experiments, das im Rahmen des Softwarelabor Ulm für die Daimler-Benz AG angefertigt wurde. In diesem Experiment vergleichen wir Tests und Reviews für das Umfeld eingebetteter Systeme. An der Durchführung des Experiments waren 12 Studenten beteiligt. Wichtige Ergebnisse waren, daß mit Reviews mehr Fehler entdeckt wurden als mit dem strukturellen oder funktionalen Test. Auch unter Berücksichtigung der dazu nötigen Aufwände schneidet die statische Prüftechnik deutlich besser als die dynamische ab. In Hinblick auf die bei den jeweiligen Prüfmethoden besser gefundenen Fehlerarten gab es keine signifikanten Unterschiede.

PDF

Autoren: Wolfgang Reif, Gerhard Schellhorn

This paper investigates the performance of automated theorem provers in formal software verification. The challenge for the provers in this application is the large number of (up to several hundred) axioms in typical software specifications. Both the success rates and the proof times strongly depend on how good the provers are able to find out the few relevant axioms that are really needed in the proofs. We present a reduction technique for this problem. It takes the axioms of a theory and a theorem and computes a reduced axiom set by eliminating as many irrelevant axioms as possible. The proof search for the theorem then is performed in the reduced set. Comparative experiments with five automated theorem provers show that with the reduction technique they can prove more theorems than before, and were faster for those that could be proved already without reduction.

PDF

Autoren: Thomas Wennekers

Die Analyse des globalen zeitlichen Verhaltens der Aktivität in großen neuronalen Netzen erfordert die Reduktion der hoch-dimensionalen Netzwerkgleichungen auf kleine, mathematisch leichter zugängliche Gleichungssysteme. In dieser Arbeit wird eine Klasse stochastisch gekoppelter Integro-Differentialgleichungen betrachtet, die eine Verallgemeinerung häufig verwendeter zeitkontinuierlicher Modelle neuronaler Netze mit graduellen, sigmoiden Neuronen darstellt. Es werden Bedingungen an die Dynamik der Einzelneurone und die statistischen Eigenschaften der Kopplungen angegeben, unter denen das betrachtete System asymptotisch in der Systemgröße und der Zeit exakt auf ein niedrigdimensionales System reduziert werden kann. Hierbei können die Einzelzellen mehrkomponentig, schwach nichtlinear und zeitabhängig sein; Kopplungen werden in Form von Responsekernen mit statistischen Parametern erfaßt.

PDF

Autoren: Peter Dadam, Klaus Kuhn, Manfred Reichert

There is an increasing interest in changing information systems to support business processes in a more direct way. This means to actively deliver the tasks to be performed to the right persons at the right point in time with the necessary information and application functions needed for performing these tasks. Process-oriented workflow technology is a very interesting candidate to achieve this goal. In fact, many companies have already started to implement information systems based on this kind of technology. Hence the important question arises, how far do we get using this technology. Is the functionality provided powerful enough to support a wide range of application scenarios or is it only suitable for rather simple applications? And, if the latter is the case, are the missing functions of the "just to do" type or are more fundamental issues addressed? The paper uses the clinical application scenario to explain, to motivate, and to elaborate the functionality needed to adequately support an advanced (and challenging) application environment. It shows that workflow technology is still lacking very important features and concepts to serve this domain. Although the clinical domain is used for explanatory purposes, the problems addressed are also valid for other non-trivial application areas. The paper surveys the state of the art in the areas addressed and presents possible solutions for some of the issues based on the concepts elaborated in the ADEPT project.

PDF

Autoren: Mohammad Ali Livani, Jörg Kaiser

This document reports the results of our research on methods to implement a distributed scheduling mechanism for CAN-bus resource in order to meet the requirements of a dynamic distributed real-time system. The key issues considered here, are distinguishing between hard real-time, soft real-time, and non real-time constraints, achieving high resource utilization for CAN-bus, and supporting dynamic real-time computing by allowing dynamic assignment of guaranteed communication resources.

PDF

Autoren: Johannes Köbler, Rainer Schuler

We use the assumption that all sets in NP (or other levels of the polynomial time hierarchy) have efficient average-case algorithms to derive collapse consequences for MA, AM, and various subclasses of P/poly. As a further consequence we get that PP = P if all sets in P(PP) are efficiently decidable on average.

PDF