Scientific publications

This paper presents an adaptive resource control mechanism for multihop ad-hoc network systems, which avoids bottleneck problems caused by the node-fairness property of IEEE 802.11. In our proposal, the feedback information from the downstream bottleneck, derived from Request-To-Send (RTS) and Clear-To-Send (CTS) messages is utilized to control the Transmission Opportunity (TXOP) limit of the upstream nodes for traffic balancing.

A new simultaneous autofocus and twofold astigmatism correction method is proposed for High Angle Annular Dark Field Scanning Transmission Electron Microscopy (HAADF-STEM). The method makes use of a modification of image variance, which has already been used before as an image quality measure for different types of microscopy, but its use is often justified on heuristic grounds.

This paper studies quantitative model checking of infinite tree-like (continuous-time) Markov chains. These tree-structured quasi-birth death processes are equivalent to probabilistic pushdown automata and recursive Markov chains and are widely used in the field of performanceevaluation.Wedeterminetime-boundedreachabilityprobabilitiesinthese processes– which with direct methods, i.

Gossip protocols are designed to operate in very large, decentralised networks. A node in such a networkbases its decision to interact (gossip) with another node on its partial view of the global system. Because of the size of these networks, analysis of gossip protocols is mostly done using simulations, but these tend to be expensive in computation time and memoryconsumption.

In this chapter we present an overview of decomposition-based analysis techniques for large open queueing networks. We present a general decompositionbased solution framework, without referring to any particular model class, and propose a general fixed-point iterative solution method for it. We concretize this framework bydescribing the well-known QNA method,as proposedby Whitt in the early 1980s, in that context, before describing our FiFiQueues approach.

A good mobility model is an essential prerequisite for performance evaluation of protocols for wireless networks with node mobility. Sensor nodes in a Wireless Body Area Network (WBAN) exhibit high mobility. The WBAN topology may completely change because of posture changes and movement evenwithin a certain typeof posture.

Evolvability, the ability to respond effectively to change, represents a major challenge to today's high-end embedded systems, such as those developed in the medical domain by Philips Healthcare. These systems are typically developed by multi-disciplinary teams, located around the world, and are in constant need of upgrading to provide new advanced features, to deal with obsolescence, and to exploit emerging enabling technologies.

The performance and dependability of critical infrastructures, such as water-treatment facilities is essential. In this paper we use various performance and dependability measures to analyze a simplified model of a water treatment facility. Building on the existing architectural framework Arcade a model is derived in XML format and then automatically mapped to the model checker PRISM Using the stochastic model checking capabilities that PRISM offers, we compare different repair strategies, with respect to their costs, system reliability, availability and survivability.

Wireless sensor networks (WSNs) are developing into a promising solution for many applications, for example in healthcare. In many scenarios, there is some form of node mobility. The medium access control (MAC) mechanisms should support the expected kind of mobility in the network. Mobility is particularly complicating for contention free MAC protocols like TDMA-based protocols, because they dedicate unique slotsto every node in a neighborhood.