Taxonomic Search: Carnegie Mellon University

Results 1 - 10 of 77

Results

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.

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 Correct-by-Design Control Software Synthesis for Highly Dynamic Systems

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

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 Forward Invariant Cuts to Simplify Proofs of Safety

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.

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.