Contracts for Real-Time, Safety Critical Systems

Verifying real-time systems goes beyond the verification of functional properties: it also requires the checking of real-time properties. This makes traditional contract-frameworks partially inept for checking real-time programs. This is a major problem because the failure of real-time and safety critical systems can have serious consequences. This thesis presents a solution to this problem by incorporating Design by Contract (annotating programs with function pre and post conditions) to such systems. The main contribution of this thesis is the development of a contract framework for cyclic real-time control applications written in C++. The contract framework allows the users to specify both functional and temporal properties for the applications. A novel approach of empirical cumulative distribution function (cdf ) based statistical inference is used for dynamically estimating temporal constraints and incorporating them in future contracts. The thesis also illustrates the use of Real-time Logic (RTL) for formal specification of the temporal properties. For evaluating our methodology, we have integrated it to a component-based framework called FASA (Future Automation System Architecture) developed at ABB Corporate Research for writing hard real time control applications. Experiments show that this contract framework can be smoothly integrated to existing control applications thereby increasing their reliability while having a acceptable overhead (less than 10%) on the performance.

Designable Visual Markers for Mobile Human-Computer Interaction

Enrico Costanza

Visual markers are graphic symbols designed to be easily recognised by machines. They are traditionally used to track goods, but there is increasing interest in their application to mobile human-computer interaction (HCI). By scanning a visual marker through a camera phone, users can retrieve localised information and access mobile services. In particular the dissertation examines the application of visual markers to physical tagging: practices of association of digital information with physical items. One missed opportunity in current visual marker systems is that the markers themselves cannot be visually designed; they are not expressive to humans, and thus fail to convey information before being scanned. To address this limitation, this dissertation introduces the idea of designable markers, visual markers that are both machine-readable and visually communicative to humans, and presents an investigation of the ways in which they can support mobile human-computer interaction. The application of designable visual markers to the creation of mobile interfaces is explored through a variety of methods: through formal usability experiments, through the creation and analysis of example designs, as well as through the qualitative analysis of two field trials. All three approaches were enabled by the engineering and development of d-touch, an actual recognition system that supports designable visual markers and by its integration in a variety of applications and experimental probes. D-touch is based on image topology, and its markers are defined in terms of constraints on the nesting of dark and light regions. The constraints imposed by d-touch are flexible enough to allow novice users to create markers which are visually expressive and at the same time machine readable. A user study demonstrates how such system enables people to design their own functional visual markers, determining their aesthetic qualities and what they visually communicate to others. A desktop application to support users in the creation of valid markers, the d-touch analyser, is presented and its usefulness is demonstrated through the same study. A formal usability experiment comparing five variations of marker-based interfaces on keypad and touch-screen phones shows that all of them allow users to reliably select targets within, on average, less than 4 seconds. Participants of the experiment reported a strong preference for interfaces that involve only marker scanning, compared to those that require a combination of marker scanning and key-presses or touch selections. Example designs of mobile interface generated by the author as well as others are presented to expose how the d-touch recognition system can be integrated in mobile applications. The examples illustrate a variety of ways in which markers can be used to augment printed materials such as cards, books and product packages, adding to them interactive capabilities. The examples show also different approaches to marker design, ranging from simple and recognisable iconic design, to symbols that integrate cues about the interactive functionality, to making them invisible by hiding them in existing graphics. Finally, the dissertation reports and analyses two field trials conducted to study what practices of physical tagging can emerge from, and be supported by, the use of markers. The trials were centred around the use of uWiki, a functional prototype based on d-touch, that allows users to associate digital content to markers printed on physical tags that can be affixed to objects or buildings. Observations show that a variety of practices emerge around the use of this technology, indicating that they provide a rich medium that has potential to attract the interest of real users. Though the results of this work are preliminary, they serve to demonstrate the range of potential for the future of such systems.

EPFL2010

Haptic interface design and control with application to surgery simulation

Ulrich Spälter

