Publications

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.

The three technical universities in the Netherlands (Eindhoven University of Technology, Delft University of Technology and University of Twente), abbreviated as 3TU, started a joint master on Embedded Systems in 2006. Embedded Systems is an interdisciplinary area of Electrical Engineering, Computer Science, Mechanical Engineering and Applied Mathematics.

In this paper, we present a dynamic analysis approach to increase the understandability of a large softwareintensive system, more particularly to enable the identification of dependencies between its execution entities. This approach analyzes the execution of a software system in a top-down fashion to cope with complexity and uses execution entities such as scenarios, components, and processes rather than code artifacts such as modules, classes, or objects.

Conformance testing for labeled transition systems starts with defining when an implementation conforms to its specification. One of the formal theories for model-based testing uses the implementation relation ioco for this purpose. A peculiar aspect of ioco is to consider the absence of outputs as an observable action, named quiescence.

During the last three years, we have been experimenting with the use of the Uppaal model checker in an introductory course on operating systems for first-year Computer Science students at the Radboud University Nijmegen. The course uses model checkers as a tool to explain, visualize and solve concurrency problems.

This chapter argues that embedded systems design faces several challenges of which late integration and the difference in development productivity between disciplines are major ones. Model driven engineeringMDE) looks a promising approach to address these challenges. However, MDE is a new approach which has to be defined and implemented in close interaction by academia and industry the near future.

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.