Publikationen

Browse

Browsing Publikationen by Serial Ulm "Ulmer Informatik-Berichte"

Now showing 1 - 20 of 207
  • Thumbnail Image
    Item
  • Thumbnail Image
    Item
    19th Workshop on (Constraint) Logic Programming W(C)LP 2005
    (Universität Ulm)
    This volume contains the refereed and accepted papers and system descriptions presented at the 19th Workshop on (Constraint) Logic Programming W(C)LP 2005 held in Ulm, Germany, from February 21 to 23, 2005.
  • Thumbnail Image
    Item
    2. Krypto-Tag - Workshop über Kryptographie
    (Universität Ulm)
    N/A
  • Thumbnail Image
    Item
    3-D visual object classification with hierarchical radial basis function networks
    (Universität Ulm) Palm, Günther; Kestler, Hans A.; Schwenker, Friedhelm
    In this chapter we present a 3-D visual object recognition system for an autonomous mobile robot. This object recognition system performs the following three tasks: object localization in the camera images, feature extraction, and classification of the extracted feature vectors with hierarchical radial basis function (RBF) networks.
  • Thumbnail Image
    Item
    A classification of multi-database languages
    (Universität Ulm) Tresch, Markus; Scholl, Marc H.
    N/A
  • Thumbnail Image
    Item
    A comparison of multimedia document models concerning advanced requirements
    (Universität Ulm) Boll, Susanne; Klas, Wolfgang; Westermann, Utz
    N/A
  • Thumbnail Image
    Item
    A complete and terminating execution model for Constraint Handling Rules
    (Universität Ulm) Raiser, Frank; Betz, Hariolf; Frühwirth, Thom
    We observe that the various formulations of the operational semantics of Constraint Handling Rules proposed over the years fall into a spectrum ranging from the analytical to the pragmatic. While existing analytical formulations facilitate program analysis and formal proofs of program properties, they cannot be implemented as is. We propose a novel operational semantics, which has a strong analytical foundation, while featuring a terminating execution model. We prove its soundness and completeness with respect to existing analytical formulations and we compare its expressivity to that of various other formulations.
  • Thumbnail Image
    Item
    A conceptual approach to an open hospital information system
    (Universität Ulm) Kuhn, Klaus; Reichert, Manfred; Nathe, Michael; Beuter, Thomas; Heinlein, Christian; Dadam, Peter
    N/A
  • Thumbnail Image
    Item
  • Thumbnail Image
    Item
    A formal framework for data-aware process interaction models
    (Universität Ulm) Knuplesch, David; Pryss, Rüdiger; Reichert, Manfred
    IT support for distributed and collaborative workflows as well as related interactions between business partners are becoming increasingly important. For modeling such partner interactions as flow of message exchanges, different topdown approaches, covered under the term interaction modeling, are provided. Like for workflow models, correctness constitutes a fundamental challenge for interaction models, e.g., to ensure the boundedness and absence of deadlocks and lifelocks. Due to their distributed execution, in addition, interaction models should be message-deterministic and realizable, i.e., the same conversation (i.e. sequence of messages) should always lead to the same result, and it should be ensured that partners always have enough information about the messages they must or may send in a given context. So far, most existing approaches have addressed correctness of interaction models without explicitly considering the data exchanged through messages and used for routing decisions. However, data support is crucial for collaborative workflows and interaction models respectively. This technical report enriches interaction models with the data perspective. In particular, it defines the behavior of data-aware interaction models based on Data-Aware Interaction Nets, which use elements of both Interaction Petri Nets and Workflow Nets with Data. Finally, formal correctness criteria for Data-Aware Interaction Nets are derived, guaranteeing the boundedness and absence of deadlocks and lifelocks, and ensuring message-determinism as well as realizability.
  • Thumbnail Image
    Item
    A formal framework for workflow type and instance changes under correctness constraints
    (Universität Ulm) Rinderle, Stefanie; Reichert, Manfred; Dadam, Peter
    The capability to rapidly adapt in-progress workflows (WF) is an essential requirement for any workflow system. Adaptations may concern single WF instances or a WF type as a whole. While changes of single instances often have to be applied in an ad-hoc manner, type changes become necessary to adapt to evolving business processes. Especially for long-running processes it is indispensable to propagate type changes to running instances as well. Very challenging in this context is to correctly adapt a (potentially large) collection of WF instances, which may be in different states and to which various ad-hoc changes may have been previously applied. This paper presents a comprehensive framework for the support of both, WF type and WF instance changes. We establish general correctness principles and show how WF instances can be automatically and efficiently migrated to a modified WF schema. We point out that our approach exceeds existing adaptation models in formal foundation, completeness, and usability.
  • Thumbnail Image
    Item
    A formal semantics of time patterns for process-aware information systems
    (Universität Ulm) Lanz, Andreas; Reichert, Manfred; Weber, Barbara
    Companies increasingly adopt process-aware information systems (PAISs) to coordinate, monitor and evolve their business processes. Although the proper handling of temporal constraints (e.g. deadlines and minimum time lags between activities) is crucial in many application domains, existing PAISs vary significantly regarding their support of the temporal perspective of business processes. Both the formal specification and operational support of temporal constraints constitute fundamental challenges in this context. In previous work, we introduced time patterns facilitating the comparison of PAISs in respect to their support of the temporal perspective and provided empirical evidence for them. To avoid ambiguities and to ease the use as well as implementation of the time patterns, this paper formally defines their semantics. To enable pattern use in a wide range of process modeling languages and pattern integration with existing PAISs, this semantics is expressed independent of a particular process meta model. Altogether, the presented pattern formalization will foster the integration of the temporal perspective in PAISs.
  • Thumbnail Image
    Item
    A generic specification for verifying peephole optimizations
    (Universität Ulm) Dold, Axel; Henke, Friedrich Wilhelm von; Pfeifer, Holger; Rueß, Harald
    N/A
  • Thumbnail Image
    Item
    A guided tour through TYPELAB*
    (Universität Ulm) Luther, Marko; Strecker, Martin
    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.
  • Thumbnail Image
    Item
    A mechanically verified compiling specification for a realistic compiler
    (Universität Ulm) Dold, Axel; Henke, Friedrich Wilhelm von; Vialard, Vincent; Goerigk, Wolfgang
    We report on a large verification effort in constructing an initial fully trusted bootstrap compiler executable for a realistic system programming language and real target processor. The construction and verification process comprises three tasks: the verification of the compiling specification (a relation between abstract source and target programs) with respect to the language semantics and a realistic correctness criterion. Second, the implementation of this specification in the high-level source language following a transformational approach, and third, the construction of a binary executable written in the compilers target language. The focus of this report is on the first verification task. This proof has been completely mechanized using the PVS specification and verification system and is one of the largest case-studies in formal verification we are aware of.
  • Thumbnail Image
    Item
    A nonadaptive NC checker for permutation group intersection
    (Universität Ulm) Arvind, Vikraman; Torán, Jacobo
    N/A
  • Thumbnail Image
    Item
    A pumping lemma for output languages of attributed tree transducers
    (Universität Ulm) Kühnemann, Armin; Vogler, Heiko
    N/A
  • Thumbnail Image
    Item
    A slightly improved upper bound on the size of weights sufficient to represent any linearly separable Boolean function
    (Universität Ulm) Schmitt, Michael
    The maximum absolute value of integral weights sufficient to represent any linearly separable Boolean function is investigated. It is shown that upper bounds exhibited by Muraga (1971) for rational weights satisfying the normalized system of inequalities also hold for integral weights. Therewith, the previous best known upper bound for integers is improved by approximately a factor of 1/2.
  • Thumbnail Image
    Item
    A small span theorem within P
    (Universität Ulm) Lindner, Wolfgang; Schuler, Rainer
    N/A
  • Thumbnail Image
    Item
    A universal unification algorithm based on unification-driven leftmost outermost narrowing
    (Universität Ulm) Vogler, Heiko; Faßbender, Heinz
    We formalize a universal unification algorithm for the class of equational theories which is induced by the class of canonical, totally-defined, not strictly subunifiable term rewriting systems (for short: ctn-trs). For a ctn-trs R and for two terms t and s, the algorithm computes a ground-complete set of E_R-unifiers of t and s, where E_R is the set of rewrite rules of R viewed as equations. The algorithm is based on the unification-driven leftmost outermost narrowing relation (for short: ulo narrowing relation) which is introduced in this paper. The ulo narrowing relation combines usual leftmost outermost narrowing steps and unification steps. Since the unification steps are applied as early as possible, some of the nonsuccessful derivations can be stopped earlier than in other approaches to E_R-unification. Furthermore, we formalize a deterministic version of our universal unification algorithm that is based on a depth-first left-to-right traversal through the narrowing trees.