This thesis proposes a framework for haptic devices interacting with virtual environments. As application of the theoretical results a haptic device for the surgical training of hysteroscopy, a gynecologic intervention, is presented. Surgery simulators, which can be described as 'flight simulators for surgeons', comprise a virtual reality for modeling and visualization of organs, and the haptic device: While the surgeon interactively follows the scene on the computer screen, he perceives the contact forces at the tool handle of the surgical instrument. The haptic device tracks the position of the surgery tool and transforms the virtual contact forces to real forces, which can be actually felt by the surgeon. This thesis treats haptic devices with application to surgery simulators for minimally-invasive surgery. Haptic interfaces are complex mechatronic systems and show inherent trade-offs between haptic realism and system stability. Human factors play an important role, as the human operator can both stabilize or destabilize the system. The haptic perception, which can vary between individuals, as a criterion for haptic rendering quality is still not formalized. The optimization of haptic interfaces, within focus of research since 15 years ago, has remained a complex task. However, with look at the emerging applications for haptics, it has become an even more important topic. For this reason it is necessary to integrate mechanical design, control design, mechatronic elements and human factors in a unifying approach. This thesis highlights the principal trade-offs of haptic interfaces and works out design guidelines for new developments and quantitative information on where and how to optimize haptic systems. As application example a haptic interface for the simulation of hysteroscopy, a gynecologic intervention on the female uterus, has been realized as prototype. The device takes the characteristics of hysteroscopy into account and introduces features like insertion and complete removal of the surgery tool from the haptic interface. A design methodology is proposed, which combines aspects of theoretical kinematics based on Lie-Groups with integrated product development – a systematic approach for engineering tasks. The result, a novel kinematic design, has been realized as haptic interface prototype. The well-known affine parameterization for all stabilizing controllers is shown to be a well-suited tool for haptic control synthesis. It provides insights into the control trade-offs and allows to integrate human factors at controller design stage. The resulting controller, demonstrated by experimental results, can reduce parasitic effects (friction, device dynamics) close to and below the human perception threshhold, thus making the device transparent within the specified bandwidth and suitable for real-time implementation. For numerical controller representation the δ-operator is discussed. It unifies continuous and discrete time domain and has beneficial numerical properties. As there is still no standardized procedure for technical performance evaluation of haptic interfaces methods proposed in literature are summarized. In the near future a large market for haptic technology can be expected with applications from surgery-assist devices and drive-by-wire interfaces in automobiles to entertainment, which highlights the relevance of the treated topic.

EPFL2006

Representation Learning for Multi-relational Data

Eda Bayram

Recent years have witnessed a rise in real-world data captured with rich structural information that can be better depicted by multi-relational or heterogeneous graphs.However, research on relational representation learning has so far mostly focused on the problems arising in simple, homogeneous graphs. Integrating the structural priors provided by multi-relational data may further empower the generalization capacity of representation learning models, yet it still remains an open challenge.Although there is a strong line of works on relational machine learning on knowledge graphs, it is quite concentrated on the task ofcompleting missing edges, which is known as link prediction. In this thesis, we shift the focus away from the well-addressed node and graph classification problems on simple graphs or the link prediction problem on knowledge graphs, and prompt new research questions targeting the representation learning problems that are overlooked in multi-relational data.First, we focus on the problem of node regression on multi-relational graphs, noting that inference of continuous node features across a graph is rather under-studied in the current relational learning research.We propose a novel propagation method which aims to complete missing features at the nodes of a multi-relational and directed graph.Our multi-relational propagation algorithm is composed of iterative neighborhood aggregations which originate from a relational local generative model. Our findings show the benefit of exploiting the inductive bias led by the multi-relational structure of the data.Next, we consider the node attribute completion problem in knowledge graphs, which is relatively unexplored by the knowledge graph reasoning literature.We propose a novel multi-relational attribute propagation method where we harness not only the relational structure of the knowledge graph, but also the dependencies between various types of numerical node attributes relying on a heterogeneous feature space.Our algorithm is framed within a message-passing scheme where the propagation parameters are estimated in advance. We also propose an alternative semi-supervised learning framework where the parameters and the missing node attributes are inferred in an end-to-end fashion.Experimental results on well-known knowledge graph datasets relay the effectiveness of our message-passing approach, which specifies the computational graph by the heterogeneity of the data.Finally, we study graph learning in multi-relational data domain.Unlike the existing structure inference methods, we aim at exploiting and combining each source of relational information provided by the data domain to learn the underlying graph of a set of observations.For this purpose, we employ a multi-layer graph representation which encodes multiple types of relationships between data entities. Then, we propose a mask learning method to infer a specific combination of the layers which reveals the structure of observations.Experiments conducted both on simulated and real-world data suggest that incorporating multi-relational domain knowledge enhances structure inference by boosting its adaptability to a variety of input data conditions.

EPFL2021