Abstract: Stochastic hybrid systems are a class of stochastic models that incorporates both continuous- and discretestate dynamics. They have wide applications in modeling various processes, such as communication networks [4] and biochemical reactions [6]. In this work, we focus on continuous-time stochastic hybrid systems (CTSHS); specifically, we propose a framework using Metric Interval Temporal Logic (MITL) [1] to describe the systems’ behavior and verifying the MITL formulas via model reduction and sampling.

Abstract: Advances in power semiconductor devices have rapidly paved the way for high-frequency power electronics to the point that high-frequency distributed power systems (HFDPSs) - such as Boolean Microgrid - are increasingly becoming a practical reality, provided the effects of transmission-line length can be mitigated. However, the usage of HFDPSs has been primarily limited to the printed-circuit-board (PCB) level applications because of the transmission-line effect that a power signal encounters as it propagates through the transmission line .

Abstract:  GRID 2020: The power grid in the U.S. and many regions of the world is undergoing changes because of new technologies and government mandates. It is believed that smart meters and a smarter grid will lead to more efficient use of our infrastructure. In addition, increased renewable energy integration will provide power at low cost.

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: 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: Researchers from the University of Illinois at Urbana-Champaign in collaboration with physicians and nurses from Intensive Care Unit, Carle Foundation Hospital are developing a new initiative on engineering next generation of medical systems. This project is part of the initiative and focuses on exploring the efficient and safe operation of integrated Emergency Cyber Physical Human (ECPH) systems in emergency scenarios from the Intensive Care Unit (ICU) environment. The key requirements are:

Abstract: Modeling, analyzing and verifying real physical systems have long been a changeling task since the dynamics are usually nonlinear and the state spaces are always continuous. In this work, we use linear inequality LTL (iLTL), a temporal logic, to specify the behavior of nonlinear dynamical systems over time and propose a framework for statistical verification of temporal formulae on nonlinear systems using set oriented methods.