[All BiBTeX entries for this year]

Flavio D. Garcia, and Peter van Rossum. * Sound Computational Interpretation of Formal Hashes. *Technical report: ICIS-R06001, January, Radboud University Nijmegen, 2006.

This paper provides one more step towards bridging the gap between the formal and computational approaches to cryptographic protocols. We extend the well-known Abadi-Rogaway logic with probabilistic hashes and we give precise semantic to it using Canettis oracle hashing. Finally, we show that this interpretation is computationally sound.

Ling Cheung, Mariï¿½lle Stoelinga, and F.W. Vaandrager. * A testing scenario for probabilistic processes. *Technical report: ICIS-R06002, January, Radboud University Nijmegen, 2006.

We introduce a notion of finite testing, based on statistical hypothesis tests, via a variant of the well-known trace machine. Under this scenario, two processes are deemed observationally equivalent if they cannot be distinguished by any finite test. We consider processes modeled as image finite probabilistic automata and prove that our notion of observational equivalence coincides with the trace distribution equivalence proposed by Segala. Along the way, we give an explicit characterization of the set of probabilistic executions of an arbitrary probabilistic automaton A and generalize the Approximation Induction Principle by defining an algebraic CPO structure on the set of trace distributions of A. We also prove limit and convex closure properties of trace distributions in an appropriate metric space.

Martijn Hendriks, and Marcel Verhoef. * Timed Automata Based Analysis of Embedded System Architecture. *Technical report: ICIS-R06003, January, Radboud University Nijmegen, 2006.

We show that timed automata can be used to model and to analyze timeliness properties of embedded system architectures. Using a case study inspired by industrial practice, we present in detail how a suitable timed automata model is composed. Exact upper bounds on the timeliness properties can be found with the Uppaal model checker for a number of usage scenarios. We compare our results with three other performance modeling techniques. This comparison shows that if the state space of the model is tractable, Uppaal gives the most accurate results at similar cost. The proposed modeling strategy can be automated, which alleviates the difficulty and error-proneness of manually constructing timed automata models.

B. van Gils, H.A. (Erik) Proper, P. van Bommel, and Th.P. van der Weide. * Aptness based search on the Web. *Technical report: ICIS-R06005, November, Radboud University Nijmegen, 2006.

The Web has, in a relatively short period of time, evolved from a medium for information exchange between scholars to one of the most important media in modern times. This has had a major impact on the infrastructure supporting the Web. Retrieval systems that select relevant resources from the ever increasing volume of resources that are available to us are becoming more and more important. In our opinion, the traditional view on these systems (where `topical relevance` seems to be the key notion) is too limited. The main contribution of this paper is an integral view on a more advanced scheme for search on the web called aptness based retrieval.

E.D. Schabell, H.A. (Erik) Proper, and Th.P. van der Weide. * IRIS Publication Management System - the first steps towards realization. *Technical report: ICIS-R06008, December, Radboud University Nijmegen, 2006.

The IRIS Publication Management System (PMS) has been a long time in coming. It has been a wish of the IRIS department to have a single entry point for dealing with the publications created by its members. The complexities of not only accepting new submissions, but to process these submissions on through the existing institutional publication infrastructure is not a hurdle easily taken. The submission of both internal and external publications generates not only a collection of doc- uments, but also a very valuable and maybe useful repository of publication data. If this data were to be collected, protected from inconsistencies and properly organized then one would only be limited in her imagination as the the uses that it could be put. To start with, one can begin to pro vide a very interesting playground for departmental retrieval experiments, provide various forms of exportable formats (think of HTML, BiBTeX, text, etc.) and generate any type of organizational reporting as deemed necessary (such as yearly overviews of departmental publications). This document discusses the definition and design of the IRIS PMS This includes the motivation (why), the (functional) requirements (what), the key design principles as well as the actual design (how).

C. Haack, E. Poll, and A. Schubert. * Immutable objects in Java. *Technical report: ICIS-R06010, Radboud University Nijmegen, 2006.

Immutability is a very useful and desirable property for objects. This paper investigates different possible notions of immutability for Java objects, to find out which notion is the most intuitive and useful, both when it comes to ways of enforcing immutability of objects, and when it comes to exploiting information about (im)mutability of objects in program verification and in various static analyses. Our ultimate aim is to agree on a semantics for an *immutable* keyword in JML.

