Carnegie Mellon University
file
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.
file
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.
file
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.
file
Abstract:
The CrAVES project seeks to lay down intellectual foundations for credible autocoding of embedded systems, by which graphical control system specifications that satisfy given open-loop and closed-loop properties are automatically transformed into source code guaranteed to satisfy the same properties. The goal is that the correctness of these codes can be easily and independently verified by dedicated proof checking systems.
file
Abstract:
The CrAVES project seeks to lay down intellectual foundations for credible autocoding of embedded systems, by which model-level control system specifications that satisfy given open-loop and closed-loop properties are automatically transformed into source code guaranteed to satisfy the same properties. The goal is that the correctness of these codes can be easily and independently verified by dedicated proof checking systems.
file
Abstract:
The verification of hybrid systems requires ways of handling both the discrete and continuous dynamics, e.g., by proofs, abstraction, or approximation. Fundamentally, however, the study of the safety of hybrid systems can be shown to reduce constructively to the problem of generating invariants for their differ- ential equations. We recently focused on this core problem. We study the case of algebraic invariant equation, i.e. invariants described by a polynomial equation of the form p = 0 for a polynomial p.
file
Abstract:
We are at the end of a fouryear effort that has dramatically improved the capability of the use of RF sensors, particularly those that measure received signal strength (RSS) to sense the locations and context of people in buildings and homes. We have investigated both systems which use RFID tags to identify a person or object, and those which use a static deployed network of transceivers for devicefree localization, to locate people moving in the environment who do not carry any tag or device. Locating people who don't wear a de
file
Abstract:
Cyber-Physical Systems comprise richly heterogeneous collections of devices (mobile devices, home electronics, taxis, robotic drones, etc.) that together gather sensor data, analyze it, and coordinate large--scale actions in response to it.
file
Abstract:
The objective of this project is to develop a theoretical framework for stochastic learning, decision-making, and control in high-dimensional cyber-physical systems. In our general framework, decision makers dynamically refine their estimates of the time-varying physical system based on acquired information, which may be obtained by distributed sensors.
file
Abstract:
During the development process of CPS, an analysis of whether the system operates safely in its target environment is of utmost importance. This entails two interconnected research goals in the research areas of system design and system verification, which tie together research in formal verification of CPS with research on knowledge representation and reasoning in multi-agent systems:
