Abstract

file

Visible to the public Cyber-Physical Cloud Computing

Abstract:

Computation advances in physical time, but embedded computing has found value in logical time programming. Likewise, robotic systems can be simplified by programming in logical space, even though robots live and move in physical space. Our tools ask the roboticist to program on a logical abstraction of the physical. The principal new products are two drivers. One handles the problem of keeping the logical model consistent with physical data. The other enables logical control actions to have physical effect.

file

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

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

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 CPS: Synergy: A Novel Biomechatronic Interface Based on Wearable Dynamic Imaging Sensors

The problem of controlling biomechatronic systems, such as multiarticulating prosthetic hands, involves unique challenges in the science and engineering of Cyber Physical Systems (CPS), requiring integration between computational systems for recognizing human functional activity and intent and controlling prosthetic devices to interact with the physical world. Research on this problem has been limited by the difficulties in noninvasively acquiring robust biosignals that allow intuitive and reliable control of multiple degrees of freedom (DoF).

file

Visible to the public Dynamical-Network Evaluation and Design Tools for Strategic-to-Tactical Air Traffic Flow Management

Abstract:

The objective of this research is to develop tools for comprehensive design and optimization of air traffic flow management capabilities at multiple spatial and temporal resolutions: at a national airspace-wide scale and one-day time horizon (strategic time- frame); and at a regional scale (of one or a few Centers) and a two-hour time horizon (tactical time-frame).

The following results were obtained in Year 4 of the project:

file

Visible to the public Dynamic Routing and Robotic Coordination for Oceanographic Adaptive Sampling

Abstract:

Networks of autonomous coordinated robots areprototypical examples of cyber-physical systems. Already today and increasingly in the near future, robotic systems will perform a broad range of environmental monitoring and logistic tasks. Aquatic robots will monitor oceanic life and conditions. Teams of vehicles will perform exploration, firefighting and search and rescue operations.

file

Visible to the public Distributed Sensing Collective to Capture 3D Soundscapes

Abstract:

Oceans are drivers of global climate; they are home to some of our most important and diverse ecosystems; and they provide a substantial amount to the world's economy as a major source of food and employment. Sound plays a vital role in the ocean ecosystem, as many organisms rely on the acoustic environment for navigation, communication, detecting predators and finding food.

file

Visible to the public Distributed Just-Ahead-Of-Time Verification of Cyber-Physical Critical Infrastructures

Abstract:

Trustworthy operation of next-generation complex power grid critical infrastructures requires mathematical and practical verification solutions to guarantee the correct infrastructural functionalities. This project develops the foundations of theoretical modeling, synthesis and real-world deployment of a formal and scalable controller code verifier for programmable logic controllers (PLCs) in cyber-physical settings. PLCs are widely used for control automation in industrial control systems.

file

Visible to the public Distributed Asynchronous Algorithms & Software Systems For Wide-Area Monitoring of Power Systems

Abstract:

The objective of this project is to develop a distributed algorithmic framework, supported by a highly fault-tolerant software system, for executing critical transmission-level operations of the North American power grid using gigantic volumes of Synchrophasor data.

file

Visible to the public Digital Control of Hybrid Systems via Simulation and Bisimulation

Abstract:

The research objective of this project is to bridge two disparate paths to the control of hybrid dynamical systems--namely, symbolic model-based and Lyapunov analysis-based approaches--via convex programming in order to address major challenges in hybrid control. Hybrid systems are characterized by the presence of both continuous dynamics and discrete logic that interact with each other.