A.J.J. van Breemen, J.J. Sarbo and Th.P. van der Weide. Toward a theory of natural conceptualization. Technical report: ICIS-R07002, January, Radboud University Nijmegen, 2007.
The focus of this paper is on the early phases of ER-modeling consisting of the primary conceptualization of the underlying application domain. To this end we introduce a process model for the generation of meaningful concepts for a domain description. In virtue of its close relation with cognitive activity, this process model also enables the modeler as well as the user to comprehend the concepts of the resulting domain in a natural way. Beyond this goal, natural conceptualization opens the possibility for the introduction of a uniform representation enabling the efficient combination of knowledge obtained from different stake holders during a modeling process.
A.J.J. van Breemen, and J.J. Sarbo. Sign Processes and the Sheets of Semeiosis. Technical report: ICIS-R07003, January, Radboud University Nijmegen, 2007.
After positioning our work in the field of information systems science, we will introduce the basic Peircean semiotic terms pertinent to sign analysis (sign aspects) and those pertinent to interpretation processes (interpretant aspects). Next we will match the sign aspects with the interpretant aspects in order to be able to derive our semiotic process model of cognitive activity. In order to derive the process model we will introduce the concept of a semiotic sheet. This paper is of interest to those engaged in semiotically oriented approaches to information systems and those interested in the Peircean theory of interpretants alike.
O. Shkaravska, R. van Kesteren, and M.C.J.D. van Eekelen. Type Checking and Weak Type Inference for Polynomial Size Analysis of First-Order Functions. Technical report: ICIS-R07004, January, Radboud University Nijmegen, 2007.
We present a size-aware type system for first-order shapely functions. Here, a function is called shapely when the size of the result is determined exactly by a polynomial in the sizes of the arguments. Examples of shapely functions are matrix multiplication and the Cartesian product of two lists. The type checking problem for the type system is shown to be undecidable in general. We define a natural syntactic restriction such that the type checking becomes decidable, even though size polynomials are not necessarily linear. Furthermore, an algorithm for weak type inference for this system is given.
S.J. Overbeek, P. van Bommel, H.A. (Erik) Proper, and D.B.B. Rijsenbrij. Characterizing Knowledge Intensive Tasks indicating Cognitive Requirements - Scenarios in Methods for Specific Tasks. Technical report: ICIS-R07005, February, 2007.
Methods for specific tasks include conceptual modelling in the context of information systems and requirements engineering in software development. Such methods dictate a specific way of working by describing necessary knowledge intensive tasks to fulfil while applying the method. An actor that is applying a method for specific tasks wishes to reach the goals following from the way of working. An actor may experience difficulties when trying to fulfil tasks as part of a method, related to the cognitive abilities required to fulfil a certain task versus the specific cognitive abilities possessed by the actor. This paper focusses on the cognitive abilities required to fulfil a knowledge intensive task while applying a method for specific tasks. This is based on a categorization and characterization of knowledge intensive tasks and scenarios in conceptual modelling of information systems and requirements engineering.
G.J.N.M. (Guido) Chorus, Y.H.C. (Yves) Janse, S.J.B.A. (Stijn) Hoppenbrouwers, C.J.P. (Chris) Nellen, and H.A. (Erik) Proper. Formalizing Architecture Principles using Object-Role Modelling. Technical report: ICIS-R07006, February, 2007.
This technical report is the result of two experiments conducted as part of an ongoing research effort to formalize architecture principles. The experiment involves a first, and modest, evaluation of the use of ORM and ORC as a means to formalize and ground architecture principles. The experiments involve the evaluation of the use of ORM and ORC to formalize the example principles provided by the TOGAF (The Open Group Architecture Framework) and principles taken from industrial practice.
P. van Bommel, S.J.B.A. (Stijn) Hoppenbrouwers, and H.A. (Erik) Proper. QoMo: A Modelling Process Quality Framework based on SEQUAL. Technical report: ICIS-R07007, March, Radboud University Nijmegen, 2007.
This paper aims to contribute to the area of conceptual model quality assessment and improvement. We present a preliminary modelling processoriented quality framework (‘QoMo’), mainly based on the established SEQUAL framework for quality of models. QoMo is based on knowledge state transitions, cost of the activities bringing such transitions about, and a goal structure for activities-for-modelling. Such goals are directly linked to concepts of SEQUAL. We discuss how goals for modelling can be linked to a rule-based way of describing processes for modelling. Such process descriptions hinge on strategy descriptions, which may be used descriptively (for studying/analysing real instances of processes) as well as prescriptively (for the guiding of modelling processes). Descriptive utility of the framework is primary for the quality/evaluation angle on processes-for-modelling, and reflects the main intended contribution of this paper.
E.D. Schabell. Taking a peek inside the cmlFramework. Technical report: ICIS-R07008, March, Radboud University Nijmegen, 2007.
This paper will walk you through a demonstration run of the Collaborative Modeling Lab (CML) Framework prototype. This will start with a conceptual overview of the component structure. The reader will then be walked through a processing run in which a Niam Normal Form (NNF) grammar is used to Filter a Logbook, produce a Contract, Distill this into an Essence, and finally using the Builder to generate an eventual Model in ORM.
C. Haack, E. Poll, J. Schafer, and A. Schubert. Immutable Objects for a Java-like Language. Technical report: ICIS-R07009, April, Radboud University Nijmegen, 2007.
We extend a Java-like language with immutability specifications and a static type system for verifying immutability. A class modifier immutable specifies that all class instances are immutable objects. Ownership types specify the depth of object states and enforce encapsulation of representation objects. The type system guarantees that the state of immutable objects does not visibly mutate during a program run. Provided immutability-annotated classes and methods are final, this is true even if immutable classes are composed with untrusted classes that follow Java
M.A.J. van Gerven. Tensor Decompositions for Probabilistic Classification. Technical report: ICIS-R07011, May, Radboud University Nijmegen, 2007, Longer version of a short paper presented at IDAMAP 2007.
Tensor decompositions are introduced as a novel approach to probabilistic classification and can be interpreted as a particular kind of mixture model. Since many problems in medicine and biology can be described as a classification problem, the approach is seen as a useful tool for biomedical data analysis. The approach is validated by means of a clinical database consisting of data about 1002 patients that suffer from hepatic disease. It is shown that the approach performs comparably to state-of-the-art results that have been obtained using a naive Bayes classifier.
Maarten de Mol, M.C.J.D. van Eekelen, and Rinus Plasmeijer. Confluent Term-Graph Reduction for Computer-Aided Formal Reasoning. Technical report: ICIS-R07012, May, Radboud University Nijmegen, 2007.
Sparkle is the dedicated proof assistant for the lazy functional programming language Clean, which is based on term-graph rewriting. Because equational reasoning is an important proof technique, Sparkle needs to offer support for formally proving e1 = e2 in as many situations as possible. The base proof of equality is by means of reduction: if e1 reduces to e2, then also e1 = e2. Therefore, the underlying reduction system of Sparkle needs to be geared towards flexibility, allowing reduction to take place as often as possible. In this paper, we will define a flexible term-graph reduction system for a simplified lazy functional language. Our system leaves the choice of redex free and uses single-step reduction. It is therefore more suited for formal reasoning than the well-established standard reduction systems for lazy functional languages, which usually fix a single redex and/or realize multi-step reduction only. We will show that our system is correct with respect to the standard systems, by proving that it is confluent and allows standard lazy functional evaluation as a possible reduction path. Our reduction system is used in the foundation of Sparkle. Because it is based on a simplified functional language, it can be applied to any other functional language based on term-graph rewriting as well.
M.C.J.D. van Eekelen, Stefan ten Hoedt, Rene Schreurs, and Yaroslav Usenko. Modeling and verifying a Real-Life Industrial Session-Layer Protocol in mCRL2. Technical report: ICIS-R07014, June, Radboud University Nijmegen, 2007.
This report describes the analysis of an industrial implementation of the session-layer of a load-balancing software system. This software comprises 7.5 thousand lines of C code. It is used for distribution of the print jobs among several document processors (workers). A large part of this commercially used software system has been modeled closely and analyzed using process-algebraic techniques. Several critical issues were discovered. Since the model was close to the code, all problems that were found in the model, could be traced back to the actual code resulting in concrete suggestions for improvement of the code. All in all, the analysis significantly improved the quality of this real-life system.
Hendrik Tews. Proceedings of the C/C++ Verification workshop. Technical report: ICIS-R07015, June, Radboud University Nijmegen, 2007.
This report contains the proceedings of the first C/C++ Verification Workshop held in Oxford on July 2nd, 2007 as a side event of IFM 2007.
M. Gromov, and T.A.C. Willemse. Testing and Model-Checking Techniques for Diagnosis. Technical report: ICIS-R07016, June, Radboud University Nijmegen, 2007.
Black-box testing is a popular technique for assessing the quality of a system. However, in case of a test failure, only little information is available to identify the root-cause of the test failure. In such cases, additional diagnostic tests may help. We present techniques and a methodology for efficiently conducting diagnostic tests based on explicit fault models. For this, we rely on Model-Based Testing techniques for Labelled Transition Systems. Our techniques rely on, and exploit differences in outputs (or inputs) in fault models, respectively. We characterise the underlying concepts for our techniques both in terms of mathematics and in terms of the modal mu-calculus, which is a powerful temporal logic. The latter characterisations permit the use of efficient, off-the-shelf model checking techniques, leading to provably correct algorithms and pseudo decision procedures for diagnostic testing.
J. Nabukenya, P. van Bommel, H.A. (Erik) Proper, and G.-J. de Vreede. An Evaluation Instrument for Collaborative Processes: Application to Organizational Policy-Making . Technical report: ICIS-R07017, July, Radboud University Nijmegen, 2007.
Decision-making in organizations is guided by policies. Organizational policy-making is a complex process in which several parties are involved, with multiple backgrounds, incompatible interests, and diverging areas of interest, yet they all have to be brought together to produce an acceptable policy result. Therefore, we propose to use techniques from collaboration engineering (CE) in this context. There is hardly any experience with CE in the field of organizational policy-making. In order to evaluate the effectiveness and efficiency of CE in organizational policy-making, it is important to have a systematic evaluation instrument. We distinguish between general and domain-specific indicators. Moreover, we consider measurement means and operationalization tools, such that organizational policy-making stakeholders can apply our instrument in their own organization.
J. Nabukenya, P. van Bommel, and H.A. (Erik) Proper. Repeatable Collaboration Processes for Mature Organizational Policy Making. Technical report: ICIS-R07019, July, Radboud University Nijmegen, 2007.
Organizational policy making processes are complex processes in which many people are involved. Very often the results of these processes are not what the different stakeholders intended. Since policies play a major role in key decision making concerning the future of organizations, our research aims at improving the policies on the basis of cooperation. In order to achieve this goal, we apply the practice of collaboration engineering to the field of organizational policy making. We use the thinklet as a basic building block for facilitating intervention to create a repeatable pattern of collaboration among people working together towards achieving a goal. Our case studies show that policy making processes do need collaboration support indeed and that the resulting policies can be expected to improve.
Wolter Pieters, and Robert van Haren. E-voting discourses in the UK and the Netherlands. Technical report: ICIS-R07020, August, Radboud University Nijmegen, 2007.
A qualitative case study of the e-voting discourses in the UK and the Netherlands was performed based on the theory of strategic niche management. In both countries, eight e-voting experts were interviewed on their expectations, risk estimations, cooperation and learning experiences. The results show that differences in these variables can partly explain the variations in the embedding of e-voting in the two countries, from a qualitative point of view.
Christian Haack, Marieke Huisman, Joe Kiniry, and Erik Poll. Proceedings of the Workshop on Verification and Analysis of Multi-threaded Java-like Programs. Technical report: ICIS-R07021, August, Radboud University Nijmegen, 2007.
This report contains the proceedings of the first Workshop on Verification and Analysis of Multi-threaded Java-like Programs (VAMP), held on September 3, 2007, as a satellite event to CONCUR in Lisbon, Portugal.
P. van Bommel, H.A. (Erik) Proper, and Th.P. van der Weide. Structured Modeling with uncertainty. Technical report: ICIS-R07022, September, Radboud University Nijmegen, 2007.
This paper starts with the description of the modeling process as a dialog, and describes the associated formal functions, including the feedback supporting the growing mutual understanding. The dialog has a procedural and an informational aspect. For this latter a controlled grammar is used, that has a user friendly and a system friendly side. These sides are related via an elementary syntactical transformation. Assuming some elementary requirements on the dialog participants, we prove the main theorem for information modeling effectiveness. We also propose a system of metrics to support the modeling process. In terms of these metrics, modeling heuristics can be described and evaluated. We demonstrate our ideas by a simple sample session.
M.A.J. van Gerven. Approximate Inference in Graphical Models using Tensor Decompositions. Technical report: ICIS-R07024, November, Radboud University Nijmegen, 2007.
We demonstrate that tensor decompositions can be used to transform graphical models into structurally simpler graphical models that approximate the same joint probability distribution. In this way, standard inference algorithms such as the junction tree algorithm, can be used in order to use the transformed graphical model for approximate inference. The usefulness of the technique is demonstrated by means of its application to thirty randomly generated small-world Markov networks.
Maarten de Mol, M.C.J.D. van Eekelen, and Rinus Plasmeijer. The Mathematical Foundation of the Proof Assistant Sparkle. Technical report: ICIS-R07025, November, Radboud University Nijmegen, 2007.
This report presents the mathematical foundation of the proof assistant SPARKLE, which is dedicated to the lazy functional language CLEAN. The mathematical foundation provides a formalization of the programming, logic and proof languages that are supported by SPARKLE. Furthermore, it formalizes the reduction of programs and the semantics of properties, and provides proofs for the soundness of the defined tactics.
J. Berendsen, and F.W. Vaandrager. Compositional Abstraction in Real-Time Model Checking. Technical report: ICIS-R07027, November, Radboud University Nijmegen, 2007.
The idea to use simulations (or refinements) as a compositional abstraction device is well-known, both in untimed and timed settings, and has already been studied theoretically and practically in many papers during the last three decades. Nevertheless, existing approaches do not handle two fundamental modeling concepts which, for instance, are frequently used in the popular Uppaal model checker: (1) a parallel composition operator that supports communication via shared variables as well as synchronization of actions, and (2) committed locations. In this paper, we describe a framework for compositional abstraction based on simulation relations that does support both concepts, and that is suitable for Uppaal. Our approach is very general and the only essential restriction is that the guards of input transitions do not depend on external variables. We have applied our compositional framework to verify the Zeroconf protocol for an arbitrary number of hosts.
Olha Shkaravska, and M.C.J.D. van Eekelen. Static inference of polynomial size-aware types. Technical report: ICIS-R07028, November, Radboud University Nijmegen, 2007.
We propose a static size analysis procedure that combines term-rewriting and type checking to automatically obtain output-on-input size dependencies for first-order functions. Attention is restricted to functions for which the size of the result is strictly polynomial, not necessarily monotonous, in the sizes of the arguments. To infer a size dependency, the procedure generates hypotheses for increasing degrees of polynomials. For each degree, to define a hypothetical polynomial one needs to know its values on a finite collection of points (subject to some geometrical condition). To compute the value of a size polynomial in a certain point we use a term-rewriting system generated by a standard size-annotations inference procedure. We have proven that if a function with a given input terminates at run-time on a meaningful stack and heap then the static (`compile-time`) term rewriting system of the size inference also terminates, on the integers representing the sizes of the corresponding inputs. The term rewriting system may terminate at compile-time when the underlying function definition does not at run-time. This makes the theoretical applicability of the proposed approach larger than the previous state-of-the-art, where run-time testing was used to generate hypothetical polynomials. Also, the practical applicability is improved due to increased efficiency since the term rewriting system at compile time abstracts from many computations that are done at run-time. We give the proof that if a function body terminates on a meaningful stack and heap then term-rewriting terminates on the integers representing the sizes of inputs. Term-rewriting may terminates when the underlying function definition does not. This makes the applicability of the proposed approach larger then its previous version, where we use run-time testing to generate hypothetical polynomials.
Wojciech Mostowski, and Erik Poll. Testing the Java Card Applet Firewall. Technical report: ICIS-R07029, December, Radboud University Nijmegen, 2007.
In this paper we discuss the methodology and results of testing the Java Card applet firewall mechanism. The main motivation for this work is the complexity of the firewall. Given the complexity, non-compliance of the cards with respect to the official specification is not unlikely. Firewall implementation faults may lead to serious security issues. Although we did not discover any serious problems on our test cards, a few minor specification violations are reported. We only found one specification violation on one card that could be considered unsafe, in that it might introduce a security risk for specific applications.
Ed Brinksma, and Jozef Hooman. Dependability for high-tech systems: an industry-as-laboratory approach. Technical report: ICIS-R07030, December, Radboud University Nijmegen, 2007.
The dependability of high-volume embedded systems, such a consumer electronic devices, is threatened by a combination of quickly increasing complexity, decreasing time-to-market, and strong cost constraints. This poses challenging research questions that are investigated in the Trader project, following the industry-as-lab approach. We present the main vision of this project, which is based on a model-based control paradigm, and the current status of the project results.
R. Hamberg, and F.W. Vaandrager. Using Model Checkers in an Introductory Course on Operating Systems. Technical report: ICIS-R07031, December, Radboud University Nijmegen, 2007.
During the last three years, we have been experimenting with the use of the Uppaal model checker in an introductory course on operating systems for first-year Computer Science students at the Radboud University Nijmegen. The course uses model checkers as a tool to explain, visualize and solve concurrency problems. Our experience is that students enjoy to play with model checkers because it makes concurrency issues tangible. Even though it is hard to measure objectively, we think that model checkers really help students to obtain a deeper insight into concurrency. In this article, we report on our experiences in the classroom, explain how mutual exclusion algorithms, semaphores and monitors can conveniently be modeled in Uppaal, and present some results on properties of small, concurrent patterns.
J. Berendsen, B. Gebremichael, Miaomiao Zhang, and F.W. Vaandrager. Formal Specification and Analysis of Zeroconf using Uppaal. Technical report: ICIS-R07032, December, Radboud University Nijmegen, 2007.
We report on a case study in which the model checker Uppaal is used to formally model parts of Zeroconf, a protocol for dynamic configuration of IPv4 link-local addresses that has been 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 modeling efforts revealed several errors (or at least ambiguities) in the RFC that no one else spotted before. We present two proofs of the mutual exclusion property for Zeroconf (for an arbitrary number of hosts and IP addresses): a manual, operational proof, and a proof that combines model checking with the application of a new abstraction relation that is compositional with respect to committed locations. The model checking problem has been solved using Uppaal, and the abstractions have been checked either by hand or by using Uppaal-Tiga.