[All BiBTeX entries for this year]

B.C.M. Wondergem, P. van Bommel, T.W.C. Huibers, and Th.P. van der Weide. * How is this document`s relevancy derived? Personalizing Inferences in Preferential Models. *Technical report, Computing Science Institute, University of Nijmegen, 1997.

In Information Retrieval, user preferences and domain knowledge play an important role. This article shows how to incorporate domain knowledge in a logical framework and provides a mechanism to exploit user preferences to personalize domain knowledge, based on the inferences made in the matching functions. The matching functions are essentially symbolic logical inferences. The logic used in this article are Preferential Models, which are augmented with domain knowledge by providing an enriched aboutness relation. However, the techniques described in this article are applicable to other logics as well. A way to personalize the domain knowledge is given, which also gives the user insight into the workings of the matching functions. In addition, sound inference rules, which are tailor-made for the domain knowledge, are provided.

[ Missing PDF ] [ Bibtex ]

P. van Bommel, and Th.P. van der Weide. * Conceptual Graphs as a Basis for Verification, Matching, and Similarity in the Context of Information System Development. *Technical report: CSI-N9701, January, Radboud University Nijmegen, 1997.

The KISS-method uses graphical structures to represent the models which are constructed during analysis and design. Such graphical structures are referred to as model graphs. Special patterns are used to describe consistency properties of model graphs, and can serve as a basis for transformations between different types of model graphs.In th is paper we show how model graphs are related to conceptual graphs, which have been widely accepted to represent knowledge structures. This relation provides the opportunity to benefit from the vast amount of results and algorithms which have been developed for conceptual graphs. As an example, we discuss similarity between models.Conceptual graphs can also serve as a uniform basis for all models of the KISS-method. This is not furhter elaborated in this paper. Conceptual graphs have a clear relation to first order prdicate calculus. This facilitates the possibility to reason about KISS-models in a formal mathematical style, meanwhile having a direct link to t he original KISS-models.In this paper the concept of patterns and its matching, is further elaborated. An inverse style of matching can be seen as an introduction of regular graph patterns.Finally we discuss graph transformation rules.

[ Missing PDF ] [ Bibtex ]

P. van Bommel, and Th.P. van der Weide. * SRL Handboek. *Technical report: CSI-N9702, Januari, Radboud University Nijmegen, 1997.

[ Missing PDF ] [ Bibtex ]

G. Kovï¿½cs, and P. van Bommel. * Designing Advanced Databases Using Dependency Graph Conducted Schema Transformation Algorithm. *Technical report: CSI-N9703, March, Radboud University Nijmegen, 1997.

[ Missing PDF ] [ Bibtex ]

A. Bleeker. * User purposes in user-centred Hypermedia design. *Technical report: CSI-N9704, April, Radboud University Nijmegen, 1997.

[ Missing PDF ] [ Bibtex ]

A. Bleeker. * A methodology for user-centred Hypermedia design. *Technical report: CSI-N9705, April, Radboud University Nijmegen, 1997.

[ Missing PDF ] [ Bibtex ]

A.T. Arampatzis. * Preprocessing documents in Profile. *Technical report: CSI-N9706, May, Computing Science Institute, University of Nijmegen, Nijmegen, The Netherlands, 1997.

[ Missing PDF ] [ Bibtex ]

B.C.M. Wondergem, J. Simons, A.T. Arampatzis, J. Mackowiak, D. Tarenskeen, and T.W.C. Huibers. * Profile Information Filtering Project. *Technical report: CSI-N9707, September, Radboud University Nijmegen, 1997.

This article provides the overall position paper of the PROFILE Information Filtering Project. The motivation for and context of the project are stated, as well as the overall organizational and functional project structures. In addition, concepts common the the project as a whole are described. The four main conponents - User Modelling, Parsing, Retrieval, and Interaction - are described in detail. The context in which reseach wil be conducted is described for each component, as well as important research questions and possible approaches to overcome the stated difficulties.

[ Missing PDF ] [ Bibtex ]

J.A. Moinhos Cordeiro. * Research Line on Functional Programming Languages. *Technical report: CSI-N9708, September, Radboud University Nijmegen, 1997.

[ Missing PDF ] [ Bibtex ]

M. Devillers. * Mechanized support for I/O automata. *Technical report: CSI-N9710, December, Radboud University Nijmegen, 1997.

Formal methods are mathematical techniques used to verifysafety-critical systems. Recent successful verifications have been credited to newly developed computer tools which mechanically support (parts of) the verification process. My research concentrates on the mechanical support of verifications of systems described as I/O automata. I wish to show how the I/O automata model of Lynch and Tuttle can be mechanically supported, and how this support can be used in a teaching environment. The support is to be implemented in a workbench, which serves as a front-end to other tools. A central research question is how to successfully combine existing technology, in particular model checkers and theorem provers, for verification purposes.

[ Missing PDF ] [ Bibtex ]

M.C.A. Devillers, and W.O.D. Griffioen. * A Formalization of Finite and Infinite Sequences in PVS. *Technical report: CSI-R9702, March, Radboud University Nijmegen, 1997.

Sequences are often used structures in mathematics and computer science.While working on a formalization of IO-automata theory, we found, asothers did before us, that a large portion of the lemmas provenconcerned sequences. The complexity of the definitions and proofs isincreased by having sequences of both finite and infinite length in asingle type.In this paper a formalization of these kinds of sequences is presented,and it is explained how some problems of other formalizations arecircumvented. The formalization is implemented in the PrototypeVerification System (PVS).This paper may be of interest to people in the field of concurrency,mechanical verifications, and to people with an interest in applications of higher order logic.

[ Missing PDF ] [ Bibtex ]

U. Hensel, and B.P.F. Jacobs. * Proof Principles for Datatypes with Iterated Recursion. *Technical report: CSI-R9703, March, Radboud University Nijmegen, 1997.

Data types like trees which are finitely branching and of (possibly) infinite depth are described by iterating initial algebras and terminal coalgebras. We study proof principles for suchdata types in the context of categorical logic, following andextending the approach of~\cite{HermidaJ95b,JacobsHermidaIndCoind96}.The technical contribution of this paper involves a description of initial algebras and terminal coalgebras in total categoriesof fibrations for lifted ``datafunctors''. These lifted functors are used to formulate our proof principles. We test these principles by proving some elementaryresults for four kinds of trees (with finite or infinite breadth or depth) using the proof tool PVS.

[ Missing PDF ] [ Bibtex ]

B.P.F. Jacobs. * Invariants, Bisimulations and the Correctness of Coalgebraic Refinements. *Technical report: CSI-R9704, March, Radboud University Nijmegen, 1997.

Coalgebraic specifications are used to formally describe thebehaviour of classes in object-oriented languages. In this paper, ageneral notion of refinement between two such coalgebraicspecifications is defined, capturing the idea that one ``concrete''class specification realises the behaviour of the other, ``abstract''class specification. Two (complete) proof-techniques are given toestablish such refinements: one involving an invariant (a predicatethat is closed under transitions) on the concrete class, and oneinvolving a bisimulation (a relation that is closed undertransitions) between the concrete and the abstract class. The lattercan only be used if the abstract class is what we call totallyspecified. The underlying theory of invariants and bisimulations in acoalgebraic setting is included, involving least and greatestinvariants and connections between invariants and bisimulations.Also, the proof-principles are illustrated in several examples(which are fully formalised and verified in PVS).

[ Missing PDF ] [ Bibtex ]

J.W.G.M. Hubbers, and T.F. Verhoef. * A Real-life Application of Software Component Modelling. *Technical report: CSI-R9705, Computing Science Institute, University of Nijmegen, Nijmegen, The Netherlands, 1997.

[ Missing PDF ] [ Bibtex ]

J.W.G.M. Hubbers, and A.H.M. ter Hofstede. * An Investigation of the Core Concepts of Object-Oriented Conceptual Data Modeling. *Technical report: CSI-R9706, Computing Science Institute, University of Nijmegen, 1997.

[ Missing PDF ] [ Bibtex ]

A.I. Bleeker, P.D. Bruza, and Th.P. van der Weide. * A User-centred View on Hypermedia Design. *Technical report: CSI-R9707, Computing Science Institute, University of Nijmegen, 1997.

Ever-increasing quantities of information, together with new developments on storage and retrieval methods, are confronting todays users with a huge information supply that they can barely oversee. Hypermedia information retrieval systems try to assist users in finding their way through the supply, but reality this is where many systems fall short. The reason is that most of them do not really communicate with users or find out what they really want. Instead, a bottom-up approach that reasons mainly from an information-oriented view point, has been a major design focus. We argue that the design of hypermedia systems should be based on an integration between both a top-down (user-oriented) and a bottom-up (information-oriented) approach, to develop hypermedia systems that know and understand their users. In this article, we present initial results of a new user-oriented approach.

Ulrich Hensel, and B.P.F. Jacobs. * Coalgebraic Theories of Sequences in PVS. *Technical report: CSI-R9708, June, Radboud University Nijmegen, 1997.

This paper explains the setting of anextensive formalisation of the theory of sequences (finite andinfinite lists of elements of some data type) in the PrototypeVerification System PVS. This formalisation is based on thecharacterisation of sequences as a final coalgebra, which is usedas an axiom. The resulting theories comprise standardoperations on sequences like composition (or concatenation), filtering,flattening, and their properties. They also involve the prefixordering and proofs that sequences form an algebraic complete partial order. The finality axiom gives rise to various reasoning principles, likebisimulation, simulation, invariance, and induction for admissiblepredicates. Most of the proofs of equality statements are based on bisimulations, and most of the proofs of prefix order statements use simulations. Some significant aspects of these theories are described in detail.This coalgebraic formalisation of sequences is presented as a concreteexample that shows the importance and usefulness of coalgebraic modeling andreasoning. Hopefully, it will help to convey the view thatcoalgebraic data types should form an intrinsic part of (future)languages for programming and reasoning. Therefore, somesuggestions for an appropriate syntax for coalgebraic datatypesare included.The use of sequences as a final coalgebra is demonstrated intwo (standard) applications: a refinement result for automatainvolving sequences of actions, and a coalgebraic definition plus correctness proof for an insert operation on ordered sequences.

[ Missing PDF ] [ Bibtex ]

J. Moonen, J. Romijn, O. Sies, J. Springintveld, L. Feijs, and R. Koymans. * A Two-Level Approach to Automated Conformance Testing of VHDL Design. *Technical report: CSI-R9709, June, Radboud University Nijmegen, 1997.

For manufacturers of consumer electronics, conformance testing of embedded software is a vital issue. To improve performance, parts of this software are implemented in hardware, often designed in the Hardware Description Language VHDL. Conformance testing is a time consuming and error-prone process. Thus automating (parts of) this process is essential.There are many tools for test generation and for VHDL simulation. However, most test generation tools operate on a high level of abstraction and applying the generated tests to a VHDL design is a complicated task. For each specific case one can build a layer of dedicated circuitry and/or software that performs this task. It appears that the ad-hoc nature of this forms the bottleneck of the testing process. We propose a generic solution for bridging this gap: a generic layer of software dedicated to interface with VHDL implementations. It consists of a number of Von Neumann-like components that can be instantiated for each specific VHDL design.This paper reports on the construction of and some initial experiences with a concrete tool environment based on these principles.

[ Missing PDF ] [ Bibtex ]

B.C.M. Wondergem, P. van Bommel, T.W.C. Huibers, and Th.P. van der Weide. * How is this documentï¿½s relevancy derived?. *Technical report: CSI-R9710, June, Radboud University Nijmegen, 1997.

In Information Retrieval, user preferences and domain knowledge play an important role. This article shows how to incorporate domain knowledge in a logical framework and provides a mechanism to exploit user preferences to personalize domain knowledge, based on the inferences made in the matching functions. The matching functions are essentially symbolic logical inferences. The logic used in this article are Preferential Models, which are augmented with domain knowledge by providing an enriched aboutness relation. However, the techniques described in this article are applicable to other logics as well. A way to personalize the domain knowledge is given, which also gives the user insight into the workings of the matching functions. In addition, sound inference rules, which are tailor-made for the domain knowledge, are provided.

[ Missing PDF ] [ Bibtex ]

M.S. klein Gebbinck, and T. E. * Area Estimation with Subpixel Accuracy for Industrial ImagingSystems. *Technical report: CSI-R9711, July, Radboud University Nijmegen, 1997.

Industrial imaging systems used for product quality control often needto make an accurate estimation of an object's area. Usually the area isestimated by counting the number of pixels classified as belonging tothe object. However, with a technique called decomposition, the numberof pixels can be estimated more accurately at the same resolution, oras accurately at a lower resolution. Another way to reduce the hardwarecosts is to lower the spatial sampling rate. The negative effects onthe area estimation accuracy can be counteracted by reconstructing theoriginal image using interpolation. In this paper, we present theresults of two experiments using HP ScanJet 4c images in which thecapabilities and limitations of decomposition and interpolation wereassessed quantitatively. It appeared that the resolution could belowered with a factor 25 without decreasing the accuracy of theestimation. A reduction of the sampling rate, on the other hand, couldnot be compensated for as well. However, interpolation did seem torestrict the decrease in accuracy somewhat, although the results werenot entirely conclusive due to hardware related reasons.

[ Missing PDF ] [ Bibtex ]

Jan Springintveld, F.W. Vaandrager, and P. R. D`Argenio. * Testing Timed Automata. *Technical report: CSI-R9712, August, Radboud University Nijmegen, 1997.

