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.

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.

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.

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.

Abstract:  Understanding failure in protection system using Temporal Causal Diagrams  Situational  awareness  in  large  electrical  systems  and  eventual  fault  source  identification  and  possibly prognostics is a very challenging problem. State of the art relies on a network of protection devices that include relays to detect anomalies and engage circuit breakers to isolate the faulty component(s) in the system.

Abstract: The objective of this project is to develop a formal methods approach to traffic management. 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.

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.

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: This project addresses the impact of the integration of renewable intermittent generation and the integration of sophisticated sensing, communication, and actuation capabilities into the grid on the system’s reliability, volatility, and economic efficiency, and seeks to develop system architectures, along with associated optimization and control algorithms to balance such trade-­‐offs. The high level goals of this project can be stated as follows:

Abstract: Recent developments in nanostructures manufacturing, sensing and wireless networking, will soon enable us to deploy Flow‐based Cyber‐Physical Systems equipped with sensing and actuation capabilities for a broad range of applications.