B. van Gils, and D. Vojevodina. * The effects of exceptions on enterprise architecture. *Technical report: ICIS-R06011, February, Radboud University Nijmegen, 2006.

Exception handling be enterprises is an increasingly important topic since execptions may seriously disrupt day to day operations which may impact on the profits of the enterprise. In this paper we explore two views on the enterprise (top down: architecture, and bottom up: workflow) with respect to exception handeling. More specifically, we focus on using both views on the enterprise to handel exceptions in a structured and efficient manner.

L. Klein Holte, M. Jansen, J. Mutter, and E.D. Schabell. * It is about time for the AbTLinux
dependency engine. *Technical report: ICIS-R06013, February, Radboud University Nijmegen, 2006, A result of RE class of 2005/2006 student project..

This document describes the requirements for the ABout Time Linux dependency engine, a component of the AbTLinux package manager. These requirements were obtained by a student project group that participated in the Radboud University Nijmegen course called Requirements Engineering. This document represents the best results obtained from the six participating groups. The basis of the project flows from the main AbTLinux project goals. Clearly documented design, clear development goals leading to each release and just getting them done. Most members of the AbTLinux project have worked on other Linux distribution projects and have grown tired of working on badly documented designs. This requirements documents goal is to provide a structured and clear way of gathering information for the dependency engine project.

R. Jurgelenaite, T. Heskes, and P.J.F. Lucas. * Noisy Threshold Functions for Modelling Causal Independence in Bayesian Networks . *Technical report: ICIS-R06014, February, Radboud University Nijmegen, 2006.

Causal independence modelling is a well-known method both for reducing the size of probability tables and for explaining the underlying mechanisms in Bayesian networks. Many Bayesian network models incorporate causal independence assumptions; however, only the noisy OR and noisy AND, two examples of causal independence models, are used in practice. Their underlying assumption that either at least one cause, or all causes together, give rise to an effect, however, seems unnecessarily restrictive. In the present paper a new, more flexible, causal independence model is proposed, based on the Boolean threshold function. A connection is established between conditional probability distributions based on the noisy threshold model and Poisson binomial distributions, and the basic properties of this probability distribution are studied in some depth. We present and analyse recursive methods as well as approximation and bounding techniques to assess the conditional probabilities in the noisy threshold models.

S Djajasaputra, T. Heskes, and P Ouwehand. * State Space Models for Seasonal Aggregation in Sales Forecasting. *Technical report: ICIS-R06015, March, Radboud University Nijmegen, 2006.

This paper describes a way to improve forecasts by simultaneously forecasting a group of products that exhibit a similar seasonal pattern. There have already been several previous publications that demonstrated forecast improvements using seasonal aggregation. However, these papers focused on various ad hoc methods to combine seasonal indices from aggregated time series. Instead, we develop state space models in which aggregation is naturally incorporated. Our primary contribution is the seasonal aggregation extension of the Harvey

B. Gebremichael, F.W. Vaandrager, and M. Zhang. * Analysis of a Protocol for Dynamic Configuration of IPv4 Link Local Addresses using Uppaal. *Technical report: ICIS-R06016, June, Radboud University Nijmegen, 2006.

Formal methods have been applied frequently to analyze (critical parts of) standards for communication protocols and it has been demonstrated that their application may help to improve the quality of these standards. Nevertheless, despite several decades of formal methods research, formal methods notations have rarely been included in the authoritative part of protocol standards. Also, the relationships between (abstract) formal models and informal protocol standards are typically obscure. It is our ambition to improve this situation. To establish the current state-of-the-art, we report in this paper on a case study where we use Uppaal to formally model parts of Zeroconf, a protocol for dynamic configuration of IPv4 link-local addresses that is defined in RFC 3927 of the IETF. Our goal has been to construct a model that (a) is easy to understand by engineers, (b) comes as close as possible to the informal text (for each transition in the model there should be a corresponding piece of text in the RFC), and (c) may serve as a basis for formal verification. Our conclusion is that Uppaal, which combines extended finite state machines, C-like syntax and concepts from timed automata theory, is able to model Zeroconf in a faithful and intuitive way, using notations that are familiar to protocol engineers. Our modeling efforts revealed some errors (or at least ambiguities) in the RFC that no one else spotted before. We also identify a number of points where Uppaal still can be improved. After applying a number of abstractions, Uppaal is able to fully explore the state space of an instance of our model with three hosts, and to establish some correctness properties.

