My name is Zhihao Jiang. I'm currently a researcher in the Electrical and Systems Engineering Department in the University of Pennsylvania.

What's New

August 2016: in silico Pre-clinical trials paper published in EMBC 2016
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.

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.