This cross-disciplinary project brings together a team of engineering and computer science researchers to create and demonstrate the value of new techniques for ensuring that systems comprised of hardware, software, and humans will perform in a synergistic and safe manner.

Abstract: Medical devices are typically developed as stand-alone units. Current industrial Verification and Validation (V&V) tech- niques primarily target stand-alone systems. Moreover, the US Food and Drug Administration’s (FDA) regulatory clearance processes are designed to approve such devices that are integrated by a single manufacturer with complete control over all components.

Abstract: Processors in cyber‐physical systems are increasingly being used in applications where they must operate in harsh ambient conditions and a computational workload which can lead to high chip temperatures. Examples include cars, robots, aircraft and spacecraft. High operating temperatures accelerate the aging of the chips, thus increasing transient and permanent failure rates. Current ways to deal with this mostly turn off the processor core or drastically slow it down when some part of it is seen to exceed a given temperature threshold.

Abstract:  Despite their importance within the energy sector, buildings have not kept pace with technological improvements and particularly  the evolution of intelligent features. A primary obstacle  in enabling intelligent buildings is their highly distributed and diverse nature.

Abstract: Robotic devices are excellent candidates for delivering repetitive and intensive practice that can restore functional use of the upper limbs, even years after a stroke. Rehabilitation of the wrist and hand in particular are critical for recovery of function, since hands are the primary interface with the world.

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.

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.

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:

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.

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.