F.W. Vaandrager. * Does it Pay Off? Model-Based Verification and Validation of Embedded Systems!. *Technical report: ICIS-R06019, July, 2006.

An overview is presented of the state-of-the-art in model-based verification and validation of embedded systems, directed towards an industrial audience. Verification and validation consists in exploring the current design against side properties expressed as part of the requirements. It includes testing, model checking, runtime verification and fault-diagnosis, and more exploratory techniques such as the use of theorem proving. During recent years, much progress has been made in theory, methods and tools for model-based verification and validation. In this paper, I will try to indicate for what type of practical problems it pays off to apply one of these modern techniques. Special attention will be paid to the results of six PROGRESS projects in this area.

S.J. Overbeek. * A Research Methodology for Supporting the Development of a Personal Digital Workspace for Knowledge Workers. *Technical report: ICIS-R06020, April, Radboud University Nijmegen, 2006.

Present day knowledge workers interact with a digital world which is full of digital services intended to support these workers in their knowledge intensive tasks. Digital services include the use of applications in general, tools that support knowledge generation, or knowledge transfer, but may also support the proliferation of knowledge in order to improve organizational decision making and value addition. However, it often occurs that contemporary digital services are not user-friendly, impersonal, and ambiguous in use. Therefore, my Ph.D. research focuses on the notion of ‘Sophia’: a reference model and a development framework for a personal digital workspace for knowledge workers. A personal digital workspace for knowledge workers aims to integrate and personalize all digital services, digital information items, and digital knowledge items, so that an individual knowledge worker can carry out his work related activities pleasantly, effectively, and efficiently in every physical, social and digital context.

E.D. Schabell. * ABout Time Linux - the requirements. *Technical report: ICIS-R06021, May, Radboud University Nijmegen, 2006.

This document will detail a project that has risen from the desire to create a generic framework for managing the software on a Linux system. It is based on my experiences while working as a developer on a sourcebased Linux distribution spanning more than three years at the time of this writing. I hope to take my experiences as a developer and package maintainer to create this new package manager. I follow in the footsteps of a few pretty good existing projects such as (micropkg, 2004), (Easinstaller, 2004) and (SMGL, 2004), though I have found these to be lacking in some way or another.

Th.P. van der Weide, and P. van Bommel. * GAM: A Generic Model for Adaptive Personalisation. *Technical report: ICIS-R06022, June, Radboud University Nijmegen, 2006.

In this paper we formally define the Generic Adaptivity Model (GAM). This model provides a strong theoretical foundation for adaptive personalisation. Staying true to existing approaches in user modelling, the GAM can be used descriptively as well as prescriptively. The GAM consists of a number of pillars bound together by a common foundation. In order to allow for extensibility the GAM is domain independent and has little restrictions in applicability. The GAM is embedded in a method for the design of adaptation models for new as well as legacy systems.

J. Berendsen, David N. Jansen, and Joost-Pieter Katoen. * Probably on Time and within Budget: On Reachability in Priced
Probabilistic Timed Automata . *Technical report: ICIS-R06023, August, 2006.

This paper presents an algorithm for cost-bounded probabilistic reachability in timed automata extended with prices (on edges and locations) and discrete probabilistic branching. The algorithm determines whether the probability to reach a (set of) goal location(s) within a given price bound (and time bound) can exceed a threshold p in [0, 1]. We prove that the algorithm is partially correct and show an example for which termination cannot be guaranteed.

Ildiko Flesch, and P.J.F. Lucas. * Graphical Reasoning with Bayesian Networks. *Technical report: ICIS-R06024, September, Radboud University Nijmegen, 2006.

Nowadays, Bayesian networks are seen by many researchers as standard tools for reasoning with uncertainty. Despite the fact that Bayesian networks are graphical representations, representing dependence and independence information, normally the emphasis of the visualisation of the reasoning process is on showing changes in the associated marginal probability distributions due to entering observations, rather than on changes in the associated graph structure. In this paper, we argue that it is possible and relevant to look at Bayesian network reasoning as reasoning with a graph structure, depicting changes in the dependence and independence information. We propose a new method that is able to modify the graphical part of a Bayesian network to bring it in accordance with available observations. In this way, Bayesian network reasoning is seen as reasoning about changing dependences and independences as reflected by changes in the graph structure.

Ildiko Flesch, P.J.F. Lucas, and Stefan Visscher. * On the modularisation of independence in dynamic Bayesian networks. *Technical report: ICIS-R06025, September, Radboud University Nijmegen, 2006.