We present a generalization of the classical theory of testing forMealy machines to a setting of dense real-time systems.A model of timed I/O automata is introduced, inspired by the timedautomaton model of Alur and Dill, together with a notion of test sequencefor this model.Our main contribution is a test generation algorithm for black-box conformancetesting of timed I/O automata.Although it is highly exponential and cannot be claimed to be of practicalvalue, it is the first algorithm that yields a finite and complete setof tests for dense real-time systems.

[ Missing PDF ] [ Bibtex ]

Hanno Wupper, and Hans Meijer. * A Taxonomy for Computer Science. *Technical report: CSI-R9713, August, Radboud University Nijmegen, 1997.

We try to capture the essence of information technology and computerscience, arguing that information technologists have the same principalgoal as all technologists: to create machines with certain properties. Toachieve this, they formalize the problem, i.e. abstract the properties intoa specification and invent or develop a schema, i.e. an abstraction of themachine's structure. Subsequently, it is their principal task to prove thatthe schema satisfies the specification. Computer scientists developmathematical and physical means to support or even enable that task. Fromthis, the principal research questions of computer science may be derived.>From this viewpoint, we try to propose a consistent set of notions togetherwith a consistent terminology, which may clarify the relation ofinformation technology and computer science to other scientific disciplinesand also give rise to new ideas about computer science education.

