## Interner Bericht des Fachbereich Informatik

### Filtern

#### Erscheinungsjahr

#### Dokumenttyp

- Bericht (108)
- Preprint (4)
- Konferenzveröffentlichung (2)

#### Sprache

- Englisch (114) (entfernen)

#### Schlagworte

- Dienstgüte (2)
- Formalisierung (2)
- Certifying Compilers (1)
- Compiler (1)
- Coq (1)
- Extraction (1)
- Formal Semantics (1)
- Formalisierung (1)
- HOL (1)
- Hub-and-Spoke-System (1)

- 299
- Wavelet Monte Carlo Methods for the Global Solution of Integral Equations (1999)
- We study the global solution of Fredholm integral equations of the second kind by the help of Monte Carlo methods. Global solution means that we seek to approximate the full solution function. This is opposed to the usual applications of Monte Carlo, were one only wants to approximate a functional of the solution. In recent years several researchers developed Monte Carlo methods also for the global problem. In this paper we present a new Monte Carlo algorithm for the global solution of integral equations. We use multiwavelet expansions to approximate the solution. We study the behaviour of variance on increasing levels, and based on this, develop a new variance reduction technique. For classes of smooth kernels and right hand sides we determine the convergence rate of this algorithm and show that it is higher than those of previously developed algorithms for the global problem. Moreover, an information-based complexity analysis shows that our algorithm is optimal among all stochastic algorithms of the same computational cost and that no deterministic algorithm of the same cost can reach its convergence rate.

- 269
- Visualization of Unstable Surface Regions (1995)
- Computer processing of free form surfaces forms the basis of a closed construction process starting with surface design and up to NC-production. Numerical simulation and visualization allow quality analysis before manufacture. A new aspect in surface analysis is described, the stability of surfaces versus infinitesimal bendings. The stability concept is derived from the kinetic meaning of a special vector field which is given by the deformation. Algorithms to calculate this vector field together with an appropriate visualization method give a tool able to analyze surface stability.

- 275
- Variance reduction for Monte Carlo methods by means of deterministic numerical computation (1995)
- A new variance reduction technique for the Monte Carlo solution of integral equations is introduced. It is based on separation of the main part. A neighboring equation with exactly known solution is constructed by the help of a deterministic Galerkin scheme. The variance of the method is analyzed, and an application to the radiosity equation of computer graphics, together with numerical test results is given.

- 285
- Variance reduction by means of deterministic computation (1996)
- We study the collision estimate of Monte Carlo methods for the solution of integral equations. A new variance technique is proposed and analyzed. It consists in the separation of the main part by constructing a neighboring equation based on deterministic numerical methods.

- 304
- Using Transport Services instead of specific Transport Protocols (2000)
- For most applications the used transport service providers are predetermined during the development of the application. This makes it difficult to consider the application communication requirements and to exploit specific features of the network technology. Specialized protocols that are more efficient and offer a qualitative improved service are typically not supported by most applications because they are not commonly available. In this paper we propose a concept for the realization of protocol independent transport services. Only a transport service is predetermined during the development of the application and an appropriate transport service provider is dynamically selected at run time. This enables to exploit specialized protocols if possible, but standard protocols could still be used if necessary. The main focus of this paper is how a transport service could provide a new transport service provider transparently to existing applications. A prototype is presented that maps TCP/IP based applications to an ATM specific transport service provider which offers a reliable and unreliable transport service like TCP/IP.

- 387
- Translating SHIM to Guarded Actions (2012)
- SHIM is a concurrent deterministic programming language for embedded systems built on rendezvous communication. It abstracts away many details to give the developer a high-level view that includes virtual shared variables, threads as orthogonal statements, and deterministic concurrent exceptions. In this paper, we present a new way to compile a SHIM-like language into a set of asynchronous guarded actions, a well-established intermediate representation for concurrent systems. By doing so, we build a bridge to many other tools, including hardware synthesis and formal verification. We present our translation in detail, illustrate it through examples, and show how the result can be used by various other tools.

- 316
- Trajectory Splitting by Restricted Replication (2001)
- New algorithms for efficient trajectory splitting are presented. By derandomizing these techniques that are derived from randomized quasi-Monte Carlo integration, trajectory splitting for the quasi-Monte Carlo method becomes available.

- 327
- Towards the Harmonisation of UML and SDL (2003)
- UML and SDL are languages for the development of software systems that have different origins, and have evolved separately for many years. Recently, it can be observed that OMG and ITU, the standardisation bodies responsible for UML and SDL, respectively, are making efforts to harmonise these languages. So far, harmonisation takes place mainly on a conceptual level, by extending and aligning the set of language concepts. In this paper, we argue that harmonisation of languages can be approached both from a syntactic and semantic perspective. We show how a common syntactical basis can be derived from the analysis of the UML meta-model and the SDL abstract grammar. For this purpose, conceptually sound and well-founded mappings from meta-models to abstract grammars and vice versa are defined and applied. On the semantic level, a comparison between corresponding language constructs is performed.

- 247
- Towards a Basic Reference Model of Open Distributed Processing (1994)
- The Basic Reference Model of ODP introduces a number of basic concepts in order to provide a common basis for the development of a coherent set of standards. To achieve this objective, a clear understanding of the basic concepts is one prerequisite. This paper makes an effort at clarifying some of the basic concepts independently of standardized or non-standardized formal description techniques. Among the basic concepts considered here are: agent, action, interaction, interaction point, architecture, behaviour, system, composition, refinement, and abstraction. In a case study, it is then shown how these basic concepts can be represented in a formal specification written in temporal logic.

- 364
- Theorem Proving in Higher Order Logics - Emerging Trends (2007)
- This technical report is the Emerging Trends proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2007), which was held during 10-13 September in Kaiserslautern, Germany. TPHOLs covers all aspects of theorem proving in higher order logics as well as related topics in theorem proving and veriﬁcation.