Autoren: Daniela Damm, Lutz Claes, Friedrich W. von Henke, Alexander Seitz, Adelinde Uhrmacher, Steffen Wolf

Im Projekt SILK wurden fallbasierte Methoden kozipiert und implementiert, die es dem Wissenschaftler erlauben, den Stand der experimentellen Forschung systematisch zu analysieren, neue Ergebnisse im Kontext anderer einzuordnen und ausgewählte Fragestellungen der Wissenschaftler auf dieser Basis effizient zu beantworten. Als exemplatrischer Anwendungsbereich diente das Gebiet der Knochenheilung.

PDF

Autoren: Thomas Bauer, Peter Dadam

In unternehmensweiten Workflow-Management-Systemen (WfMS) kann die von der WF-Engine zu bewältigende Last sehr groß werden. Außerdem werden hohe Anforderungen an die Verfügbarkeit eines solchen Systems gestellt. Deshalb wurden in der Literatur zahlreiche Architekturen für skallierbare WfMSe vorgeschlagen, die auf unterschiedlichen Verteilungen der WF-Engine basieren. Diese Architekturen werden in dem Beitrag verglichen und klassifiziert. Des weiteren wird die Belastung der einzelnen Systemkomponenten analysiert und die Ansätze werden auf Schwachstellen hin untersucht. Die gewonnenen Erkenntnisse werden verwendet, um eine Ent\-schei\-dungs\-hilfe für die Auswahl einer geeigneten Architektur für bestimmte Anwendugstypen zu geben.

PDF

Autoren: Marko Luther, Martin Strecker

This report gives a survey of Typelab, a specification and verification environment that integrates interactive proof development and automated proof search. Typelab is based on a constructive type theory, the Calculus of Constructions, which can be understood as a combination of a typed lambda-calculus and an expressive higher-order logic. Distinctive features of the type system are dependent function types for modeling polymorphism and dependent record types for encoding specifications and mathematical theories. After presenting an extended example which demonstrates how program development by stepwise refinement of specifications can be carried out, the theory underlying the prover component of Typelab is described in detail. A calculus with metavariables and explicit substitutions is introduced, and the meta-theoretic properties of this calculus are analyzed. Furthermore, it is shown that this calculus provides an adequate foundation for automated proof search in fragments of the logic.

PDF

Autoren: Heiko Neumann, Luiz Pessoa

We study the problem of the reconstruction of achromatic surface properties, namely brightness. We show that the filling-in of brightness through a diffusion process can be linked to the general framework of feature reconstruction through regularization theory that is widely used in computer vision. In particular, it will be shown that brightness filling-in is a means of reconstructing smooth information from local contrast data that minimizes first order derivative information. Our investigation provides a formal link between modeling perceptual data for biological vision and the mathematical frameworks of regularization and linear spatially variant diffusion. The present analysis of filling-in in also suggests a new diffusion mechanism that effectively employs confidence information. Simulations on psychophysical stimuli illustrate the mechanism's potential.

PDF

Autoren: Ercüment Canver

Coordinated atomic actions (CAAs) have been used in a semi-formal way for the design of the production cell case study. This paper presents a formal specification and verification of the production cell building on this design. However, this report is not intended to present yet another formalization of the production cell case study but rather as an approach to formalizing a CAA based system design in order to formally verify its properties. Each CAA is modeled as an atomic state transition characterized by its pre- and postconditions. In order for such transitions to become enabled, conditions are formalized requiring all associated roles to be activated. Activation of roles is performed by controllers, which are again modeled in terms of state transitions. The state space of the production cell can be viewed as being finite; hence, the production cell is specified as a finite state transition system and the formal verification of the CAA-design is carried out using model-checking.

PDF

Autoren: Andreas Küchler

The folding architecture together with adequate supervised training algorithms is a special recurrent neural network model designed to solve inductive inference tasks on structured domains. Recently, the generic architecture has been proven as a universal approximator of mappings from rooted labeled ordered trees to real vector spaces. In this article we explore formal correspondences to the automata theory in order to characterize the representational capabilities of different instances of the generic folding architecture. As the main result we prove that simple instances of the folding architecture have the computational power of at least the class of deterministic bottom-up tree automata. All proofs are carried out in a constructive manner and a detailed analysis of the space complexity of the construction schemes is provided. We derive bounds for the principled node complexity of folding architecture implementations of tree automata. The possible embedding of the neural folding architecture into a general knowledge-injection-refinement-
extraction framework is briefly discussed.

PDF

Autoren: Heiko Neumann, Thorsten Hansen, Luiz Pessoa

We propose a novel model of visual contrast measurement based on segregated pathways that are fed by responses from initial ON and OFF center-surround processing. The primary goals of our investigation were to (1) establish a mechanism selective for sharp local transitions in the luminance distribution; and (2) to generate a robust scheme of oriented contrast detection. The resulting circuit realizes a soft AND-gate mechanism and is selective to proper scales in a linear scale-space of the current signal.