[ Missing PDF ] [ Bibtex ]

Marieke Huisman. * Binary addition in Lego. *Technical report: CSI-R9714, August, Radboud University Nijmegen, 1997.

This paper describes how the implementation of hardwarebinary additioncan be simulated in the interactive proof development system Lego.A general addition function is described that can add two lists ofarbitrary digits.Several properties are proven for this general addition function. It is shownhow this addition function can be used for particular digits such as bits andlists of length k of bits.These properties allow that all the reasoning and calculations are done onthe level of binary numbers, where this can be done much faster.

[ Missing PDF ] [ Bibtex ]

Marieke Huisman. * Designing a satellite tracking system with the use of PVS and Maple. *Technical report: CSI-R9716, September, Radboud University Nijmegen, 1997.

This paper describes the specification and design of a satellite trackingsystem. Its goal is to show how such a design can be made and verified formally,with the aid of various tools. The design is compositional and in some of the components much mathematics is involved. The specifications of the whole system and its components are described in predicate logic and in the specification language of the theorem prover PVS. Because of the mathematics that is involved it was useful to use also the computer algebra system Maple.Maple simplifies some expressions, so that the results can be used by PVS.This paper shows that formal methods can be used easily on a high levelof design and that the use of different tools is very practical. Further itshows that the design process is easier, when first an idealized version ofthe system is designed, which is then transformed into a more realistic one.

