Abstraction is intensively used in the verification of large, complex or infinite-state systems. With abstractions getting more complex it is often difficult to see whether they are valid. However, for using abstraction in model checking it has to be ensured that properties are preserved. In this paper, we use a translation validation approach to verify property preservation of system abstractions. We formulate a correctness criterion based on simulation between concrete and abstract system for a property to be verified. For each distinct run of the abstraction procedure the correctness is verified in the theorem prover Isabelle/HOL. This technique is applied in the verification of embedded adaptive systems. This paper is an extended version a previously published work.
The Super-Peer Selection Problem is an optimization problem in network topology construction. It may be cast as a special case of a Hub Location Problem, more exactly an Uncapacitated Single Allocation p-Hub Median Problem with equal weights. We show that this problem is still NP-hard by reduction from Max Clique.
Embedded systems have become ubiquitous in everyday life, and especially in the automotive industry. New applications challenge their design by introducing a new class of problems that are based on a detailed analysis of the environmental situation. Situation analysis systems rely on models and algorithms of the domain of computational geometry. The basic model is usually an Euclidean plane, which contains polygons to represent the objects of the environment. Usual implementations of computational geometry algorithms cannot be directly used for safety-critical systems. First, a strict analysis of their correctness is indispensable and second, nonfunctional requirements with respect to the limited resources must be considered. This thesis proposes a layered approach to a polygon-processing system. On top of rational numbers, a geometry kernel is formalised at first. Subsequently, geometric primitives form a second layer of abstraction that is used for plane sweep and polygon algorithms. These layers do not only divide the whole system into manageable parts but make it possible to model problems and reason about them at the appropriate level of abstraction. This structure is used for the verification as well as the implementation of the developed polygon-processing library.
The IEEE 802.11 networks have a tremendous growth in the last years, but also now there is a rapid development of the wireless LAN technologies. High transmission rates, simple deployment and especially low costs make this network technology an efficient and cheap way to get access to the Internet. Fon is the world-wide greatest WIFI community and in January 2007 this community offers more than 11.000 access points in Germany and nearly 55.000 all over the world. However, this technology has also his shady sides. For example, it is possible for everyone to receive data from the wireless medium. So a protection against this open data traffic is a encryption mechanism called Wired Equivalent Privacy (WEP). The tragic end of theWired Equivalent Privacy (WEP) and the simplicity of various Denial-of-Service (DoS) attacks on the wireless medium have resulted in giving up the security at the logical-link layer and shifting it to upper layers (or in the best case leaving it within virtual private networks (VPNs)). Nevertheless, there is an enormous growth in using public access to the Internet via HotSpots in cafés, libraries, schools or at airports, train stops etc. Therefore, it is important for the Wireless Internet Service Provider (WISP) to make sure that anyone with a usual wireless device can connect to their access points. Offering this service to anybody makes giving a sufficient level of security very difficult. On the one hand it should be easy for everyone to use this access, on the other hand there is, in most cases, no security. A businessman is not very pleased about phishing his account data for a great enterprise or for his online office like the KIS at the University of Technology in Kaiserslautern. In most cases the WISPs use a simple web based authentication mechanism. By connecting to the WISPs services, the user is redirected to a webpage requesting his login data or credit card information. Therefore the user only needs a wireless LAN device and a webbrowser to authenticate. An attacker could sniff on the wireless medium to phish delicate data from a legal connected user or use DoS attacks as initial point for various other attacks. In most cases, this can be done with no or only small effort. On the other side, in some cases, the WISP has to do a hard reset on his wireless devices after a DoS attack. Therefore an analysis of access points is done in this work. So, the first part is to show how "‘new"’ access points react to flooding attacks and what mechanisms are used to protect them. The second part implements an attack using an anomaly of some access points that are discovered in the first part. And the last chapter deals with some information about using an Intrusion Detection System (IDS) to protect the devices against such attacks.
The provision of network Quality-of-Service (network QoS) in wireless (ad-hoc) networks is a major challenge in the development of future communication systems. Before designing and implementing these systems, the network QoS requirements are to be specified. Since QoS functionalities are integrated across layers and hence QoS specifications exist on different system layers, a QoS mapping technique is needed to translate the specifications into each other. In this paper, we formalize the relationship between layers. Based on a comprehensive and holistic formalization of network QoS requirements, we define two kinds of QoS mappings. QoS domain mappings associate QoS domains of two abstraction levels. QoS scalability mappings associate utility and cost functions of two abstraction levels. We illustrate our approach by examples from the case study Wireless Video Transmission.
The provision of network Quality-of-Service (network QoS) in wireless (ad-hoc) networks is a major challenge in the development of future communication systems. Before designing and implementing these systems, the network QoS requirements are to be specified. Existing approaches to the specification of network QoS requirements are mainly focused on specific domains or individual system layers. In this paper, we present a holistic, comprehensive formalization of network QoS requirements, across layers. QoS requirements are specified on each layer by defining QoS domain, consisting of QoS performance, reliability, and guarantee, and QoS scalability, with utility and cost functions. Furthermore, we derive preorders on multi-dimensional QoS domains, and present criteria to reduce these domains, leading to a manageable subset of QoS values that is sufficient for system design and implementation. We illustrate our approach by examples from the case study Wireless Video Transmission.
Calibration of robots has become a research field of great importance over the last decades especially in the field industrial robotics. The main reason for this is that the field of application was significantly broadened due to an increasing number of fully automated or robot assisted tasks to be performed. Those applications require significantly higher level of accuracy due to more delicate tasks that need to be fulfilled (e.g. assembly in the semiconductor industry or robot assisted medical surgery). In the past, (industrial) robot calibration had to be performed manually for every single robot under lab conditions in a long and cost intensive process. Expensive and complex measurement systems had to be operated by highly trained personnel. The result of this process is a set of measurements representing the robot pose in the task space (i.e. world coordinate system) and as joint encoder values. To determine the deviation, the robot pose indicated by the internal joint encoder values has to be compared to the physical pose (i.e. external measurement data). Hence, the errors in the kinematic model of the robot can be computed and therefore later on compensated. These errors are inevitable and caused by varying manufacturing tolerances and other sources of error (e.g. friction and deflection). They have to be compensated in order to achieve sufficient accuracy for the given tasks. Furthermore for performance, maintenance, or quality assurance reasons the robots may have to undergo the calibration process in constant time intervals to monitor and compensate e.g. ageing effects such as wear and tear. In modern production processes old fashioned procedures like the one mentioned above are no longer suitable. Therefore a new method has to be found that is less time consuming, more cost effective, and involves less (or in the long term even no) human interaction in the calibration process.
Embedded systems are becoming more and more important in today’s life in many ways. They can be found in dishwashers, mobile phones, coffee machines, PDAs, etc. Although there is no common definition of what an embedded system is, it can be generally defined as a special-purpose information processing system, containing both: software and hardware. Embedded systems are integrated in a larger systems which interact with environment for achieving a set of predefined tasks or applications. In general, embedded systems are characterized by resources scarcity, among which energy is becoming more and more important (especially the energy consumed by the processor). The energy consumed by an embedded system is strongly influenced by the software running on it (the embedded software). That is why it is crucial to explore the software characteristics that have an influence on the energy consumption, and to understand how this influence could be represented. In order to realize this task, there is a need for the construction of a reliable measurement platform for energy consumption by embedded devices. The target of this work is to design and implement a framework for measuring energy consumption of embedded software. This framework is based on the XScale architecture, a popular Intel platform designed for energy aware applications. The framework has a software repository which contains a number of programs (user-defined) that are supposed to run on the mentioned platform. These program codes are the input of the framework. Automated measurements for energy consumption are performed on all programs for gathering the required information. In the context of this work, a first evaluation of the framework was performed to make an initial check its quality.
Nowadays, accounting, charging and billing users' network resource consumption are commonly used for the purpose of facilitating reasonable network usage, controlling congestion, allocating cost, gaining revenue, etc. In traditional IP traffic accounting systems, IP addresses are used to identify the corresponding consumers of the network resources. However, there are some situations in which IP addresses cannot be used to identify users uniquely, for example, in multi-user systems. In these cases, network resource consumption can only be ascribed to the owners of these hosts instead of corresponding real users who have consumed the network resources. Therefore, accurate accountability in these systems is practically impossible. This is a flaw of the traditional IP address based IP traffic accounting technique. This dissertation proposes a user based IP traffic accounting model which can facilitate collecting network resource usage information on the basis of users. With user based IP traffic accounting, IP traffic can be distinguished not only by IP addresses but also by users. In this dissertation, three different schemes, which can achieve the user based IP traffic accounting mechanism, are discussed in detail. The inband scheme utilizes the IP header to convey the user information of the corresponding IP packet. The Accounting Agent residing in the measured host intercepts IP packets passing through it. Then it identifies the users of these IP packets and inserts user information into the IP packets. With this mechanism, a meter located in a key position of the network can intercept the IP packets tagged with user information, extract not only statistic information, but also IP addresses and user information from the IP packets to generate accounting records with user information. The out-of-band scheme is a contrast scheme to the in-band scheme. It also uses an Accounting Agent to intercept IP packets and identify the users of IP traffic. However, the user information is transferred through a separated channel, which is different from the corresponding IP packets' transmission. The Multi-IP scheme provides a different solution for identifying users of IP traffic. It assigns each user in a measured host a unique IP address. Through that, an IP address can be used to identify a user uniquely without ambiguity. This way, traditional IP address based accounting techniques can be applied to achieve the goal of user based IP traffic accounting. In this dissertation, a user based IP traffic accounting prototype system developed according to the out-of-band scheme is also introduced. The application of user based IP traffic accounting model in the distributed computing environment is also discussed.