Autoren: Ercüment Canver, Jan-Tecker Gayen, Adam Moik

Die computergesteuerte ''elektrisch ortsbediente Weiche (EOW)'' ist ein Produkt aus dem Bereich des spurgeführten Verkehrs und wird in Gleisanlagen eingesetzt, die mit nur geringer Geschwindigkeit befahren werden dürfen. Für einen sicheren und ordnungsgemäßen Betrieb werden dennoch hohe Anforderungen an die Steuerungssoftware der EOW gestellt. Die EOW ist als Industrieprodukt von hoher praktischer Relevanz. Da die Größe der Steuerungssoftware in einem handhabbaren Rahmen liegt, bietet sich mit dieser Anwendung eine geeignete Fallstudie zur Erprobung der in dem System ``Verification Support Environment (VSE)'' bereitgestellten formalen Methoden, einem Werkzeug zur formalen Spezifikation und Verifikation von sicherheitsrelevanten Softwaresystemen. Die Fallstudie wurde von einer interdisziplinären Arbeitsgruppe bearbeitet und es wurde versucht, das an\-wen\-dungs\-orientierte Vorgehen eines Ingenieurs und die methodik\-orien\-tier\-te formale Vorgehensweise eines Soft\-ware\-ent\-wicklers miteinander zu verknüpfen. Vorliegender Bericht wendet sich insbesondere an diese beiden Lesergruppen. Zunächst werden die EOW und die Anforderungen an die Steuerungssoftware beschrieben und der mit VSE zu modellierende Softwareausschnitt definiert. Die Abgrenzung und Schnittstellen dieses Ausschnitts zum Gesamtsystem werden festgelegt. Danach ist an diesem Ausschnitt die VSE-Methodik illustriert. Abschließend sind die Erfahrungen und Schlußfolgerungen aus dieser Fallstudie zusammengefaßt.

PDF

Autoren: Bernhard Nebel

While the worst-case computational properties of Allen's calculus for qualitative temporal reasoning have been analyzed quite extensively, the determination of the empirical efficiency of algorithms for solving the consistency problem in this calculus has received only little research attention. In this paper, we will demonstrate that using the ORD-Horn class in Ladkin and Reinefeld's backtracking algorithm leads to performance improvements when deciding consistency of hard instances in Allen's calculus. For this purpose, we prove that Ladkin and Reinefeld's algorithm is complete when using the ORD-Horn class, we identify phase transition regions of the reasoning problem, and compare the improvements of ORD-Horn with other heuristic methods when applied to instances in the phase transition region. Finally, we give evidence that combining search methods orthogonally can dramatically improve the performance of the backtracking algorithm.

PDF

Autoren: Ton Vullinghs, Wolfram Schulte, Thilo Schwinn

This report is an introduction to TkGofer. TkGofer is a library of functions for writing graphical user interfaces (GUIs) in the pure functional programming language Gofer. The library provides a convenient, abstract and high-level way to write window-oriented applications. The implementation rests on modern concepts like monads and constructor classes.The main goal of this report is to illustrate the way in which you write GUIs in TkGofer. All the provided widgets are introduced and explained by a set of illustrating examples. The last part of the manual lists the signatures of the user functions of the GUI library.

PDF

Autoren: Thomas Beuter, Peter Dadam

Workflow--Management--Systeme (WFMS) erobern sich neue Anwendungsgebiete mit jeweils spezifischen Anforderungen an die Leistungsfähigkeit dieser Systeme. Neben den Anforderungsprofilen an WFMS aus verschiedenen Anwendungsgebieten werden hier besonders die Anforderungen aus dem Bereich des Concurrent--Engineerings aufgezeigt. Die jeweiligen anwendungsspezifischen Anforderungen führen nicht nur zu einer großen Zahl unterschiedlich mächtigerModellierungskomponenten, sondern auch zu verschiedenen Alternativen für mögliche Laufzeitumgebungen der WFMS. Der Bericht zeigt die Probleme auf, die sich daraus für WFMS--Anwender und --Entwickler ergeben, und leitet praxisrelevante Fragestellungen ab, die aus wissenschaftlicher Sicht zu bearbeiten sind.

