Scientific publications

Model-based testing is one of the promising technologies to increase the efficiency and effectiveness of software testing. In modelbased testing, a model specifies the required behaviour of a system, and test cases are algorithmically generated from this model. Obtaining a valid model, however, is often difficult if the system is complex, contains legacy or third-party components, or if documentation is incomplete.

Dataflow formalisms are useful for specifying signal processing and streaming applications. To adequately capture the dynamic aspects of modern applications, the formalism of Scenario-Aware Dataflow (SADF) was recently introduced, which allows analysis of worst/best-case and average-case performance across different modes of operation (scenarios).

Embedded control is a key product technology differentiator for many high-tech industries, including ASML. The strong increase in complexity of embedded control systems, combined with the occurrence of late changes in control requirements, results in many timing performance problems showing up only during the integration phase.

Embedded multimedia and wireless applications require a model-based design approach in order to satisfy stringent quality and cost constraints. The Model-of-Computation (MoC) should appropriately capture system dynamics, support analysis and synthesis, and allow low-overhead model-driven implementations.

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.