[ Missing PDF ] [ Bibtex ]

J.I. Farkas, V. Kamphuis, and J.J. Sarbo. * Natural Language Concept Analysis: Towards a Theoretical Foundation. *Technical report: CSI-R9717, September, Radboud University Nijmegen, 1997.

Can we do text analysis without phrase structure? We think the answercould be positive. In this paper we outline the basics of anunderlying theory which yields hierarchical structure as the result of more abstract principles relating to the combinatorial properties oflinguistic units. We discuss the nature of these propertiesand illustrate our model with examples.

[ Missing PDF ] [ Bibtex ]

U. Hensel, M. Huisman, B.P.F. Jacobs, and H. Tews. * Reasoning about classes in Object-Oriented Languages: Logical Models and Tools. *Technical report: CSI-R9718, October, Radboud University Nijmegen, 1997.

A formal language CCSL is introduced for describing specifications ofclasses in object-oriented languages. We show how class specifications in CCSL can be translated into higher order logic. This allows us to reason about these specifications.In particular, it allows us (1)to describe (various) implementations of a particular class specification,(2)to develop the logical theory of a specific class specification, and (3)to establish refinements between two class specifications.We use the (dependently typed) higher order logic of the proof-assistantPVS, so that we have extensive tool support for reasoning about class specifications. Moreover, we describe our own front-end tool to PVS, which generates fromCCSL class specifications appropriate PVS theoriesand proofs of some elementary results.

