Abstract: The goals of this project include the development of real-time control for human-machine co-control of highly dynamic and potentially dangerous systems. The work focuses on formalizing the automated assessment of trust, primarily focusing on the degree to which a computer should trust a human operator. We are focusing on two experimental tasks: a) a crane operation task, where control in automation settings requires a highly skilled operator, and b) rehabilitation and training tasks.

Abstract: Correct functioning of cyber-physical systems is of critical importance. This is more so in the case of safety critical systems such as in medical or automotive applications.

Abstract: CyberPhysical Systems (CPS) that self-modify to improve performance or repair damage often rewrite the modular relationships that make system modeling or Verification and Validation (V&V) possible. In this project, we are exploring methods to create self- modifying CPS systems that, in addition to self-improving or self-repairing, are also capable of maintaining system models that support the use of V&V techniques.

Abstract: Optimization algorithms used in a real-time and safety-critical context offer the potential for considerably advancing robotic and autonomous systems by improving their ability to execute complex missions. However, this promise cannot happen without proper attention to the considerably stronger operational constraints that real time, safety-critical applications must meet, unlike their non-real-time, desktop counterparts.

Abstract: Our objective is to engineer vehicles that can collaborate on the use of a  roadway.  The protocols that define the collaboration must be provably safe, and the implementations of the protocols by different manufacturers must be guaranteed to inter­‐operate. As an example we are using a collaborative merge protocol, that assists a driver merging between two vehicles in an adjacent lane.

Abstract: This project develops a theoretical framework as well as software tools to support testing and verification of a Cyber-Physical System (CPS) within a Model-Based Design (MBD) process. The theoretical bases of the framework are stochastic optimization methods, and robustness notions of                    formal specification languages.

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.

Abstract: Traditionally, buildings have been viewed as mere energy consumers; however, with the new power grid infrastructure and distributed energy resources, buildings can not only consume energy, but they can also output energy. As a result, this project removes traditional boundaries between buildings in the same cluster or between the cluster and power grids, transforming individual smart buildings into NetZero building clusters enabled by cyber-support tools.

Abstract: The artificial pancreas (AP) is a set of increasingly sophisticated devices and algorithms that will automate the delivery of insulin to patients with type-­‐1 diabetes. While the AP concept promises to alleviate the burden posed by the self-­‐ management of blood glucose levels, it also poses significant risks arising from a combination of external disturbances such as patient meals, physical activity, sensor errors, network delays and physiological variations.

Securing critical networked cyber-physical systems (NCPSs) such as the power grid or transportation systems has emerged as a major national and global priority. The networked nature of such systems renders them vulnerable to a range of attacks both in cyber and physical domains as corroborated by recent threats such as the Energetic Bear virus.