Abstract: This project is developing a formal methods approach to meet temporal logic specifications in traffic control. Formal methods is an area of computer science that develops efficient techniques for proving the correct operation of systems, such as computer programs and digital circuits, and for designing systems that are correct by construction.  We have uncovered two key structural properties of traffic networks that make them amenable to this approach.

Abstract: Scientific challenges: How can multiple cooperative cyber-physical systems communicate and coordinate to accomplish complex high-level tasks within unknown, dynamic and adversarial environments?

Abstract: Inherent vulnerabilities of information and communication technology systems to cyber-attacks (e.g., malware) impose significant security risks to Cyber-Physical Systems (CPS). This is evidenced by a number of recent accidents. Noticeably, current distributed control of CPS is not really attack-resilient (ensuring task completion despite attacks). Although provable resilience would significantly lift the trustworthiness of CPS, existing defenses are rather ad-hoc and mainly focus on attack detection.

Abstract:  This project focuses on fundamental theory studies so to enable a scalable, correct-by-construction formal design of multi-robot systems that can guarantee the accomplishment of high-level team missions through automatic synthesis of local coordination mechanisms and control laws.

Abstract: Modern cyber-physical systems are monitored and controlled by multi-core platforms, and thermal management of multi-core chips is critical as overheated cores thereon will suffer from exponentially decaying lifetime and unacceptable performance degradation. To meet the timing and system lifetime reliability requirements under dynamic workloads and operating environment, we need a real-time thermal management (RTM) scheme that predicts run-time temperature and actuates effective thermal control without compromising task deadlines.

Abstract: Shared hardware resources like caches and memory introduce timing unpredictability for real-time systems. Worst-case execution time (WCET) analysis with shared hardware resources is often so pessimistic that the extra processing capacity of multicore systems is negated. We propose techniques to improve performance and schedulability for multicore systems.

Abstract: Objective: A powered prosthesis is one of typical cyber-physical systems (CPS) with a human-in-the-loop. The human and prosthesis interaction is highly complicated; although the human user could learn to manipulate the prosthesis, increased effort from the user would be required. The prosthesis requires tuning to minimize the user’s energy expenditure such that the user can use of and interact with the prosthesis effortlessly and with comfort.

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: Implantable Cardiac Defibrillators (ICDs) are at the forefront of preventing sudden death in patients suffering from ventricular arrhythmias. ICDs have evolved into complex Cyber-Physical Systems (CPS) which tightly sensing, hardware, and software to diagnose arrhythmias based on electrogram signals and control cardiac excitation. These devices are life-critical, yet the Verification and Validation (V&V) techniques used for establishing their safety have remained informal, and rely largely on extensive unit testing.

NSF Awards #1035603 and #1545097 seek to bring software programmability to cyber-physical Laboratories-on-a-Chip (LoCs) that combine electrowetting-on-dielectric (EWoD) technology, driven by active-matrix addressing, with integrated sensing. Compared to traditional benchtop chemistry methods, EWoD-based LoCs reduce reagent consumption and the human error through miniaturization, automation, and programmability.