PDF

Autoren: Thomas Wennekers

The concept of synfire chains has been proposed by Abeles as a reasonable biophysical model for cortical long-time correlations and replicating spike patterns in multi unit recordings. Some recent computational modelling approaches extend the model into a functional direction proposing that the synchronization of synfire chains may help to solve the binding problem of cortical information processing. In the present paper we investigate further computational aspects of synfire chains. First, we show how they can be used as spatio-temporal feature stores capable to learn, regenerate and recognize spatio-temporal signals. Thereby synfire chains introduce time into the static world of attractor neural networks as paradigms for cortical information processing. Then we extend the synfire chain model from linear autonomously evolving networks to graph-like structures with external input signals. Such `synfire graphs' can implement arbitrary deterministic and nondeterministic finite state automata. We prove formally that synfire graphs consisting of time-continuous spiking neurons can robustly process arbitrary long input words even if realistic postsynaptic potentials, bounded background noise and spike-timing jitter are taken into consideration. A single synfire node may consist of a single spiking neuron or a larger set of cells. In the latter case connections between two nodes can be diluted or have otherwise random synaptic efficacies. The extension of synfire chains to synfire graphs introduces operational (logical, procedural, cognitive) components into common modelling of Hebbian cell assemblies and brain functioning.

PDF

Autoren: Thomas Bauer, Peter Dadam

In diesem Beitrag wird ein Verfahren fŸr die Berechnung einer optimalen Verteilung für die Aktivitäten eines Workflows vorgestellt. Es wird berücksichtigt, da§ in Bearbeiterbeschreibungen vorausgegangene Aktivitäten referenziert werden können, weshalb die Menge der potentiellen Bearbeiter und damit der optimale Server erst zur Laufzeit feststeht.

PDF

Autoren: Heiko Neumann, Wolfgang Sepp

A computational model is proposed for feedforward and feedback interaction in early visual information processing. The neural network model realizes an architecture for dynamic feature detection and top-down hypothesis generation. The recurrent interaction provides a mechanism for hypothesis testing and input data selection. Simulations demonstrate that the model realizes mechanisms of local grouping of fragmented shape outline, and explains texture surround and density effects, and the interpolation of illusory contours.

PDF

Autoren: Frank Houdek, Dietmar Ernst, Thilo Schwinn

Die Softwareprüfung spielt bei der Softwareentwicklung eine wesentliche Rolle. Daher wurden hierzu in den letzten Jahren auch eine Vielzahl von Techniken entwickelt. Allerdings gibt es bisher nur wenig empirisch gesicherte Aussagen zu der Wirkungsweise der verschiedenen Techniken in verschiedenen Umfeldern. In diesem Bericht beschreiben wir eine experimentelle Untersuchung, in der verschiedene, gängige Verfahren der Softwareprüfung auf zwei Arten von Artefakte -- Programmcode und ausführbare Spezifikationen -- im Bereich der eingebetteten Systeme angewandt wurden. Bei der Untersuchung konnten wir ein signifikant besseres Abschneiden statischer Prüfverfahren (Inspektionen) feststellen und auch die bereits von Myers publizierte Beobachtung disjunkter Fehlerklassen bestätigen.

PDF

Autoren: Gerhard Schellhorn

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 directed graphs. We present a structured algebraic specification of directed graphs with 165 axioms. 54 theorems are given, 46 of which can be proved without induction (some of them rely on the 8 inductive consequences). Test files are available in Otter syntax, as Setheo clauses and in the common syntax of the DFG-Schwerpunkt "Deduktion".

PDF

Autoren: Gerhard Schellhorn, Wolfgang Reif

The paper describes a large experiment in using automated theorem provers on first-order goals that showed up in a KIV case study on the verification of a Prolog compiler. Based on an algebraic specification with 456 axioms, 580 theorems were proven in KIV. For the theorems using induction, additional goals were generated for induction bases and steps, resulting in 733 noninductive goals. These were given to Otter, Setheo and Spass in several versions: with and without an axiom reduction preprocessing step, and with and without a precedence order generated from the specification structure. Test files are available in Otter syntax, as Setheo clauses and in the common syntax of the DFG-Schwerpunkt "Deduktion", which is used by Spass.

PDF

Autoren: Mohammad Ali Livani

The paper presents a mechanism called Shadow Retransmitter (SHARE) which ensures the reliable transmission of broadcast messages in a CAN bus. Due to its full transparency, SHARE can be added to existing application systems to provide high reliability. Keywords: Reliable Broadcast, Real-time communication, fault-tolerance, CAN.

PDF

Autoren: Mohammad Ali Livani, Jörg Kaiser

In this paper, we present a multicast protocol which guarantees atomic order in a CAN bus under anticipated fault conditions. The protocol exploits features of the underlying communication layers to maintain atomic multicast delivery with minimum additional overhead. Keywords: Real-time communication, fault-tolerance, atomic multicast, causal order, CAN.

PDF