The provision of quality-of-service (QoS) on the network layer is a major challenge in communication networks. This applies particularly to mobile ad-hoc networks (MANETs) in the area of Ambient Intelligence (AmI), especially with the increasing use of delay and bandwidth sensitive applications. The focus of this survey lies on the classification and analysis of selected QoS routing protocols in the domain of mobile ad-hoc networks. Each protocol is briefly described and assessed, and the results are summarized in multiple tables.
Guaranteeing correctness of compilation is a ma jor precondition for correct software. Code generation can be one of the most error-prone tasks in a compiler. One way to achieve trusted compilation is certifying compilation. A certifying compiler generates for each run a proof that it has performed the compilation run correctly. The proof is checked in a separate theorem prover. If the theorem prover is content with the proof, one can be sure that the compiler produced correct code. This paper presents a certifying code generation phase for a compiler translating an intermediate language into assembler code. The time spent for checking the proofs is the bottleneck of certifying compilation. We exhibit an improved framework for certifying compilation and considerable advances to overcome this bottleneck. We compare our implementation featuring the Coq theorem prover to an older implementation. Our current implementation is feasible for medium to large sized programs.
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.
This report gives an overview of the separate translation of synchronous imperative programs to synchronous guarded actions. In particular, we consider problems to be solved for separate compilation that stem from preemption statements and local variable declarations. We explain how we solved these problems and sketch our solutions implemented in the our Averest framework to implement a compiler that allows a separate compilation of imperative synchronous programs with local variables and unrestricted preemption statements. The focus of the report is the big picture of our entire design flow.
SHIM is a concurrent deterministic programming language for embedded systems built on rendezvous communication. It abstracts away many details to give the developer a high-level view that includes virtual shared variables, threads as orthogonal statements, and deterministic concurrent exceptions.
In this paper, we present a new way to compile a SHIM-like language into a set of asynchronous guarded actions, a well-established intermediate representation for concurrent systems. By doing so, we build a bridge to many other tools, including hardware synthesis and formal verification. We present our translation in detail, illustrate it through examples, and show how the result can be used by various other tools.
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.
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.
Selbstorganisation ist eine interessante und vielversprechende Möglichkeit, um die Komplexität verteilter Systeme beherrschbar zu machen. In diesem Beitrag schlagen wir ein leistungsfähiges Rechnersystem auf Basis von rekonfigurierbarer Hardware vor, welches aufgrund seiner Flexibilität in vielen Bereichen eingesetzt werden kann. Es wird die geplante Systemarchitektur und Systemsoftware beschrieben und ein intelligentes, verteiltes Kamerasystem vorgestellt, welches wir als Anwendung mit dem vorgeschlagenen System realisieren wollen, um Selbstorganisation in verteilten Systemen näher zu untersuchen.
Objective: In some surgical specialties, e.g. orthopedics, robots are already used in the operating room for bony milling work. Oto- and otoneurosurgery may also greatly benefit by robotic enhanced precision. Study Design: Experimental study on robotic milling on oak wood and human temporal bone specimen. Methods: A standard industrial robot with a 6 degrees-of-freedom serial kinematics was used with force feedback to proportionally control the robot speed. Different milling modes and characteristic path parameters were evaluated to generate milling paths based on CAD geometry data of a cochlear implant and an implantable hearing system. Results: The best suited strategy proofed to be the spiral horizontal milling mode with the burr held perpendicularly to the temporal bone surface. In order to avoid high grooves, the distance in between paths should equal half the radius of the cutting burr head. Due to the vibration of the robot’s own motors, a rather high oscillation of the standard deviation of forces was encountered. This oscillation dropped drastically to nearly 0 N, when the burr head reached contact with the dura mater due to its damping characteristics. The cutting burr could be moved a long time on the dura without damaging it, because of its rather blunt head. The robot moved the burr very smoothly according to the encountered resistances. Conclusion: This is the first development of an functioning robotic milling procedure for otoneurosurgery with force-based speed control. It is planned to implement ultrasound-based local navigation and to perform robotic mastoidectomy.
Das Handlungsreisendenproblem ist eines der bekanntesten NP-vollständigen kombinatorischen Optimierungsprobleme. Algorithmen mit unterschiedlichen Konzepten und Strategien wurden entwickelt, die sich in Lösungsqualität und Laufzeit unterscheiden. Ein vergleichsweise neuer Ansatz stellt jedoch das Kombinieren vorhandener Lösungen dar. Hier werden die Kantenmengen gegebener Handlungsreisendertouren als Ausgangsbasis für weitere Optimierungen verwendet. Erste Veröffentlichungen zu diesem Gebiet stellen bereits vielversprechende Ergebnisse vor, die nachfolgend vertieft evaluiert werden.