[ Missing PDF ] [ Bibtex ]

P.A. Jones, P. van Bommel, C.H.A. Koster, and Th.P. van der Weide. * Stratified Recursive Backup for Best First Search. *Technical report: CSI-R9720, November, Information Systems Group, Computing Science Institute, University of Nijmegen, The Netherlands, EU, 1997.

In this paper a new abstract machine model, the Stratified Recursive Backup machine model, is described. This machine model can be used to implement best first search algorithms efficiently. Two applications of best first search, a text layouting system and a natural language parser, are analyzed to provide an indepth understanding of the Stratified Recursive Backup machine model.

A.T. Arampatzis, Th.P. van der Weide, P. van Bommel, and C.H.A. Koster. * Syntactical Analysis for Text Filtering. *Technical report: CSI-R9721, November, Computing Science Institute, University of Nijmegen, Nijmegen, The Netherlands, 1997.

[ Missing PDF ] [ Bibtex ]

B.C.M. Wondergem, P. van Bommel, T.W.C. Huibers, and Th.P. van der Weide. * Opportunities for Electronic Commerce in Agent-Based Information Discovery. *Technical report: CSI-R9722, December, Radboud University Nijmegen, 1997.

This article investigates the connection between Electronic Commerce (EC) and Information Discovery (ID). ID is the synthesis of distributed Information Retrieval and Information Filtering, filled in with intelligent agents and information brokers. Currently, no link exists between EC and ID. We argue that this link consists of a cost model for ID. We therefore propose several (types of) cost models, which enable application of EC to the whole of ID. This is illustrated with examples.

[ Missing PDF ] [ Bibtex ]

A. Fehnker. * Automotive Control Revisited. *Technical report: CSI-R9723, December, Radboud University Nijmegen, 1997.

Reachability analysis of hybrid system imposes restrictions on either the continuous or the discrete behavior. In this paper a method is proposed that approximates the reachable set of linear systems by linear inequalities. It allows to use the full continuous dynamics of hybrid systems for reachability analysis. This method is applied to an automotive control problem, which was presented by Stauner et al. in [SMF97]

[ Missing PDF ] [ Bibtex ]

M. Devillers, D. Griffioen, and O. Mï¿½ller. * Possibly Infinite Sequences in Theorem Provers: A Comparative Study. *Technical report: CSI-R9724, December, Radboud University Nijmegen, 1997.

We compare four different formalizations of possibly infinitesequences in theorem provers based on higher-order logic. The formalizations have been carried out in different proof tools, namely in Gordon's HOL, in Isabelle and in PVS. The comparison considers different logics and proof infrastructures, but emphasizes on the proof principles that are available for each approach. The different formalizations discussed have been used not only to mechanize proofsof different properties of possibly infinite sequences, but also for the verification of some non-trivial theorems of concurrency theory.

[ Missing PDF ] [ Bibtex ]

D.J. Chen, W.C. Chen, C.C. Hwang, C.S. Koong, G.Y. Hsu, and N.W.P. van Diepen. * A Visual Software Construction Approach. *Technical report: CSI-R9725, December, Radboud University Nijmegen, 1997.