Dynamic Bayesian networks are Bayesian networks which explicitly incorporating the dimension of time. They are distinguished into repetitive and non-repetitive networks. Repetitive networks have the same set of random (statistical) variables and independence relations at each time step, whereas in non-repetitive networks the set of random variables and the independence relations between these random variables may vary in time. Due to their structural symmetry, repetitive networks are easier to use and are, therefore, often considered as the standard dynamic Bayesian networks. However, repetitiveness is a very strong assumption, which usually does not hold, because dependences and independences that only hold at certain time steps may be lost. In this paper, we propose a new framework for the modularisation of non-repetitive dynamic Bayesian networks, which offers a practical approach to coping with the computational and structural difficulties associated with unrestricted dynamic Bayesian networks. This framework is based on separating temporal and atemporal independence relations in the model. We investigate properties of the modularisation and show to be compositive.

S.J. Overbeek, P. van Bommel, H.A. (Erik) Proper, and D.B.B. Rijsenbrij. * Foundations and Applications of Intelligent Knowledge Exchange. *Technical report: ICIS-R06026, October, Radboud University Nijmegen, 2006.

Exchange of knowledge is becoming increasingly important to modern organizations. In this chapter is explained what this elementary knowledge exchange consists of and how a virtual workplace can support knowledge exchange between workers. A scenario from the medical domain illustrates how physicians can improve their knowledge exchange by utilizing the virtual workplace models introduced. Better adaptation to the rapidly changing nature of providing health care is a desirable effect of improved knowledge exchange between physicians. Explicit models concerning possible physical, social and digital contexts of knowledge exchange are discussed, as well as models which depict how knowledge relatedness enable intelligent knowledge exchange. Researchers studying virtual workplace models for industry and academic purposes belong to the intended audience of this chapter. Administrators of public sector or other non-profit agencies who wish to incorporate virtual workplace models and methods into their daily operations can also benefit from the contents discussed.

