Scientific publications

Practical experience reveals the characteristic properties of Wireless Body Area Networks (WBANs), signifying the need for a well-designed communication protocol. High mobility, stringent resource constraints, and low and time-variant quality of wireless links are some of the challenging issues in WBANs.

Adaptation of the network architecture through ondemand data forwarding is an efficient mechanism to provide robustness against long outages in WBANs. We developed an experimental testbed that provides online observation of the network behavior for different data propagation approaches in WBANs. The demonstration shows how different approaches deal with special challenges in WBANs such as low quality of wirelesslinks, topology variations due to posture changes, and mobility.

This paper describes the use of a formal method to support component-based development in the healthcare domain. The method is based on a commercial tool suite which combines formal modeling, compositional model checking, and code generation. The main approach of the tool suite will be explained and demonstrated from a user point of view.

In this paper, we report on our research to improve the creation, implementation, and evolution of interoperability standards. Our approach was to systematically investigate a particular evolving interoperability standard, i.e., Teletext, to obtain relevant and beneficial insights that might generalize to other standards.

Many technical products and systems nowadays have functionality that is largely determined by software, so called software-intensive systems. The requirements for software-intensive systems change over time, causing the system to evolve. We define evolvability as the ability of the system to respond to such changes.

Although agent technology fits naturally to the control of the massively parallel processes in warehouses, agent-based warehouse management and control systems (WMCSs) have hardly been used in industry. We argue that model-driven development of such systems is crucial for their industrial applicability.

To increase the confidence in the correctness of software components, we investigated the use of two complementary formal methods in industrial software development. We combine a commercial refinement checker, the ASD:Suite of the company Verum, with the academic verification tool Uppaal to encompass a larger range of verification possibilities.

Probabilistic model checking has been used recently to assess, among others, dependability measures for a variety of systems. However, the numerical methods employed, such as those supported by model checking tools such as PRISM and MRMC, suffer from the state-space explosion problem. The main alternative is statistical model checking, which uses standard Monte Carlo simulation, but this performs poorly when small probabilities need to be estimated.