Software reuse is considered one of the effective approaches forimproving software productivity and software quality. ReusableSoftware Components (RSCs) are the basic building components forsoftware program constructed based on thesoftware reuse approach. An object-oriented approach is used forthe design and implementation of our RSCs. So far, we haveimplemented more than 300 reusable software components (includingdesign level frameworks), in various application domains, withabout 200,000 lines of code in our library. These components andframeworks are accumulated from the design and implementation ofstrategy-based game systems, multimedia authoring systems(2-D and 3-D), multimedia play-back systems, and other applicationsystems. The RSCs and frameworks can be visualized through iconsfor a visual programming model. In this way, reuse-in-the-large isrealized practice by use of a visual programming technique basedon these visualized components. In this paper, the design principleand the implementation technique for our RSCs and frameworks arediscussed, and a visual software construction paradigm is proposedbased on the use of RSCs and frameworks. Specifically, both thedesign concept and the implementation of such a visual softwareconstruction approach and potential advantages of the proposedconstruction approach are discussed. From our study, we believethat the visual software construction paradigm will become a newdirection for both academic researchers and software constructorsto search for a better software construction approach.

[ Missing PDF ] [ Bibtex ]

H. van Thienen. * Prosperoï¿½s Book. *Technical report: CSI-R9726, December, Radboud University Nijmegen, 1997.

Prospero is a programmable calculator, designed to run on palm top computers such as the Psion Series 3a. Prospero can be programmed using a small functional language which is also called Prospero. This report describes the syntax and semantics of the Prospero language.Prospero is designed to expres numerical computations. Therefore, the main basic data objects are (real) numbers. The only data structuring mechanism is the l ist. Prospero contains many constructs and operators to handle numbers and lists. This report only describes the language. Its purpose is to document the language as it is currently implemented. It is not intended as a tutorial, neither is it an apology in which the the rationale behind certain design decisions is explained

[ Missing PDF ] [ Bibtex ]

A.H. Mader. * Verification of Modal Properties Using Infinite Boolean Equation Systems. *Technical report: CSI-R9727, December, Radboud University Nijmegen, 1997.

In this paper we show the equivalence of model checking infinite systems and solving infinite Boolean equation systems, andgive a method that solves infinite Boolean equation systems. The method issound and complete, even if the problem itself is undecidable.

[ Missing PDF ] [ Bibtex ]

M.C.A. Devillers, W.O.D. Griffioen, J.M.T. Romijn, and F.W. Vaandrager. * Verification of a Leader Election Protocol. *Technical report: CSI-R9728, December, Radboud University Nijmegen, 1997.

The IEEE 1394 high performance serial multimedia bus protocolallows several components to communicate with each other at high speed.In this paper we present a formal model and verification of a leaderelection algorithm that forms the core of the tree identify phase ofthe physical layer of the 1394 protocol.We describe the algorithm formally in the I/O automata model ofLynch and Tuttle, and verify that for an arbitrary tree topology exactlyone leader is elected. A large part of our verification has been checkedmechanically with PVS, a verification system for higher-order logic.

H. Wupper. * Design as the Discovery of a Mathematical Theorem:. *Technical report: CSI-R9729, December, Radboud University Nijmegen, 1997.

This paper tries to contribute to the understanding of the essence of rational systems design and verification. Information technologists and teachers and students of computer science may find the concepts presented here helpful to disentangle complex achievenments of computer science and re-use their constituents in other contexts, but also to view their own activities in the light of other disciplines.First a consistent set of notions and a diagram and a formula are introduced, with respect to which important aspects of a rational design process can be understood, together with a proposal for a consistent terminology. Subsequently, formal definitions are provided for basic concepts of formal methods and a mathematical foundation for our formula. They shall illustrate that the rï¿½le of mathematics in development and verification is not limited to useful calculations: Ideally, designing is a creative mathematical activity, which comprises finding a theorem, if necessary strengthening its assumptions until it can be proven.Although for good reasons most systems are designed without use of formal methods it may be a source of useful insight to understand all design as an ï¿½approximationï¿½ of such a mathematical activity. This leads amongst others to a taxonomy of design decisions and of fault tolerance. And it may help to relate paradigms, theories, methods, languages, and tools from different areas of computer science to each other to make optimal use of them.

[ Missing PDF ] [ Bibtex ]

H. Wupper. * Quantified Modal Algebra:. *Technical report: CSI-R9730, December, Radboud University Nijmegen, 1997.

[ Missing PDF ] [ Bibtex ]