Kaiserslautern - Fachbereich Informatik
Refine
Year of publication
- 1997 (8) (remove)
Document Type
- Report (8) (remove)
Has Fulltext
- yes (8)
Faculty / Organisational entity
Estelle is an internationally standardized formal description technique (FDT) designed for the specification of distributed systems, in particular communication protocols. An Estelle specification describes a system of communicating components (module instances). The specified system is closed in a topological sense, i.e. it has no ability to interact with some environment. Because of this restriction, open systems can only be specified together with and incorporated with an environment. To overcome this restriction, we introduce a compatible extension of Estelle, called "Open Estelle". It allows the specification of (topologically) open systems, i.e. systems that have the ability to communicate with any environment through a well-defined external interface. We define aformal syntax and a formal semantics for Open Estelle, both based on and extending the syntax and semantics of Estelle. The extension is compatible syntactically and semantically, i.e. Estelle is a subset of Open Estelle. In particular, the formal semantics of Open Estelle reduces to the Estelle semantics in the special case of a closed system. Furthermore, we present a tool for the textual integration of open systems into environments specified in Open Estelle, and a compiler for the automatic generation of implementations directly from Open Estelle specifications.
Formale Beschreibungstechniken (FDTs) erlauben durch ihre formale Syntax und Semantik eine präzise Systembeschreibung und sind Grundlage für die formale Verifikation. Bei der Implementierung von Systemen wird jedoch nach wie vor von Hand implementiert, selbst wenn ausgereifte Werkzeuge zur automatischen Generierung von Kode direkt aus der formalen Spezifikation existieren. Die Ursache dafür liegt in dem Ruf dieser Werkzeuge, Kode mit extrem geringer Leistungsfähigkeit zu erzeugen. Es gibt jedoch kaum quantitative Leistungsvergleiche zwischen manuell und automatisch generierten Implementierungen, die dieses Vorurteil stützen oder widerlegen könnten. In diesem Beitrag wird ein solcher Leistungsvergleich anhand des Hochleistungsprotokolls XTP und der FDT Estelle vorgestellt. Er liefert eine Bestandsaufnahme des momentanen Entwicklungsstandes bei der automatischen Generierung von Kode aus Estelle-Spezifikationen im direkten Vergleich zu gut optimierten Handimplementierungen. Es zeigt sich, daß in dem betrachteten Fall eines komplexen Protokolls die Handimplementierung zwar merklich leistungsstärker ist. Dieser Leistungsvorteil wird jedoch durch einen sehr hohen Implementierungsaufwand sowie die Schwierigkeit, die Korrektheit bzgl. der Spezifikation sicherzustellen, erkauft. Im einzelnen Anwendungsfall kann es daher trotz der Leistungseinbußen durchaus vorteilhaft sein, automatisch Kode zu erzeugen, zumal in der Bestandsaufnahme festgestellt wurde, daß automatisch generierte Implementierungen z.T. besser abschneiden als erwartet. Zudem besteht - anders als bei der bereits umfassend optimierten Handimplementierung - noch ein erhebliches ungenutztes Potential zur Leistungsverbesserung der automatisch generierten Implementierung.
In dieser Arbeit wird eine Integration der temporallogischen Verarbeitungskonzepte
der Programmiersprache ExTeLL in die objektorientierte Wirtssprache \(C^{++}\) vorgestellt. Dabei war unser Ziel eine Schnittstelle zur komfortablen Kommunikation der Sprachkomponenten zu entwickeln, derart daß die Sprachsynthese eine homogene Gesamtsprache darstellt . Hierbei haben wir besonderen Wert auf die Nutzung der Möglichkeiten der jeweils hinzugefügten Sprachkomponente und einen syntaktisch einheitlichen Aufbau der Gesamtsprache gelegt. Dies erforderte insbesondere die Integration des Typkonzepts von \(C^{++}\) sowie der Mechanismen zur Überladung von Funktionen und Prozeduren in ExTeLL und in der zugrundeliegenden Temporallogik
EITeL.
We study the problem of global solution of Fredholm integral equations. This means that we seek to approximate the full solution function (as opposed to the local problem, where only the value of the solution in a single point or a functional of the solution is sought). We analyze the Monte Carlo complexity, i.e. the complexity of stochastic solution of this problem. The framework for this analysis is provided by information based complexity theory. Our investigations complement previous ones on stochastic complexity of local solution and on deterministic complexity of
both local and global solution. The results show that even in the global case Monte Carlo algorithms can perform better than deterministic ones, although the difference is not as large as in the local case.
The intuitionistic calculus mj for sequents, in which no other logical symbols than those for implication and universal quantification occur, is introduced and analysed. It allows a simple backward application, called mj-reduction here, for searching for derivation trees. Terms needed in mj-reduction can be found with the unification algorithm. mj-Reduction with unification can be seen as a natural extension of SLD-resolution. mj-Derivability of the sequents considered here coincides with derivability in Johansson's minimal intuitionistic calculus LHM in [6]. Intuitionistic derivability of formulae with negation and classical derivability of formulae with all usual logical symbols can be expressed with mj-derivability and hence be verified by mj-reduction. mj-Derivations can be easily translated into LJ-derivations without
"Schnitt", or into NJ-derivations in a slightly sharpened form of Prawitz' normal form. In the first three sections, the systematic use of mj-reduction for proving in predicate logic is emphasized. Although the fourth section, the last and largest, is exclusively devoted to the mathematical analysis of the calculus mj, the first three sections may be of interest to a wider readership, including readers looking for applications of symbolic logic. Unfortunately, the mathematical analysis of the calculus mj, as the study of Gentzen's calculi, demands a large amount of technical work that obscures the natural unfolding of the argumentation. To alleviate this, definitions and theorems are completely embedded in the text to provide a fluent and balanced mathematical discourse: new concepts are indicated with bold-face, proofs of assertions are outlined, or omitted when it is assumed that the reader can provide them.
The problem of constructing a geometric model of an existing object from a set of boundary points arises in many areas of industry. In this paper we present a new solution to this problem which is an extension of Boissonnat's method [2]. Our approach uses the well known Delaunay triangulation of the data points as an intermediate step. Starting with this structure, we eliminate tetrahedra until we get an appropriate approximation of the desired shape. The method proposed in this paper is capable of reconstructing objects with arbitrary genus and can cope with different point densities in different regions of the object. The
problems which arise during the elimination process, i.e. which tetrahedra can be eliminated, which order has to be used to control the process and finally, how to stop the elimination procedure at the right time, are discussed in detail. Several examples are given to show the validity of the method.
Instant Radiosity
(1997)
We present a fundamental procedure for instant rendering from the radiance equation. Operating directly on the textured scene description, the very efficient and simple algorithm produces photorealistic images without any kernel or solution discretization of the underlying integral equation. Rendering rates of a few seconds are obtained by exploiting graphics hardware, the deterministic
technique of the quasi-random walk for the solution of the global illumination problem, and the new method of jittered low discrepancy sampling.