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.

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.

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.

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.

Abstract: This project addresses highly dynamic Cyber-Physical Systems (CPSs) understood as systems where a computing delay of a few milliseconds or an incorrectly computed response to a disturbance can lead to catastrophic consequences. Such is the case of advanced safety systems on passenger cars, unmanned air vehicles performing critical maneuvers such as landing, or disaster and rescue response bipedal robots rushing through the rubble to collect information or save human lives.

Abstract: This project addresses highly dynamic Cyber-Physical Systems (CPSs) understood as systems where a computing delay of a few milliseconds or an incorrectly computed response to a disturbance can lead to catastrophic consequences. Such is the case of advanced safety systems on passenger cars, unmanned air vehicles performing critical maneuvers such as landing, or disaster and rescue response bipedal robots rushing through the rubble to collect information or save hu- man lives.

Abstract: The last decade has seen increasing studies on bacteria and other cells-integrated bio-hybrid microrobot. A major motivation of them is to apply such kind of microsystems into targeted drug delivery system. Although various fabrication techniques have been developed to improve the efficacy of the system, control of the bio- hybrid microrobot is severely understudied, especially at population level. This poses an challenge for further application of the bio-hybrid microrobots, such as targeted drug delivery engineering.