Ron van Kesteren, M.C.J.D. van Eekelen, and Maarten de Mol. Proof Support for General Type Classes. Technical report: ICIS-R05001, January, Radboud University Nijmegen, 2005.
We present a proof rule and an effective tactic for proving properties about Haskell type classes by proving them for the available instance definitions. This is not straightforward, because instance definitions may depend on each other. The proof assistant Isabelle handles this problem for single parameter type classes by structural induction on types. However, this does not suffice for an effective tactic for more complex forms of overloading. We solve this using an induction scheme derived from the instance definitions. The tactic based on this rule is implemented in the proof assistant Sparkle.
Leonard Lensink, and M.C.J.D. van Eekelen. Induction and Co-Induction in Sparkle. Technical report: ICIS-R05002, January, Radboud University Nijmegen, 2005.
Sparkle is a proof assistant designed for the lazy evaluatingfunctional programming language Clean. It is designed with the clearobjective in mind that proofs of first order logical predicates onprograms should be as easy as possible for programmers. Sincerecursion is at the heart of functional languages, support forrecursive reasoning should be as exhaustive as possible. Until nowthe induction tactic in Sparkle was rather basic. We have extendedSparkle with two standard techniques to perform inductive andco-inductive reasoning about programs. By means of examples, we showfrom research papers how they benefit the programmer. Moreimportantly, we propose a new technique to derive induction schemesfor mutually recursive programs by using strongly connectedcomponents of complete call graphs to derive a well founded orderingand induction scheme. These induction schemes can be used tosemi-automatically prove properties of programs out of reach ofother automated proof techniques. Together this extends the realm ofprograms for which easy proofs in Sparkle can be constructed by theprogrammer.
B.P.F. Jacobs. A Bialgebraic Review of Regular Expressions, Deterministic Automata and Languages. Technical report: ICIS-R05003, February, Radboud University Nijmegen, 2005.
This papers reviews the classical theory of deterministic automata and regular languages from a categorical perspective. The basis is formed by Ruttens description of the Brzozowski automaton structure in a coalgebraic framework. We enlarge the framework to a so-called bialgebraic one, by including algebras together with suitable distributive laws connecting the algebraic and coalgebraic structure of regular expressions and languages. This culminates in a reformulated proof via finality of Kozens completeness result. It yields a complete axiomatisation of observational equivalence (bisimilarity) on regular expressions. We suggest that this situation is paradigmatic for (theoretical) computer science as the study of ""generated behaviour.
Ichiro Hasuo, and B.P.F. Jacobs. Context-free Languages via Coalgebraic Trace Semantics. Technical report: ICIS-R05004, January, Radboud University Nijmegen, 2005.
In this paper we identify context-free grammars as coalgebras.To obtainthe associated context-free languages (consisting of only finite-length strings)we introduce a general and novel technique of finite trace semantics forcoalgebras. It builds on top of the (possibly infinite) tracesemantics introduced earlier by the second author, but extracts onlyfinite behavior. Interestingly the finite trace isuniquely characterized corecursively and hence it yields a finalcoalgebra in a suitable Kleisli category, while the ordinary trace is notunique and yields a weakly final coalgebra.Additionally, the constructions of both finite and possibly infinite parsetrees are shown to be monads. Hence our extension of the applicationdomain of coalgebras identifies several new mathematical constructionsand structures.
Ernesto Wandeler, Lothar Thiele, Marcel Verhoef, and Paul Lieverse. System Architecture Evaluation Using Modular Performance Analysis. Technical report: ICIS-R05005, January, Radboud University Nijmegen, 2005.
Performance analysis plays an increasingly important role in the designof embedded real-time systems. Time-to-market pressure in this domain ishigh while the available implementation technology is often pushed to itslimit tominimize cost. This requires analysis of performance as early as possible inthesystem life cycle. Simulation based techniques are often not sufficientlyproductive.This paper presents an alternative, analytical, approach based on Real-TimeCalculus developed at ETH Zurich. Modular Performance Analysis (MPA) ispresented through a case study in which several candidate architectures areevaluatedfor a distributed in-car radio navigation system. The analysis is efficientdueto the high abstraction level of the model, which makes the techniquesuitable forearly design exploration.
S.J.B.A. (Stijn) Hoppenbrouwers, H.A. (Erik) Proper, and Th.P. van der Weide. Fundamental Understanding of the Act of Modelling. Technical report: ICIS-R05006, January, Radboud University Nijmegen, 2005.
In an ongoing effort to better understand the process of creating models (in particular formal ones), we present a fundamental view of the process of modelling. We base this view on the idea that participants in such a process are involved in a deliberate and goal-driven effort to share and reconcile representations of their personal conceptions of (parts of) the world. This effort takes the shape of a modelling dialogue, involving the useof controlled language. We thus take a fundamental approach to subjective aspects of modelling, as opposed to traditional approaches which essentially consider models asobjective entities. We describe our core theory, explain why it is proposed, and briefly discuss how we intend to validate and further develop our theory of modelling.
S. Bosman, and Th.P. van der Weide. Towards formalization of the information modeling dialog. Technical report: ICIS-R05012, Computing Science Institute, University of Nijmegen, 2005.
Abstract: This paper proposes a formalization of the modeling dialog between domain expert and system analyst, in which domain knowledge is specified and refined until a formal conceptual model of a domain results. This formalization is then used to describe the task of the system analyst in two settings. The ultimate goal of this work is to enable computer support for the system analyst in the modeling process.
S.J.B.A. (Stijn) Hoppenbrouwers, Th.P. van der Weide, and H.A. (Erik) Proper. Dealing with Uncertainty in Information Modelling. Technical report: ICIS-R05013, Institute for Information and Computing Sciences, Radboud University, Nijmegen, The Netherlands, EU, 2005.
We present ongoing research concerning a communication-based approach to information modelling. The general goal of our research is to understand and support (contextualized) modelling dialogues rather than the models that result from these dialogues or the modelling languages in which the models are expressed. We take the point of view that information modelling dialogues are subject to the same kinds of uncertainty that occur in any communication between human agents. This uncertainty is for a large part due to the contextualized nature of information models. By focusing on dialogues and guiding them through strategies for dealing with uncertainty, we hope to achieve better, properly contextualized, information models. We present an analysis of uncertainty in information modelling, and give an example of a viable approach to one particular type of uncertainty reduction in information modelling. We work towards a functional design for an interactive modelling environment for testing our theories.
Martijn Hendriks. Model Checking the Time to Reach Agreement. Technical report: ICIS-R05014, February, Radboud University Nijmegen, 2005.
The timed automaton framework of Alur and Dill is a natural choice forthe specification of partially synchronous distributed systems. The pasthas shown, however, that verification of these systems by model checkingusually is very difficult. Therefore, model checking techniques havethus far not really been used for their design, even though thesetechniques are widely used in other areas, e.g., hardware verification.The present paper demonstrates that the revolutionary development ofboth the usability and the efficiency of model checking tools may changethis. It is shown that a complex partially synchronous distributed algorithm can easily be modeled with the Uppaal model checker, and that it is possible to analyze some interesting and non-trivial instances with reasonable computational resources. Clearly, such analysis results can greatly support the design of these systems: model checking tools may provide valuable early feedback on subtle design errors and hint at system invariants that can subsequently be used in the general correctness proof.
P. R. D`Argenio, and B. Gebremichael. The Coarsest Congruence for Timed Automata with Deadlines Contained in Bisimulation. Technical report: ICIS-R05015, March, Radboud University Nijmegen, 2005.
Delaying the synchronisation of actions may reveal some hidden behaviour that would not happen if the synchronisation would meet the specified deadlines. This precise phenomenon makes bisimulation fail to be a congruence for the parallel composition of timed automata with deadlines, a variant of timed automata where time progress is controlled by deadlines imposed on each transition. This problem has been known and unsolved for several years. In this paper we give a characterisation of the coarsest congruence that is included in the bisimulation relation. In addition, a symbolic characterisation of such relation is provided and shown to be decidable. We also discuss the pitfalls of existing parallel compositions in this setting and argue that our definition is both reasonable and sufficiently expressive as to consider the modelling of both soft and hard real-time constraints.
B. Gebremichael, F.W. Vaandrager, and Miaomiao Zhang. Formal Models of Guaranteed and Best-Effort Services for Networks on Chip. Technical report: ICIS-R05016, March, Radboud University Nijmegen, 2005.
Networks on a chip (NoC) are emerging as a scalable, compositional and efficient alternative to existing on-chip interconnects (such as point to point networks or buses). Aethereal is a protocol that has been proposed byPhilips to enable both guaranteed and best effort communication in an on-chip packet switching network. We present a formal specification of the Aethereal protocol and its underlying network. All components of the network and their behavior are specified in detail, using the PVS specification language. Using PVS we prove, for an abstract version of our model, absence of deadlock within the Aethereal protocol.
Ling Cheung, and Martijn Hendriks. Causal Dependencies in Parallel Composition of Stochastic Processes. Technical report: ICIS-R05020, September, Radboud University Nijmegen, 2005.
We present some new perspectives on an old problem: compositionality of trace-style semantics for stochastic processes. The initial step is a more fine-grained analysis of how parallel composition of stochastic processes can be defined in a meaningful way. We make a connection between the notion of adversary models and the formal definitions of stochastic system types and parallel composition operators. In particular, we focus on causal dependencies arising from the so-called strong adversaries and argue that trace-style semantic compositionality cannot be achieved under strong adversaries.We identify a structural feature of stochastic processes called ``invisible probabilistic branching and illustrate its connection with strong adversaries. Based on these observations, we introduce a new system type together with appropriate notions of observable behavior and parallel composition. We prove a finite approximation theorem for behaviors and use that to prove semantic compositionality. Finally, we present a model of the Chor-Israeli-Li consensus protocol in our new framework.
E.D. Schabell, and B. van Gils. Implementing Vimes - the broker component. Technical report: ICIS-R05028, Radboud University Nijmegen, 2005.
This document will discuss the Vimes retrieval architecture broker component from the research project Profile Based Retrieval Of Networked Information Resources (PRONIR). It will provide an overview of the development process from requirements investigations done with use cases, on to the actual design and implementation.
J.J. Sarbo, J.I. Farkas, and A.J.J. van Breemen. Natural Grammar. Technical report: ICIS-R05032, Radboud University, Nijmegen, The Netherlands, EU, 2005.
What is `natural in natural language? Can that property be captured formally in a type of grammar? The promise of this paper is that natural grammar may exist indeed. Our research has revealed additionally that such grammar can be given a naive logical as well as a semiotic interpretation, which are isomorphic, indicating that naive logic and natural language, as different types of knowledge, can have a uniform, semiotically based representation. Natural grammar bears similarity with dependency based formalisms like Link Grammar, its types of rules define an induced triadic classification of language concepts analogous to X-bar theory.
Marcel Verhoef. On the Use of VDM++ for Specifying Real-time Systems. Technical report: ICIS-R05033, October, Radboud University Nijmegen, 2005.
Language extensions have been suggested in the past to make VDM++ better suited for specification of real-time applications and tool support was developed to analyze these extended VDM++ models. Practical experiences with the language extensions and the supporting tools are discussed in this paper. Improvements to the language extensions and tool support are suggested.
Martijn Warnier, and Martijn Oostdijk. Non-interference in JML. Technical report: ICIS-R05034, October, Radboud University Nijmegen, 2005.
This paper deals with the specification of non-interference properties in the behavioral specification language JML. The notion of a specification pattern for JML is introduced and it is shown how such patterns can be used to specify non-interference properties such as confidentiality and integrity. The main contribution of this paper is an algorithm that takes a Java source file as input and generates a source file annotated with specification patterns for confidentiality in JML. The algorithm works for input programs written in a non-trivial subset of sequential Java. We prove that the specifications generated by the algorithm are correct and express confidentiality. In case of loops, the specifications will have to be over-approximations. Fortunately, the generated specifications can easily be refined and combined with existing hand-written JML specifications. The resulting specifications can be verified using any of the JML tools.
Ling Cheung. Randomized Wait-Free Consensus using An Atomicity Assumption. Technical report: ICIS-R05035, November, Radboud University Nijmegen, 2005.
We present a randomized algorithm for asynchronous wait-free consensus using multi-writer multi-reader shared registers. This algorithm is based on earlier work by Chor, Israeli and Li (CIL) and is correct under the assumption that processes can perform a random choice and a write operation in one atomic step. The expected total work for our algorithm is shown to be O(N log(log N)), compared with O(N^2) for the CIL algorithm and O(N log N) for the best weak-adversary algorithm previously known. We also model check instances of our algorithm using the probabilistic model checking tool PRISM.
Egon L. van den Broek, Theo E. Schouten, Peter M. F. Kisters, and Harco Kuppens. Weighted Distance Mapping (WDM). Technical report: ICIS-R05036, Decewmber, Radboud University Nijmegen, 2005.
A new method is introduced for describing, visualizing, and inspecting data spaces. It is based on an adapted version of the Fast Exact Euclidean Distance (FEED) transform. It computes a description of the complete data space based on partial data. Combined with a metric, a true Weighted Distance Map (WDM) can be computed, which can define a probability space. Subsequently, distances between data points can be determined. Using edge detection, borders (or boundaries) between categories (or clusters) of data can be found. Hence, Voronoi diagrams can be created. Moreover, the visualization of such WDMs provides excellent means for data inspection. Several examples illustrate the use of WDMs as well as their efficiency. So, a new, fast, and exact data analysis method has been developed that yields the means for a rich and intuitive method of data inspection.
Eva M. van Rikxoort, Egon L. van den Broek, and Theo E. Schouten. The development of a human-centered object-based image retrieval engine. Technical report: ICIS-R05037, December, Radboud University Nijmegen, 2005.
The development of a new object-based image retrieval(OBIR) engine is discussed. Its goal was to yield intuitive results for users by using human-based techniques. The engine utilizes a unique and efficient set of 15 features: 11 color categories and 4 texture features, derived from the color correlogram. These features were calculated for the center object of the images, which was determined by agglomerative merging. Subsequently, OBIR was applied, using the color and texture features of the center objects on the images. The final OBIR engine, as well as all intermediate versions, were evaluated in a CBIR benchmark, consisting of the engine, the Corel image database, and an interface module. The texture features proved to be useful in combination with the 11 color categories. In general, the engine proved to be generically applicable, be fast and yields intuitive results for users.
Egon L. van den Broek, Eva M. van Rikxoort, and Theo E. Schouten. Human-centered object-based image retrieval. Technical report: ICIS-R05038, December, Radboud University Nijmegen, 2005.
A new object-based image retrieval (OBIR) scheme is introduced. The images are analyzed using the recently developed, human-based 11 colors quantization scheme and the color correlogram. Their output served as input for the image segmentation algorithm: agglomerative merging, which is extended to color images. From the resulting coarse segments, boundaries are extracted by pixelwise classification, which are smoothed by an opening operation. The resulting features of the extracted shapes, completed the data for a