Carnegie Mellon University
file
Abstract:
People with upper extremity disabilities are gaining increased independence through the use of assistive robotic arms, but performing tasks that require many small precise movements remains difficult. In fact, a confounding factor is that the more severe a person's motor impairment, the more limited are the control interfaces available to them to operate the system.
file
Abstract:
Despite many advances in vehicle automation, much remains to be done: the best autonomous vehicle today still lags behind human drivers, and connected vehicle (V2V) and infrastructure (V2I) standards are only just emerging. In order for such cyber-physical systems to fully realize their potential, they must be capable of exploiting one of the richest and most complex abilities of humans, which we take for granted: seeing and understanding the visual world.
file
Abstract:
Commodity operating systems manage time in a best effort fashion, where clock synchronization is performed independently of both application demand and resource constraints. The vision of the RoseLine project is to develop a Quality of Time (QoT) stack for Linux that enables developers to write distributed applications that perform computation with a common sense of time.
file
Abstract:
Time is not necessarily what a clock reports. There is an uncertainty in time which is often not reported. Quantifying this timing uncertainty with clock parameters such as accuracy, precision, jitter or wander, is what introduces quality in time. Modern operating systems such as Linux lacks this perception of Quality of Time (QoT). It exposes some default clocks which are time synchronized / syntonized on best-effort basis through NTP or PTP, irrespective of the applications demand and the resources at hand.
file
Abstract:
The computing landscape is a richly-heterogeneous space including both fixed and mobile nodes with a large variety of sensing, actuation and computational capabilities (including mobile devices, home electronics, taxis, robotic drones, etc.). Cyber-physical applications built on these devices have the potential to gather data on, analyze, and adapt to or control a range of environments.
file
Abstract:
KeYmaera X is a theorem prover for specifying and verifying correctness properties of hybrid systems (systems that mix discrete and continuous dynamics). KeYmaera X implements differential dynamic logic (dL) and provides a high degree of control over automated proof search.
video
Submitted by jessygrizzle on Tue, 12/02/2014 - 4:45pm
file
Abstract:
The use of deductive techniques, such as theorem provers, has several advantages in safety verification of hybrid systems. State-of-the-art theorem provers, however, suffer from a significant lack of automation.
