My name is Zhihao Jiang. I'm currently a researcher in the Computer & Information Science Department in University of Pennsylvania.

What's New

June 2016: Invited talk at Mathworks Research Summit
May 2016: Obtained PhD degree
Jan 2016: Publication in IEEE Computer January Outlook.
Jan 2016: Publication in Foundations and Trends in Electronic Design Automation.
Oct 2015: Attending the Kick-off meeting for CyberCardia project

Research Highlights

My research focuses on the foundation for developing safe Medical Cyber-Physical Systems, which are designed to maintain or improve physiological conditions of the patients. Evaluating the safety and efficacy of medical CPS requires extensive knowledge of human physiology. In my research I used implantable cardiac devices as example to demonstrate the use of physiological modeling in closed-loop validation of implantable cardiac devices (Proceedings of IEEE'12). The physiological models enabled formal techniques like model checking to be applied to provide safety assurance of the devices (STTT'14), and can be seamlessly integrated into the development and certification process (IEEE Computer'16).

Physiological Modeling for Closed-loop Validation of Medical Devices

Closed-loop medical devices interact with patient physiologcy in closed-loop, therefore the safety and efficacy of the closed-loop devices should be evaluated within their physiological context. The biggest challenge for model-based closed-loop validation is the lack of appropriate models of the physiological context. In this work we developed a heart model structure which can be used for closed-loop validation of implantable cardiac devices.

Closed-loop Model Checking of Implantable Cardiac Devices

Closed-loop model checking of medical devices requires model(s) of the physiological context which not only general enough to capture the behaviors of physiological conditions specified in the requirement, but also expressive enough to explain the physiological phenomena. In this project we use implantable pacemaker as example to demonstrate the abstractions and refinements of physiological models during closed-loop model checking. The results can be used for risk analysis of closed-loop medical devices.

Model-based Design Framework For Closed-loop Medical Devices

A model-driven development toolchain automatically translates formally verified models, which represent over-approximations of the realistic models, into deterministic models which can interact with real controllers within realistic environments. The model translation process guarantees that the properties verified in the early stage were still satisfied, as the system model was refined. As the verified model is translated into executable code for physical implementation, it is validated using conformance testing procedures based on the initial system specification.

in silico Pre-Clinical Trials For Closed-loop Medical Devices

The ultimate closed-loop validation of the medical devices is clinical trial, in which the devices are directly used on patients. However, clinical trials are expensive both in time and money, and poorly-planned clinical trials lead to failure, which pose significant risks on the patients involved. In this project, we propose in silico pre-clinical trials, in which the devices are evaluated on a virtual patient population consists of physiological models for different patient conditions. The results of these in silico trials can be used to provide insights that can be beneficial to the actual clinical trials.