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.
There is a well known relationship between alternating automata on finite words and symbolically represented nondeterministic automata on finite words. This relationship is of practical relevance because it allows to combine the advantages of alternating and symbolically represented nondeterministic automata on finite words. However, for infinite words the situation is unclear. Therefore, this work investigates the relationship between alternating omega-automata and symbolically represented nondeterministic omega-automata. Thereby, we identify classes of alternating omega-automata that are as expressive as safety, liveness and deterministic prefix automata, respectively. Moreover, some very simple symbolic nondeterminisation procedures are developed for the classes corresponding to safety and liveness properties.
Ownership Domains generalize ownership types. They support programming patterns like iterators that are not possible with ordinary ownership types. However, they are still too restrictive for cases in which an object X wants to access the public domains of an arbitrary number of other objects, which often happens in observer scenarios. To overcome this restriction, we developed so-called loose domains which abstract over several precise domains. That is, similar to the relation between supertypes and subtypes we have a relation between loose and precise domains. In addition, we simplified ownership domains by reducing the number of domains per object to two and hard-wiring the access permissions between domains. We formalized the resulting type system for an OO core language and proved type soundness and a fundamental accessibility property.
With the UML 2.0 standard, the Unified Modeling Language took a big step towards SDL, incorporating many features of the language. SDL is a mature and complete language with formal semantics. The Z.109 standard defines a UML Profile for SDL, mapping UML constructs to corresponding counterparts in SDL, giving them a precise semantics. In this report, we present a case study for the formalisation of the Z.109 standard. The formal definition makes the mapping precise and can be used to derive tool support.
This document introduces the extension of Katja to support position structures and explains the subtleties of their application as well as the design decisions made and problems solved with respect to their implementation. The Katja system was first introduced by Jan Schäfer in the context of his project work and is based on the MAX system developed by Arnd Poetzsch-Heffter.
Katja is a tool generating order-sorted recursive data types as well as position types for Java, from specifications using an enhanced ML like notation. Katja’s main features are its conciseness of specifications, the rich interface provided by the generated code and the Java atypical immutability of types. After several stages of extending and maintaining the Katja project, it became apparent many changes had to be done. The original design of Katja wasn’t prepared for the introduction of several backends, the introduction of position sorts and constant feature enhancements and bug fixes. By supplying this report Katja reaches release status for the first time.
Over a period of 30 years, ITU-T’s Specification and Description Language (SDL) has matured to a sophisticated formal modelling language for distributed systems and communication protocols. The language definition of SDL-2000, the latest version of SDL, is complex and difficult to maintain. Full tool support for SDL is costly to implement. Therefore, only subsets of SDL are currently supported by tools. These SDL subsets - called SDL profiles - already cover a wide range of systems, and are often suffcient in practice. In this report, we present our approach for extracting the formal semantics for SDL profiles from the complete SDL semantics. We then formalise the approach, present our SDL-profile tool, and report on our experiences.
Web-based authentication is a popular mechanism implemented by Wireless Internet Service Providers (WISPs) because it allows a simple registration and authentication of customers, while avoiding the high resource requirements of the new IEEE 802.11i security standard and the backward compatibility issues of legacy devices. In this work we demonstrate two different and novel attacks against web-based authentication. One attack exploits operational anomalies of low- and middle-priced devices in order to hijack wireless clients, while the other exploits an already known vulnerability within wired-networks, which in dynamic wireless environments turns out to be even harder to detect and protect against.