ICIS Technical Reports:


2017 2016 2015 2014 2013 2012 2011 2010 2009 2008 2007 2006 2005 2004 2003 2002 2001 2000 1999 1998 1997 1996 1995 1994 1993 1992 1991 1990 1989 1988 1987

2003

[All BiBTeX entries for this year]

A conceptual model of Information Supply. Technical report, May, 2003.

This paper introduces a conceptual model for information supply. The model is based on the notion that similar information can be conveyed by multiple representations. Hence, we define that information services provide access to several representations. The relation between these two concepts is provided by what we call features. Furthermore, we recognize the fact that information services are interrelated by means of relations. We informally introduce this model using the ER-notation, and provide a formalization as well. Last but not least, the notion of transformations is introduced. Using transformations we are able to transform representations to a type that is both acceptable and useful for the user of an IR-system.

[ Missing PDF ] [ Bibtex ]

F.A. Grootjen, and Th.P. van der Weide. Information Retrieval as a Semantics Transformation. Technical report: NIII-R0303, Computing Science Institute, University of Nijmegen, 2003.

In this paper we present Information Retrieval as a semantics transformation problem. We describe a general theory to derive concepts, and discuss 2 special cases: the vector model and the set model. The vector model leads to Singular Value Decomposition, while the set model leads to Formal Concept Analysis. We discuss the relation between the resulting systems of concepts.

[ PDF ] [ Bibtex ]

D.C. van Leijenhorst. A Note on Expression Growth in Process Algebra. Technical report: NIII-R0304, February, Radboud University Nijmegen, 2003.

[ Missing PDF ] [ Bibtex ]

D.C. van Leijenhorst. On Witt's Proof of Wedderburn's Theorem. Technical report: NIII-R0305, February, Radboud University Nijmegen, 2003.

[ Missing PDF ] [ Bibtex ]

A. Fehnker, F.W. Vaandrager, and M. Zhang. Modeling and Verifying a Lego Car Using Hybrid I/O Automata. Technical report: NIII-R0308, March, Radboud University Nijmegen, 2003.

We illustrate the application of the hybrid I/O automata framework of Lynch, Segala & Vaandrager by using it to model and analyze the behavior of a simple Lego car with caterpillar treads. We derive constraints on the values of the parameters that occur in our hybrid model that guarantee that the car will always move forwards along a black tape, and will never get off the tape or move backward. In order to symplify the correctness proof, we intoduce a transition systems that abstracts from the hybrid automation in a rather drastic manner, but still preserves validity of the correctness properties in which we are interested. Even though our original model does not involve any disturbances, the general parametric analysis of the system allows us to extend our results in a trivial manner to a hybrid model in which several disturbances are allowed (mistakes in measurements of lengths, drift and jitter of the hardware clock, velocity, and distance between the two caterpillar treads).

[ PDF ] [ Bibtex ]

L. Burdy, Y. Cheon, D. Cok, M. Ernst, J.R. Kiniry, G.T. Leavens, K.R.M. Leino, and E. Poll. An overview of JML tools and applications. Technical report: NIII-R0309, March, Radboud University Nijmegen, 2003.

The Java Modeling Language (JML) can be used to specify the detailed design of Java classes and interfaces by adding annotations to Java source files. The aim of JML is to provide a specification language that is easy to use for Java programmers and that is supported by a wide range of tools for specification type-checking, runtime debugging, static analysis, and verification.This paper gives an overview of the main ideas behind JML, the different groups collaborating to provide tools for JML, and the existing applications of JML. Thus far, most applications have focused on code for programming smartcards written in the Java Card dialect of Java.

[ Missing PDF ] [ Bibtex ]

B.P.F. Jacobs, J.R. Kiniry, and M.E. Warnier. Java Program Verification Challenges. Technical report: NIII-R0310, March, Radboud University Nijmegen, 2003.

This paper aims to raise the level of verification challenges by presenting a collection of sequential Java programs with correctness annotations formulated in JML. The emphasis lies more on the underlying semantical issues than on verification.

[ Missing PDF ] [ Bibtex ]

B. Gebremichael, and F.W. Vaandrager. Control Synthesis for a Smart Card Personalization System using Symbolic Model Checking. Technical report: NIII-R0312, May, Radboud University Nijmegen, 2003.

