Fides Aarts, Bengt Jonsson, Johan Uijen, and Frits Vaandrager. Generating Models of Infinite-State Communication Protocols using Regular Inference with Abstraction. Technical report: ICIS-R13001, January, Radboud University Nijmegen, 2013.
In order to facilitate model-based verification and validation, effort is underway to develop techniques for generating models of communication system components from observations of their external behavior. Most previous such work has employed regular inference techniques which generate modest-size finite-state models. They typically suppress parameters of messages, although these have a significant impact on control flow in many communication protocols. We present a framework, which adapts regular inference to include data parameters in messages and states for generating components with large or infinite message alphabets. A main idea is to adapt the framework of predicate abstraction, successfully used in formal verification. Since we are in a black-box setting, the abstraction must be supplied externally, using information about how the component manages data parameters. We have implemented our techniques by connecting the LearnLib tool for regular inference with the protocol simulator ns-2, and generated models of SIP and TCP components as implemented in ns-2.
M.M. Bonsangue, H.H. Hansen, A. Kurz, and J. Rot. Presenting Distributive Laws. Technical report: ICIS-R13007, June, Radboud University Nijmegen, 2013.
Distributive laws of a monad T over a functor F are categorical tools for specifying algebra-coalgebra interaction. They proved to be important for solving systems of corecursive equations, for the specification of well-behaved structural operational semantics and, more recently, also for enhancements of the bisimulation proof method. If T is a free monad, then such distributive laws correspond to simple natural transformations. However, when T is not free it can be rather difficult to prove the defining axioms of a distributive law. In this paper we describe how to obtain a distributive law for a monad with an equational presentation from a distributive law for the underlying free monad. We apply this result to show the equivalence between two different representations of context-free languages.
Marko van Eekelen, Rachid Ben Moussa, Engelbert Hubbers, and Roel Verdult. Blackboard Security Assessment. Technical report: ICIS-R13004, April, Radboud University Nijmegen, 2013.
A security assessment is given of the BlackBoard Learn electronic learning environment. As a result of this assessment the board of the Radboud University Nijmegen has decided to stop with summative testing using BlackBoard, to quit using Blackboard Grade Center and to use the Blackboard discussion forum for non-privacy-sensitive topics only.
David N. Jansen. More or less true: DCTL for continuous-time MDPs. Technical report: ICIS-R13006, June, Radboud University Nijmegen, 2013.
Discounted Computation Tree Logic is a logic that measures utility (as a real value in the interval [0,1]) instead of discrete truth (only 0 or 1). It is able to express properties that give more weight to the near future than to the far future. This article extends earlier work on DCTL with time, to continuous-time Markov chains and continuous-time Markov decision processes. It presents model checking algorithms for the two possible semantics of DCTL.
This technical report is an extended version of a FORMATS 2013 publication.
David N. Jansen, Lei Song, and Lijun Zhang. Revisiting Weak Simulation for Substochastic Markov Chains. Technical report: ICIS-R13005, May, Radboud University Nijmegen, 2013.
The spectrum of branching-time relations for probabilistic systems has been investigated thoroughly by Baier, Hermanns, Katoen and Wolf (2003, 2005), including weak simulation for systems involving substochastic distributions. Weak simulation was proven to be sound w. r. t. the liveness fragment of the logic PCTL\X, and its completeness was conjectured. We revisit this result and show that soundness does not hold in general, but only for Markov chains without divergence. It is refuted for some systems with substochastic distributions. Moreover, we provide a counterexample to completeness. In this paper, we present a novel definition that is sound for live PCTL\X, and a variant that is both sound and complete.
This technical report is an extended version of a QEST 2013 conference publication.
Sebastiaan J.C. Joosten, and Hans Zantema. Relaxation of 3-partition instances. Technical report: ICIS-R13002, February, Radboud University Nijmegen, 2013.
The 3-partition problem admits a straightforward formulation as a 0-1 Integer Linear Program (ILP). We investigate problem instances for which the half-integer relaxation of the ILP is feasible, while the ILP is not. We prove that this only occurs on a set of at least 18 elements, and in case of 18 elements such an instance always contains an element of weight ‚?• 10. These bounds are sharp: we give all 14 instances consisting of 18 elements all having weight ‚?§ 10. Our approach is based on analyzing an underlying graph structure.
Ken Madlener, Sjaak Smetsers, and Marko van Eekelen. Modular Bialgebraic Semantics and Algebraic Laws. Technical report: ICIS-R13008, July, Radboud University Nijmegen, 2013.
The ability to independently describe operational rules is indispensable for a modular description of programming languages. This paper introduces a format for open-ended rules and proves that conservatively adding new rules results in well-behaved translations between the models of the operational semantics. Silent transitions in our operational model are truly unobservable, which enables one to prove the validity of algebraic laws between programs. We also show that algebraic laws are preserved by extensions of the language and that they are substitutive. The work presented in this paper is developed within the framework of bialgebraic semantics.
Ammar Osaiweran, Mathijs Schuts, Jozef Hooman, and Jacco Wesselius. Incorporating Formal Techniques into Industrial Practice: an Experience Report. Technical report: ICIS-R13003, March, Radboud University Nijmegen, 2013.
We report about experiences at Philips Healthcare with component-based development supported by formal techniques. The formal Analytical Software Design (ASD) approach of the company Verum has been incorporated into the industrial workflow. The commercial tool ASD:Suite supports both compositional verification and code generation for control components. For other components test-driven development has been used. We discuss the results of these combined techniques in a project which developed the power control service of an interventional X-ray system.
Paolo Parisen Toldin, Rody Kersten, Bernard van Gastel, and Marko van Eekelen. Soundness Proof for a Hoare Logic for Energy Consumption Analysis. Technical report: ICIS-R13009, October, Radboud University Nijmegen, 2013.
Energy inefficient software implementations may cause battery drain for small systems and high energy costs for large systems. Dynamic energy analysis is often applied to mitigate these issues. However, this is often hardware-specific and requires repetitive measurements using special equipment. We present a static analysis deriving upper-bounds for energy consumption based on an introduced energy-aware Hoare logic. Software is considered together with models of the hardware it controls. The Hoare logic is parametric with respect to the hardware. Energy models of hardware components can be specified separately from the logic. Parametrised with one or more of such component models, the analysis can statically produce a sound (over-approximated) upper-bound for the energy-usage of the hardware controlled by the software.