Leonard Lensink, Sjaak Smetsers, and Marko van Eekelen. A Proof Framework for Concurrent Programs. Technical report: ICIS-R12001, January, Radboud University Nijmegen, 2012.
This paper presents a proof framework for verifying concurrent programs that communicate using global variables. The approach is geared towards verification of models that have an unbounded state size and are as close to the original code as possible. The bakery algorithm is used as a demonstration of the framework basics, while the (full) framework with thread synchronization was used to verify and correct the reentrant readers writers algorithm as used in the Qt library.
David N. Jansen, Flemming Nielson, and Lijun Zhang. Belief bisimulation for hidden Markov models: logical characterisation and decision algorithm. Technical report: ICIS-R12002, February, Radboud University Nijmegen, 2012.
This paper establishes connections between logical equivalences and bisimulation relations for hidden Markov models (HMM). Both standard and belief state bisimulations are considered. We also present decision algorithms for the bisimilarities. For standard bisimilarity, an extension of the usual partition refinement algorithm is enough. Belief bisimilarity, being a relation on the continuous space of belief states, cannot be described directly. Instead, we show how to generate a linear equation system in time cubic in the number of states.
Arjan Lamers, and Marko van Eekelen. Analyzing Isoefficiency of Partition Local Algorithms. Technical report: ICIS-R12003, February, Radboud University Nijmegen, 2012.
For network applications scalable performance is paramount. NoSQL database systems provide us with a tool to achieve scalable systems. In practice, scalability of performance can depend heavily upon the way of partitioning of the data models. To help making these engineering considerations we develop a first step towards a performance model that will incorporate the effects of partitioning. With this basic model we study the scalability properties of algorithms on sets of processors, each with its own statically assigned local part of a given data set. Within this model we calculate the isoefficiency of a special class of algorithms, partition local algorithms (that can run fully within a single partition). We study different algorithm complexity classes and show the validity of our results using a simulator.
Marija Bjekovic. ArchiMetal case study. Technical report: ICIS-R12004, May, Radboud University Nijmegen, 2012, Technical Note.
Enterprise architecture (EA) is defined as a coherent whole of principles, methods, and models that are used in design and realisation of an enterpriseā??s organisational structure, business processes, information systems, and infrastructure. This study illustrates the usefulness of EA instruments, in particular ArchiMate 1.0 modelling language, for the analysis and transformation of a fictitious company from metallurgic industry named ArchiMetal.
Attila Gobi, Olha Shkaravska, and Marko van Eekelen. A higher-order size system for a higher-order functional language. Technical report: ICIS-R12005, July, Radboud University Nijmegen, 2012.
The authors present a higher-order size type system for a higher-order functional language. A condition for decidability of type checking is given.
S. Michels, M. Velikova, A.J. Hommersom, and P.J.F. Lucas. A Probabilistic Logic-based Model for Fusing Attribute Information of Objects Under Surveillance. Technical report: ICIS-R12006, December, Radboud University Nijmegen, 2012.
The goal of surveillance is to detect or predict certain events, like accidents or illegal activities, by continuously monitoring the position and behaviour of objects of interest. The monitoring requires the collection of information from various and heterogeneous sources. The sheer amount of information leads to information overload of human operators. Additionally, for humans it is very hard to reason about uncertain information in a consistent, unbiased way. We developed a framework to fuse information about intrinsic properties and intentions of objects under surveillance to support human surveillance operators. The framework is based on a probabilistic logic. We show how our approach can be applied to build a model for maritime surveillance by adding domain specific knowledge to the general framework and experimentally show that our model can correct for errors in information transmitted by simulated vessels by fusing this information with information from other sources. To our knowledge this is one of the very few real-world applications of probabilistic logics in a real-world setting.
Martijn Hendriks, and F.W. Vaandrager. Reconstructing Critical Paths from Execution Traces. Technical report: ICIS-R12007, December, Radboud University Nijmegen, 2012.
We consider the problem of constructing critical paths from incomplete information. In general, a directed acyclic graph of tasks with their execution times (i.e., a task graph) is necessary to extract critical paths. We assume, however, that only the set of tasks, and their start and end times are known, e.g., an execution trace in the form of a Gantt chart. This information can be extracted from real machines or from the output of analysis tools, whereas extraction of the exact task graph often is problematic due to imperative modeling formalisms and complicated platform semantics (resource allocation, varying execution speeds). We show that, based on start and end times only, an over-approximation of the critical paths of an unknown task graph can be extracted nevertheless. Furthermore, this approach is generalized to deal with ``noisy`` execution traces of real machines in which control overhead is present. Finally, we discuss various methods to deal with false positives, and apply our approach to a complex industrial case study.