P. R. D`Argenio, and B. Gebremichael. * Axiomatizing timed automata with deadlines. *Technical report: ICIS-R06027, October, Radboud University Nijmegen, 2006.

It is known that the usual timed bisimulation fails to be a congruence for timed automata with deadlines - a variant of timed automata where component synchronization is delayable, and time progress is controlled by deadlines on transitions instead of invariants on locations. Recently, we found the coarsest congruence relation that is included in timed bisimulation for timed automata with deadlines. In the present paper we provide an algebraic proof system for direct derivation of such relation by syntactic manipulation. We establish that the proof system is sound and complete.

B. van Gils, and H.A. (Erik) Proper. * Fundamentals of Quality on the Web. *Technical report: ICIS-R06029, June, 2006.

We use information from the Web for performing our daily tasks more and more often. Locating the right resources that help us in doing so is a daunting task, especially with the present rate of growth of the Web as well as the many different kinds of resources available. The tasks of search engines is to assist us in finding those resources that are apt for our given tasks; search engines assess the quality of resources for players. In this paper we present a formal model for the notion of quality on the Web. We base our model on a thorough literature study of how the quality notion is used in different fields. Even more, we show how the quality of resources is affected by software manipulations (transformations).

E.D. Schabell. * Touring the ICIS Publication Management System (PMS v1.2). *Technical report: ICIS-R06031, November, Radboud University Nijmegen, 2006, Sources can also be found in CodeYard project repo..

The Publication Management System (PMS) was initially developed and deployed for usage by the IRIS department within the Radboud University Nijmegen. It was born from a wish to provide extensive services in managing and reporting our publications. This paper takes the reader through a tour of the current version of PMS, from the basic services available to any user, on to specific functionality for our institutes members, through the API and finally leaves the reader with some examples of how to use the more advanced features PMS provides.

M.A.J. van Gerven. * Efficient Bayesian Inference by Factorizing Conditional Probability Distributions. *Technical report: ICIS-R06032, November, Radboud University Nijmegen, 2006.

Bayesian inference becomes more efficient when one makes use of the structure that is contained in the potentials that together constitute a joint probability distribution. Such structure can be represented in the form of probability trees or Boolean polynomials. However, in order to make use of such representations in Bayesian inference, one needs to be able to represent it compactly within the inference engine. Recently, it was shown that potentials that exhibit functional dependence can be factorized efficiently by means of the introduction of hidden variables. Here we demonstrate how these techniques can be applied to represent arbitrary potentials compactly thus improving the efficiency of Bayesian inference for models with arbitrary potentials.

M.A.J. van Gerven, and B.G. Taal. * Structure and Parameters of a Bayesian Network for Carcinoid Prognosis. *Technical report: ICIS-R06033, November, Radboud University Nijmegen, 2006.

In this report, we describe the structure and parameters of a Bayesian network for prognosis of patients that present with carcinoid tumors. The report acts as a reference guide to the carcinoid model, which has been developed in collaboration with an expert physician at the Netherlands Cancer Institute.

Jozef Hooman, Hillel Kugler, Iulian Ober, Anjelika Votintseva, and Yuri Yushtein. * Supporting UML-based Development of Embedded Systems by Formal Techniques. *Technical report: ICIS-R06034, November, Radboud University Nijmegen, 2006.

We describe an approach to support UML-based development of embedded systems by formal techniques. A subset of UML is extended with timing annotations and given a formal semantics. UML models are translated, via XMI, to the input format of formal tools, to allow timed and non-timed model checking and interactive theorem proving. Moreover, the Play-Engine tool is used to execute and analyze requirements by means of live sequence charts. We apply the approach to a part of an industrial case study, the MARS system, and report about the experiences, results and conclusions.

Mohamed Layouni, Jozef Hooman, and Sofiene Tahar. * Formal Specification and Verification of the Intrusion-Tolerant Encalves Protocol. *Technical report: ICIS-R06035, November, Radboud University Nijmegen, 2006.

We demonstrate the application of formal methods to the verification of intrusion-tolerant agreement protocols that have a distributed leadership and can tolerate Byzantine faults. As an interesting case study, the Enclaves group-membership protocol has been verified using two techniques: model checking and theorem proving. We use the model checker Murphi to prove the correctness of authentication, and the interactive theorem prover PVS to formally specify and verify Byzantine agreement, termination of agreement, and integrity.

J. Nabukenya, P. van Bommel, and H.A. (Erik) Proper. * Collaborative policy-making processes. *Technical report: ICIS-R06036, December, Radboud University Nijmegen, 2006.

This paper is concerned with the application of collaboration engineering to improve the quality of policy-making processes. Policies are needed to guide complex decision-making. The creation of such policies is a collaborative process. The quality of this collaboration has a profound impact on the quality of the resulting policies and the acceptance by its stakeholders. We therefore focus on the use of techniques and methods from the field of collaboration engineering to improve the quality. We present the results of two case studies conducted on the use of collaboration engineering in the context of the policy making processes. This result also involves a generic design of a policy making process in terms of elementary constructs from collaboration engineering, which has been arrived at using the emph{action research} approach. Before presenting these case studies, however, some theoretical background on policy-making processes and collaboration engineering is provided.

J. Tretmans. * Model Based Testing with Labelled Transition Systems. *Technical report: ICIS-R06037, December, Radboud University Nijmegen, 2006.

Model based testing is one of the promising technologies to meet the challenges imposed on software testing. In model based testing an implementation under test is tested for compliance with a model that describes the required behaviour of the implementation. This tutorial paper describes a model based testing theory where models are expressed as labelled transition systems, and compliance is defined with the â€˜iocoâ€™ implementation relation. The ioco-testing theory, on the one hand, provides a sound and well-defined foundation for labelled transition system testing, having its roots in the theoretical area of testing equivalences and refusal testing. On the other hand, it has proved to be a practical basis for several model based test generation tools and applications. Definitions, underlying assumptions, an algorithm, properties, and several examples of the ioco-testing theory are discussed, involving specifications, implementations, tests, the ioco implementation relation and some of its variants, a test generation algorithm, and the soundness and exhaustiveness of this algorithm.

J. Nabukenya, G.-J. de Vreede, and H.A. (Erik) Proper. * Research Methods for Collaboration Engineering: An Assessment of Applicability Using Collaborative Policy-Making Example. *Technical report: ICIS-R07010, November, Radboud University Nijmegen, 2006.

Collaboration Engineering (CE) is a new field of research and practice which involves the design of recurring collaboration processes that are meant to cause predictable and success among organizationsâ€™ recurring mission-critical collaborative tasks. To measure the effectiveness of CE research efforts, we would need to use a research methodology. This article therefore provides an overview of selected research methods, and an assessment of their applicability to CE research using collaborative organizational policy-making processes as the primary example. This article also presents examples of research questions that can be answered in the CE research using the respective research methods.