Carnegie Mellon University

file

Visible to the public CrAVES : Credible Autocoding and Verification of Embedded Software

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

Visible to the public Differential Radical Invariants: Safety Verification and Design of Correct Hybrid Systems

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

Visible to the public Enabling and Advancing Human and Probabilistic Context Awareness for Smart Facilities and Elder Care

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

Visible to the public Efficient Mapping and Management of Applications onto Cyber-Physical Systems

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

Visible to the public Event-Based Information Acquisition, Learning, and Control in High-Dimensional Cyber-Physical Systems

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

Visible to the public Knowledge-Aware Cyber-Physical Systems

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:

file

Visible to the public ROSELINE: Enabling Robust, Secure and Efficient Knowledge of Time Across the System Stack

Abstract:

Central to the operation of cyber-physical systems (CPS) is accurate and reliable knowledge of time, both for meaningfully sensing and controlling the physical world state and for correct, high-performance and energy-efficient orchestration of computing and communication operations. Emerging applications that seek to control agile physical processes or depend on precise knowledge of time to infer location and coordinate communication, make use of time with diverse semantics and dynamic quality requirements.