Scientific publications

Development of computerized embedded control systems is difficult because it brings together systems theory, electrical engineering and computer science. The engineering and analysis approaches advocated by these disciplines are fundamentally different which complicates reasoning about e.g. performance at the system level.

The verification of cryptographic protocol specifications is an active research topic and has received much attention from the formal verification community. By contrast, the black-box testing of actual implementations of protocols, which is, arguably, as important as verification for ensuring the correct functioning of protocols in the “real” world, is little studied.

Performance models are mostly simple mathematical formulas. The challenge is to model the performance at an appropriate level. In this presentation we introduce several levels of modeling, labeled zeroth order, second order, et cetera. AS illiustration we use the performance of MRI reconstruction.

The growing complexity and size of systems and the organizations that create these systems trigger the need for instruments that facilitate the creation of these systems. We shortly analyze these trends and the (potential) role of reference architectures as facilitating means. After a short discussion about the content of Reference Architectures and their relation with system architectures, system design and actual systems, we zoom in on the question what the appropriate level of detail is for Reference Architectures.

A critical task for system operators is the precise identification of the root causes underlying an error situation. This identification is fundamental in deciding optimal maintenance actions, such as replacing a component versus calibrating it. However, the actual causes of an error are often neither measured nor unique.

Synchronous dataflow graphs (SDFGs) are widely used to model streaming applications such as signal processing and multimedia applications. These are often implemented on resource-constrained embedded platforms ranging from PDAs and cell phones to automobile equipment and printing systems. Trade-off analysis between resource usage and performance is critical in the life cycle of those products, from tailoring platformsto target applications at design time to resource management at runtime.

This paper presents a simple resource control mechanism with traffic scheduling for 2-hop ad-hoc networks, in which the Request-To-Send (RTS) packet is utilized to deliver feedback information. With this feedback information, the Transmission Opportunity (TXOP) limit of the sources can be controlled to balance the traffic.

With the increasing capabilities of Wireless Sensor Networks (WSN), complexity and expectation of the WSN applications increase as well. In order to make design-space exploration possible, it is necessary to have fast models that provide adequate insight in system behavior. In this paper, we propose a highly abstracted, hierarchical, system-level modeling method for WSN.

Wireless sensor networks (WSNs) consist of numerous sensor nodes with several possible configurations for each node. As there are a lot of nodes in a typical WSN, each with its own set of configurations, the number of configurations for the network as a whole is huge and the design space is extremely large.

Electronic passports, or e-passports for short, contain a contactless smartcard which stores digitally signed data. To rigorously test e-passports, we developed formal models of the e-passport protocols that enable model-based testing using the TorXakis framework.