Kaiserslautern - Fachbereich Informatik
Refine
Year of publication
Document Type
- Report (111) (remove)
Language
- English (111) (remove)
Has Fulltext
- yes (111)
Keywords
- Dienstgüte (3)
- Formalisierung (3)
- AG-RESY (1)
- Ad-hoc-Netz (1)
- Compiler (1)
- Coq (1)
- Extraction (1)
- Formal Semantics (1)
- Fräsen (1)
- Funknetz (1)
Faculty / Organisational entity
This paper introduces a new high Level programming language for a novel
class of computational devices namely data-procedural machines. These machines are by up to several orders of magnitude more efficient than the von Neumann paradigm of computers and are as flexible and as universal as computers. Their efficiency and flexibility is achieved by using field-programmable logic as the essential technology platform. The paper briefly summarizes and illustrates the essential new features of this language by means of two example programs.
The provision of quality-of-service (QoS) on the network layer is a major challenge in communication networks. This applies particularly to mobile ad-hoc networks (MANETs) in the area of Ambient Intelligence (AmI), especially with the increasing use of delay and bandwidth sensitive applications. The focus of this survey lies on the classification and analysis of selected QoS routing protocols in the domain of mobile ad-hoc networks. Each protocol is briefly described and assessed, and the results are summarized in multiple tables.
Guaranteeing correctness of compilation is a ma jor precondition for correct software. Code generation can be one of the most error-prone tasks in a compiler. One way to achieve trusted compilation is certifying compilation. A certifying compiler generates for each run a proof that it has performed the compilation run correctly. The proof is checked in a separate theorem prover. If the theorem prover is content with the proof, one can be sure that the compiler produced correct code. This paper presents a certifying code generation phase for a compiler translating an intermediate language into assembler code. The time spent for checking the proofs is the bottleneck of certifying compilation. We exhibit an improved framework for certifying compilation and considerable advances to overcome this bottleneck. We compare our implementation featuring the Coq theorem prover to an older implementation. Our current implementation is feasible for medium to large sized programs.
Abstraction is intensively used in the verification of large, complex or infinite-state systems. With abstractions getting more complex it is often difficult to see whether they are valid. However, for using abstraction in model checking it has to be ensured that properties are preserved. In this paper, we use a translation validation approach to verify property preservation of system abstractions. We formulate a correctness criterion based on simulation between concrete and abstract system for a property to be verified. For each distinct run of the abstraction procedure the correctness is verified in the theorem prover Isabelle/HOL. This technique is applied in the verification of embedded adaptive systems. This paper is an extended version a previously published work.
Many applications dealing with geometry acquisition and processing produce polygonal meshes that carry artifacts like discretization noise. While there are many approaches to remove the artifacts by smoothing or filtering the mesh, they are not tailored to any specific application subject to·certain restrictive objectives. We show how to incorporate smoothing schemes based on the general Laplacian approximation to satsify all those objectives at
the same time for the results of flow simulation in the application field of car manufacturing. In the presented application setting the major restrictions come from the bounding volume of the flow simulation, the so-called installation space. In particular, clean mesh regions (without noise) should not be smoothed while at the same time the installation space must not be violated by the smoothing of the noisy mesh regions. Additionally, aliasing effects at the boundary between clean and noisy mesh regions must be prevented. To address the fact that the meshes come from flow simulation, the presented method is versatile enough to preserve their exact volume and to apply anisotropic filters using the flow information.
Although the paper focuses on the results of a specific application, most of its findings can be transferred to different settings as well.
The quality of freeform surfaces is one of the major topics of CAD/CAM. Aesthetic and technical demands require the construction of high quality surfaces with strong shape conditions. Quality diminishing properties like dents or flat points have to be eliminated while approximation conditions must hold at the same time. Our approach combines quality and approximation criteria to a nonlinear multicriteria optimization problem and achieves an automatic approximation and fitting process.
This report gives an overview of the separate translation of synchronous imperative programs to synchronous guarded actions. In particular, we consider problems to be solved for separate compilation that stem from preemption statements and local variable declarations. We explain how we solved these problems and sketch our solutions implemented in the our Averest framework to implement a compiler that allows a separate compilation of imperative synchronous programs with local variables and unrestricted preemption statements. The focus of the report is the big picture of our entire design flow.
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.
We introduce the concept of streamballs for fluid flow visualization. Streamballs are based upon implicit surface generation techniques adopted from the well-known metaballs. Their property to split or merge automatically in areas of significant divergence or convergence makes them an ideal tool for the visualization of arbitrary complex flow fields. Using convolution surfaces generated by continuous skeletons for streamball construction offers the possibility to visualize even tensor fields.
Optimal degree reductions, i.e. best approximations of \(n\)-th degree Bezier curves
by Bezier curves of degree \(n\) - 1, with respect to different norms are studied. It
is shown that for any \(L_p\)-norm the euclidean degree reduction where the norm is applied to the euclidean distance function of two curves is identical to componentwise degree reduction. The Bezier points of the degree reductions are found to lie on parallel lines through the Bezier points of any Taylor expansion of degree \(n\) - 1 of the original curve. This geometric situation is shown to hold also in the case of constrained degree reduction. The Bezier points of the degree reduction are explicitly given in the unconstrained case for \(p\) = 1 and \(p\) = 2 and in the constrained case for \(p\) = 2.
The problem to interpolate Hermite-type data (i.e. two points with attached tangent vectors) with elastic curves of prescribed tension is known to have multiple solutions. A method is presented that finds all solutions of length not exceeding one period of its curvature function. The algorithm is based on algebraic relations between discrete curvature information which allow to transform the problem into a univariate one. The method operates with curves that by construction partially interpolate the given data. Hereby the objective function of the problem is drastically simplified. A bound on the maximum curvature value is established that provides an interval containing all solutions.
Experience gathered from applying the software process modeling language MVP-L in software development organizations has shown the need for graphical representations of process models. Project members (i.e„ non MVP-L specialists) review models much more easily by using graphical representations. Although several various graphical notations were developed for individual projects in which MVP-L was applied, there was previously no consistent definition of a mapping between textual MVP-L models and graphical representations. This report defines a graphical representation schema for MVP-L
descriptions and combines previous results in a unified form. A basic set of building blocks (i.e., graphical symbols and text fragments) is defined, but because we must first gain experience with the new symbols, only rudimentary guidelines are given for composing basic
symbols into a graphical representation of a model.
Intellectual control over software development projects requires the existence of an integrated set of explicit models of the products to be developed, the processes used to develop them, the resources needed, and the productivity and quality aspects involved. In recent years the development of languages, methods and tools for modeling software processes, analyzing and enacting them has become a major emphasis of software engineering research. The majority of current process research concentrates on prescriptive modeling of small, completely formalizable processes and their execution entirely on computers. This research direction has produced process modeling languages suitable for machine rather than human consumption. The MVP project, launched at the University of Maryland and continued at Universität Kaiserslautern, emphasizes building descriptive models of large, real-world processes and their use by humans and computers for the purpose of understanding, analyzing, guiding and improving software development projects. The language MVP-L has been developed with these purposes in mind. In this paper, we
motivate the need for MVP-L, introduce the prototype language, and demonstrate its uses. We assume that further improvements to our language will be triggered by lessons learned from applications and experiments.
The provision of network Quality-of-Service (network QoS) in wireless (ad-hoc) networks is a major challenge in the development of future communication systems. Before designing and implementing these systems, the network QoS requirements are to be specified. Existing approaches to the specification of network QoS requirements are mainly focused on specific domains or individual system layers. In this paper, we present a holistic, comprehensive formalization of network QoS requirements, across layers. QoS requirements are specified on each layer by defining QoS domain, consisting of QoS performance, reliability, and guarantee, and QoS scalability, with utility and cost functions. Furthermore, we derive preorders on multi-dimensional QoS domains, and present criteria to reduce these domains, leading to a manageable subset of QoS values that is sufficient for system design and implementation. We illustrate our approach by examples from the case study Wireless Video Transmission.
The provision of network Quality-of-Service (network QoS) in wireless (ad-hoc) networks is a major challenge in the development of future communication systems. Before designing and implementing these systems, the network QoS requirements are to be specified. Since QoS functionalities are integrated across layers and hence QoS specifications exist on different system layers, a QoS mapping technique is needed to translate the specifications into each other. In this paper, we formalize the relationship between layers. Based on a comprehensive and holistic formalization of network QoS requirements, we define two kinds of QoS mappings. QoS domain mappings associate QoS domains of two abstraction levels. QoS scalability mappings associate utility and cost functions of two abstraction levels. We illustrate our approach by examples from the case study Wireless Video Transmission.
User interfaces for large distributed applications have to handle specific problems: the complexity of the application itself and the integration of online-data into the user interface. A main task of the user interface architecture is to provide powerful tools to design and augment the end-user system easily, hence giving the designer more time to focus on user requirements. Our experiences developing a user interface system for a process control room showed that a lot of time during the development process is wasted for the integration of online-data residing anywhere but not in the user interface itself. Furtheron external data may be kept by different kinds of programs, e.g. C-programs running
a numerical process model or PROLOG-programs running a diagnosis system, both in parallel to the process and in parallel to the user interface. Facing these specific requirements, we developed a user interface architecture following two main goals: 1. integration of external information into high-level graphical objects and 2. the system should be open for any program running as a separate process using its own problem-oriented language. The architecture is based on two approaches: an asynchronous, distributed and language independent communication model and an object model describing the problem domain and the interface using object-oriented techniques. Other areas like rule-based programming are involved, too. With this paper, we will present the XAVIA user interface architecture, the (as far as we know) first user inteface architecture, which is consequently based on a distributed object model.
This document offers a concise introduction to the Goal Question Metric Paradigm (GQM Paradigm), and surveys research on applying and extending the GQM Paradigm. We describe the GQM Paradigm in terms of its basic principles, techniques for structuring GQM-related documents, and methods for performing tasks of planning and implementing a measurement program based on GQM. We also survey prototype software tools that support applying the GQM Paradigm in various ways. An annotated bibliography lists sources that document experience gained while using the GQM Paradigm and offer in-depth information about the GQM Paradigm.
The World Wide Web is a medium through which a manufacturer may allow Internet visitors to customize or compose his products. Due to missing or rapidly changing standards these applications are often restricted to relatively simple CGI or JAVA based scripts. Usually, results like images or movies are stored in a database and are transferred on demand to the web-user. Viper (Visualisierung parametrisch editierbarer Raumkomponenten) is a Toolkit [VIP96] written in C++ and JAVA which provides 3D-modeling and visualization methodsfor developing complex web-based applications. The Toolkit has been designed to built a prototype, which can be used to construct and visualize prefabricated homes on the Internet. Alternative applications are outlined in this paper. Within Viper, all objects are stored in a scene graph (VSSG ), which is the basic data structure of the Toolkit. To show the concept and structure of the Toolkit, functionality, and implementation of the prototype are described.
Best-Fit Pattern Matching
(1994)
This report shows that dispatching of methods in object oriented languages is in principle the same as best fit pattern matching. A general conceptual description of best fit pattern matching is presented. Many object oriented features are modelled by means of the general concept. This shows that simple methods, multi methods, overloading of functions, pattern matching,
dynamic and union types, and extendable records can be combined in a single comprehensive concept.
Gauss Frame Offsets
(1992)
Objective: In some surgical specialties, e.g. orthopedics, robots are already used in the operating room for bony milling work. Oto- and otoneurosurgery may also greatly benefit by robotic enhanced precision. Study Design: Experimental study on robotic milling on oak wood and human temporal bone specimen. Methods: A standard industrial robot with a 6 degrees-of-freedom serial kinematics was used with force feedback to proportionally control the robot speed. Different milling modes and characteristic path parameters were evaluated to generate milling paths based on CAD geometry data of a cochlear implant and an implantable hearing system. Results: The best suited strategy proofed to be the spiral horizontal milling mode with the burr held perpendicularly to the temporal bone surface. In order to avoid high grooves, the distance in between paths should equal half the radius of the cutting burr head. Due to the vibration of the robot’s own motors, a rather high oscillation of the standard deviation of forces was encountered. This oscillation dropped drastically to nearly 0 N, when the burr head reached contact with the dura mater due to its damping characteristics. The cutting burr could be moved a long time on the dura without damaging it, because of its rather blunt head. The robot moved the burr very smoothly according to the encountered resistances. Conclusion: This is the first development of an functioning robotic milling procedure for otoneurosurgery with force-based speed control. It is planned to implement ultrasound-based local navigation and to perform robotic mastoidectomy.
The Chained Lin-Kernighan algorithm (CLK) is one of the best heuristics to solve Traveling Salesman Problems (TSP). In this paper a distributed algorithm is proposed, were nodes in a network locally optimize TSP instances by using the CLK algorithm. Within an Evolutionary Algorithm (EA) network-based framework the resulting tours are modified and exchanged with neighboring nodes. We show that the distributed variant finds better tours compared to the original CLK given the same amount of computation time. For instance fl3795, the original CLK got stuck in local optima in each of 10 runs, whereas the distributed algorithm found optimal tours in each run requiring less than 10 CPU minutes per node on average in an 8 node setup. For instance sw24978, the distributed algorithm had an average solution quality of 0.050% above the optimum, compared to CLK's average solution of 0.119% above the optimum given the same total CPU time (104 seconds). Considering the best tours of both variants for this instance, the distributed algorithm is 0.033% above the optimum and the CLK algorithm 0.099%.
The local solution problem of multivariate Fredholm integral equations is studied. Recent research proved that for several function classes the complexity of this problem is closely related to the Gelfand numbers of some characterizing operators. The generalization of this approach to the situation of arbitrary Banach spaces is the subject of the present paper.
Furthermore, an iterative algorithm is described which - under some additional conditions - realizes the optimal error rate. The way these general theorems work is demonstrated by applying them to integral equations in a Sobolev space of periodic functions with dominating mixed derivative of various order.
In this paper the complexity of the local solution of Fredholm integral equations
is studied. For certain Sobolev classes of multivariate periodic functions with dominating mixed derivative we prove matching lower and upper bounds. The lower bound is shown using relations to s-numbers. The upper bound is proved in a constructive way providing an implementable algorithm of optimal order based on Fourier coefficients and a hyperbolic cross approximation.
We study the complexity of local solution of Fredholm integral equations. This means that we want to compute not the full solution, but rather a functional (weighted mean, value in a point) of it. For certain Sobolev classes of multivariate periodic functions we prove matching upper and lower bounds and construct an algorithm of the optimal order, based on Fourier coefficients and a hyperbolic cross approximation.
In recent years, Smolyak quadrature rules (also called hyperbolic cross points or sparse grids) have gained interest as a possible competitor to number theoretic quadratures for high dimensional problems. A standard way of comparing the quality of multivariate quadrature formulas
consists in computing their \(L_2\)-discrepancy. Especially for larger dimensions, such computations are a highly complex task. In this paper we develop a fast recursive algorithm for computing the \(L_2\)-discrepancy (and related quality measures) of general Smolyak quadratures. We carry out numerical comparisons between the discrepancies of certain Smolyak rules, Hammersley and Monte Carlo sequences.
A notion of discrepancy is introduced, which represents the integration error on spaces of \(r\)-smooth periodic functions. It generalizes the diaphony and constitutes a periodic counterpart to the classical \(L_2\)-discrepancy as weil as \(r\)-smooth versions of it introduced recently by Paskov [Pas93]. Based on previous work [FH96], we develop an efficient algorithm for computing periodic discrepancies for quadrature formulas possessing certain tensor product structures, in particular, for Smolyak quadrature rules (also called sparse grid methods). Furthermore, fast algorithms of computing periodic discrepancies for lattice rules can easily be derived from well-known properties of lattices. On this basis we carry out numerical comparisons of discrepancies between Smolyak and lattice rules.
In this paper, the complexity of full solution of Fredholm integral equations of the second kind with data from the Sobolev class \(W^r_2\) is studied. The exact order of information complexity is derived. The lower bound is proved using a Gelfand number technique. The upper bound is shown by providing a concrete algorithm of optimal order, based on a specific hyperbolic cross approximation of the kernel function. Numerical experiments are included, comparing the optimal algorithm with the standard Galerkin method.
We introduce two novel techniques for speeding up the generation of digital \((t,s)\)-sequences. Based on these results a new algorithm for the construction of Owen's randomly permuted \((t,s)\)-sequences is developed and analyzed. An implementation of the new techniques is available at http://www.cs.caltech.edu/~ilja/libseq/index.html
This report explains basic notions and concepts of Abstract State Machines (ASM) as well as notation for defining ASM models. The objective here is to provide an intuitive understanding of the formalism; for a rigorous definition of the mathematical foundations of ASM, the reader is referred to [2] and [3]. Further references on ASM-related material can be found on the ASM Web Pages [1].
Today, test methods for communication protocols assume, among other things, that the protocol design is specified as a single, monolithic finite state machine (FSM). From this specification, test suites that are capable of detecting output and/or transfer faults in the protocol implementation are derived. Limited applicability ofthese methods is mainly because oftheir specific assumptions, and due to the size of the derived test suite and the resulting test effort for realistic protocols. In this work, the compositional test method (C-method), which exploits the available structure of a communication protocol, is proposed. The C-method first tests each protocol component separately for output and/or transfer faults, using one of the traditional test methods, then checks for composability, and finally tests the composite system for composition faults. To check for composability and to derive the test suite for the detection of composition faults, it is not required to construct the global state machine. Instead, all information is derived from the component state machines, which avoids a potential state explosion and lengthy test cases. Furthermore, the test suite checks for composition faults only. This substantially reduces the size of the test suite and thus the overall test effort.
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.
With the UML 2.0 standard, the Unified Modeling Language took a big step towards SDL, incorporating many features of the language. SDL is a mature and complete language with formal semantics. The Z.109 standard defines a UML Profile for SDL, mapping UML constructs to corresponding counterparts in SDL, giving them a precise semantics. In this report, we present a case study for the formalisation of the Z.109 standard. The formal definition makes the mapping precise and can be used to derive tool support.
Over a period of 30 years, ITU-T’s Specification and Description Language (SDL) has matured to a sophisticated formal modelling language for distributed systems and communication protocols. The language definition of SDL-2000, the latest version of SDL, is complex and difficult to maintain. Full tool support for SDL is costly to implement. Therefore, only subsets of SDL are currently supported by tools. These SDL subsets - called SDL profiles - already cover a wide range of systems, and are often suffcient in practice. In this report, we present our approach for extracting the formal semantics for SDL profiles from the complete SDL semantics. We then formalise the approach, present our SDL-profile tool, and report on our experiences.
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.
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.
The CAD/CAM-based design of free-form surfaces is the beginning of a chain of operations, which ends with the numerically controlled (NC-) production of the designed object. During this process the shape control is an important step to amount efficiency. Several surface interrogation methods already exist to analyze curvature and continuity behaviour of the shape. This paper deals with a new aspect of shape control: the stability of surfaces with respect to infnitesimal bendings. Each inEnitesimal bending of a surface determines a so called instability surface, which is used for the stability investigations. The kinematic meaning of this instability surface will be discussed and we present algorithms to calculate it.
Hardware / Software Codesign
(1994)
We study summation of sequences and integration in the quantum model of computation. We develop quantum algorithms for computing the mean of sequences which satisfy a \(p\)-summability condition and for integration of functions from Lebesgue spaces \(L_p([0,1]^d)\) and analyze their convergence rates. We also prove lower bounds which show that the proposed algorithms are, in many cases, optimal within the setting of quantum computing. This extends recent results of Brassard, Høyer, Mosca, and Tapp (2000) on computing the mean for bounded sequences and complements results of Novak (2001) on integration of functions from Hölder classes.
We study high dimensional integration in the quantum model of computation. We develop quantum algorithms for integration of functions from Sobolev classes \(W^r_p [0,1]^d\) and analyze their convergence rates. We also prove lower bounds which show that the proposed algorithms are, in many cases, optimal within the setting of quantum computing. This extends recent results of Novak on integration of functions from Hölder classes.
The \(L_2\)-discrepancy is a quantitative measure of precision for multivariate quadrature rules. It can be computed explicitly. Previously known algorithms needed \(O(m^2\)) operations, where \(m\) is the number of nodes. In this paper we present algorithms which require
\(O(m(log m)^d)\) operations.
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.
Approximation properties of the underlying estimator are used to improve the efficiency of the method of dependent tests. A multilevel approximation procedure is developed such that in each level the number of samples is balanced with the level-dependent variance, resulting in a considerable reduction of the overall computational cost. The new technique is applied to the Monte Carlo estimation of integrals depending on a parameter.
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.
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.
Monte Carlo integration is often used for antialiasing in rendering processes.
Due to low sampling rates only expected error estimates can be stated, and the variance can be high. In this article quasi-Monte Carlo methods are presented, achieving a guaranteed upper error bound and a convergence rate essentially as fast as usual Monte Carlo.
The radiance equation, which describes the global illumination problem in computer graphics, is a high dimensional integral equation. Estimates of the solution are usually computed on the basis of Monte Carlo methods. In this paper we propose and investigate quasi-Monte Carlo methods, which means that we replace (pseudo-) random samples by low discrepancy sequences, yielding deterministic algorithms. We carry out a comparative numerical study between Monte Carlo and quasi-Monte Carlo methods. Our results show that quasi-Monte Carlo converges considerably faster.