Using the Berkeley SMV symbolic model checker we synthesize, under certain error assumptions, a controller for the smart card personalization system, a case study that has been proposed by Cybernetix Recherche in the context of the EU IST project AMETIST. The contoller that we synthesize, and of which we prove optimality, has been previously patented. Due to the large number of states (which is beyond 1011), this control synthesis problem appears to be out of the scope of existing tools for contoller synthesis, which typically use some form of explicit state enumeration. Our result provides new evidence that model checkers can be useful to tackle industrial sized problems in the area of scheduling and control synthesis.

[ PDF ] [ Bibtex ]

S.J.B.A. (Stijn) Hoppenbrouwers, and H. Weigand. Conceptualisation Support for Language Development. Technical report: NIII-R0314, May, Radboud University Nijmegen, 2003.

Conceptualisation, or the development of Conceptual Models, can be performed for several reasons. One important goal nowadays is to support communication systems. A communication system aims at supporting communication in or between organizations and is typically supportes by IT. It is based on some language that must be developed and agreed upon first, and must be adapted or redeveloped when changes in the environment occur. Conceptualisation as part of language development becomes more an more a continuous effort. This paper introduces a phased model for the conceptualisation process. It discusses which techniques are useful in which phase and which ones can be applied in a continuous conceptualisation effort.

[ Missing PDF ] [ Bibtex ]

C.-B. Breunesse, N. Catano, M. Huisman, and B.P.F. Jacobs. Formal Methods for Smart Cards: an experience report. Technical report: NIII-R0316, August, Radboud University Nijmegen, 2003.

This paper presents a case study in formal specification and verification of a smart card application. The application is an electronic purse implementation, developed by the smart card producer Gemplus as a test case for formal methods for smart cards. The application has beensupplemented (by the authors) with specifications using the Java Modeling Language (JML), a language designed tospecify the functional behavior of Java classes. The reason for using JML as a specification language is that several tools are available to check (parts of) the specification w.r.t. an implementation. These tools vary in their level of automatization and in the level of correctness they ensure.Several of these tools have been used for the Gemplus case study. We discuss how the usage of these different tools is complementary: large parts of the specification can be checked automatically, while more precise verification methods can be used for the more intricate parts of the specification and implementation. We believe that having such a range of tools available for a single specification language is an important step towards acceptance of formal methods in industry.

[ Missing PDF ] [ Bibtex ]

E.D. Schabell. Building the PRONIR Conversion Clearinghouse. Technical report: NIII-R0317, Nijmegen Institute for Information and Computing Sciences, University of Nijmegen, Nijmegen, The Netherlands, EU, 2003.

As a vital part of the larger architecture, our document conversion system will need to provide for the transformation of documents to a requested format. The first step on the way to realizing this system is to gather all the various conversion routines in a central location. To achieve this, the Conversion Clearinghouse has been implemented to provide a means for anyone to submit her favorite conversion routines. Our Conversion Clearinghouse also allows anyone to browse through and pick out any of the collected conversions.

The following report describes the design and implementation of the various elements that make up our Conversion Clearinghouse. This work is part of the ongoing research project Profile Based Retrieval Of Networked Information Resources (PRONIR).

[ PDF ] [ Bibtex ]

B.P.F. Jacobs, and E. Poll. Java Program Verification at Nijmegen: Developments and Perspective. Technical report: NIII-R0318, September, Radboud University Nijmegen, 2003.

This paper presents a historical overview of the work on Java program verification at the University of Nijmegen (the Netherlands) over the past six years (1997--2003). It describes the development and use of the LOOP tool that is central in this work. Also, it gives a perspective on the field.

[ Missing PDF ] [ Bibtex ]

S. Bosman, and Th.P. van der Weide. Information modelling by formalizing vague representations. Technical report: NIII-R0319, September, Radboud University Nijmegen, 2003.

[ Missing PDF ] [ Bibtex ]

M.D. Oostdijk, and M.E. Warnier. On the combination of Java Card Remote Method Invocation and JML. Technical report: NIII-R0321, October, Radboud University Nijmegen, 2003.