PDF

Autoren: Gerhard Schellhorn, Wolfgang Ahrendt

This paper describes the first steps of the formal verification of a Prolog compiler with the KIV system. We build upon the mathematical definitions given by B\örger and Rosenzweig. There an operational semantics of Prolog is defined using the formalism of Evolving Algebras, and then transformed in several systematic steps to the Warren Abstract Machine (WAM). To verify these transformation steps formally in KIV, a translation of deterministic Evolving Algebras to Dynamic Logic is defined, which may also be of general interest. With this translation, correctness of transformation steps becomes a problem of program equivalence in Dynamic Logic. We define a proof technique for verifying such problems, which corresponds to the use of proof maps in Evolving Algebras. Although the transformation steps are small enough for a mathematical analysis, this is not sufficient for a successful formal correctness proof. Such a proof requires to explicitly state a lot of facts, which were only implicitly assumed in the analysis. We will argue that these assumptions cannot be guessed in a first proof attempt, but have to be filled in incrementally. We report on our experience with this `evolutionary' verification process for the first transformation step, and the support KIV offers to do such incremental correctness proofs.

Autoren: Manindra Agrawal, Thomas Thierauf

PDF

Autoren: Vikraman Arvind, Jacobo Toran

In this paper we design a nonadaptive NC checker for permutation group intersection, sharpening a result from Blum and Kannan. This is a consequence of two results. First we show that a nontrivial permutation in the intersection of two given permutation groups (described by lists of generators) can be computed by an NC algorithm with one round of parallel queries to the Group Intersection problem. Next we design a two-round interactive proof system for the complement of the Group Intersection problem, for which the honest prover can be simulated by an NC algorithm with one round of parallel queries to Group Intersection. As a consequence we also have nonadaptive NC checkers for some related group-theoretic problems. On the technical side, we define a generalization of wreath products of permutation groups. This product plays a crucial role in the design of the nonadaptive checkers.

PDF

Autoren: David Cyrluk, Oliver Möller, Harald Rueß

The theory of fix-sized bitvectors with composition and extraction has been shown to be useful in the realm of hardware verification. In this paper we develop an efficient algorithm for deciding this theory. A proper input is an unquantified bitvector equation, say t = u, and our algorithm returns true if t = u is valid in the bitvector theory, false if t = u is unsatisfiable, and a system of solved equations otherwise. The worst-case time complexity of this solver is O(|t| + n^2), where |t| is the length of the bitvector term t and n denotes the number of bits on either side of the equation. Moreover, the resulting procedure can readily be integrated into Shostak's procedure for deciding combinations of theories.

PDF

Autoren: Bernd Biechele, Dietmar Ernst, Frank Houdek, Joachim Schmid, Wolfram Schulte

Die strukturierte Analyse (SA) definiert eine systematische Vorgehensweise zur Erstellung verständlicher Analysemodelle. In dieser Arbeit vergleichen wir für das Umfeld eingebetteter Systeme zwei SA-Ausprägungen. Um einen praxisrelevanten Vergleich zu ermöglichen, wurde eine realistische Fallstudie herangezogen und aktuelle Werkzeuge, die die betrachteten SA-Ausprägungen unterstützen, mit betrachtet. Diese Arbeit präsentiert einige Ergebnisse einer Studie, die im Rahmen des Softwarelabor Ulm für die Daimler-Benz AG angefertigt wurde. Die vergleichende Betrachtung ergab, daß die Anwendung formaler Methoden und insbesondere eine frühzeitige Simulation sich positiv auf Verständnis und Korrektheit auswirken.

PDF

Autoren: Falk Bartels, Axel Dold, Friedrich W. von Henke, Holger Pfeifer, Harald Rueß

PDF

Autoren: Axel Dold, Friedrich W. von Henke, Holger Pfeifer, Harald Rueß

PDF

Autoren: Axel Dold, Friedrich W. von Henke, Holger Pfeifer, Harald Rueß

PDF

Autoren: Klaus Achatz, Helmuth Partsch

PDF