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.
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.
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.