This paper explores the possibilities for using the Java Modeling Language (JML) to specify Java Card applets that use Remote Method Invocation (JCRMI). The JCRMIframework makes it possible to call methods directly on a Java Card smart card without the (explicit) use of low level byte sequences, called APDUs. We introduce a new way of designing JCRMI applets, using the Java Modeling Language (JML) to formally specify (part of) its code. It turns out that some advanced JML specification features, such as model variables, are necessary to specify JCRMIapplets. Two JML tools, the JML runtime assertion checker and the LOOP tool, are subsequently used to verify that the implementation satisfies the JML specifications. We conclude that the JML specifications are simpler and easier to write, understand and verify when using JCRMI. Ideally this should lead to more trustworthy and error free code.

[ PDF ] [ Bibtex ]

E.M.G.M. Hubbers, and E. Poll. Reasoning about Card Tears and Transactions in Java Card. Technical report: NIII-R0322, October, Radboud University Nijmegen, 2003.

The Java dialect Java Card for programming smartcards contains some features which do not exist in Java.Java Card distinguishes persistent and transient data(data stored in EEPROM and RAM, respectively). Because power to a smartcard can suddenly be interrupted by a so-called card tear, by someone removing the smartcard from the reader, Java Card provides a notion of transaction to ensure that updates of multiple fields in persistent memory can be performed atomically.This paper describes a way to reason about these Java Card specific language features.

[ Missing PDF ] [ Bibtex ]

M. Niqui. Exact Arithmetic on the Stern-Brocot Tree. Technical report: NIII-R0325, November, Radboud University Nijmegen, 2003.

In this paper we present the Stern-Brocot tree as a basis for performing exact arithmetic on rational and real numbers. We introduce the tree and mention its relation with continued fractions. Based on the tree we present a binary representation of rational numbers and investigate various algorithms to perform exact rational arithmetic using a simplified version of the homographic and the quadratic algorithms [19, 12]. We show generalisations of homographic and quadratic algorithms to multilinear forms in n variables and we prove the correctness of the algorithms. Finally we modify the tree to get a redundant representation for real numbers.

[ Missing PDF ] [ Bibtex ]

P.J.F. Lucas. Quality Checking of Medical Guidelines through Logical Abduction. Technical report: NIII-R0327, November, Radboud University Nijmegen, 2003.

Formal methods have been used in the past for the verificaton of the correctness of formalised versions of medical guidelines. In this paper a second possible application of the use of formal methods is proposed: checking whether a guideline conforms to global medical quality requirements. It is argued that this allows spotting design errors in medical guidelines, which is seen as a useful application for formal methods in medicine. However, this type of verification may require medical knowledge currently not available within the guidelines, i.e. medical background knowledge. in this paper, we propose a method for checking the quality of a treatment for a disorder, based on the theory of abductive diagnosis. We also examine the medical background knowledge required to be able to quality check a guideline. The method is illustrated by the formal analysis of an actual guideline for the managemant of diabetis mellitus type 2.

[ Missing PDF ] [ Bibtex ]

P. Koopman, and J. Tretmans. 9e Nederlandse Testdag. Technical report: NIII-R0328, November, Radboud University Nijmegen, 2003.

[ Missing PDF ] [ Bibtex ]

E.D. Schabell. The DocConversion framework. Technical report: NIII-R0332, Nijmegen Institute for Information and Computing Sciences, University of Nijmegen, Nijmegen, The Netherlands, EU, 2003.

Continuing where the ``PRONIR Conversion Clearinghouse'' left off, this technical report presents the basic framework of the DocConversion tool. In its first phase our DocConversion tool will support single step document conversions, provide a Broker that negotiates the conversion process and a conversion Server. This is the first of three phases to be traversed on our way to a complete document conversion system. This work is part of the ongoing research project Profile Based Retrieval Of Networked Information Resources (PRONIR).

[ PDF ] [ Bibtex ]

M. Giero, and F. Wiedijk. MMode, a Mizar Mode for the proof assistant Coq. Technical report: NIII-R0333, December, Radboud University Nijmegen, 2003.

We present a set of tactics for version 7.4 of the Coq proof assistant which makes it possible to write proofs for Coq in a language similar to the proof language of the Mizar system. These tactics can be used with any interface of Coq, and they can be freely mixed with the normal Coq tactics.The system described in this report can be downloaded on the web at

[ Missing PDF ] [ Bibtex ]