FormalMethod

Environment Modeling During Model Checking of Cyber-Physical Systems
A domain-independent framework which can balance coverage and expressiveness of environment models during closed-loop model checking of Cyber-Physical Systems.
Guangyao Chen, Zhihao Jiang
Cite Project DOI
Environment Modeling During Model Checking of Cyber-Physical Systems
Model-based Clinical Assist System for Cardiac Ablation
Enumerate suspected heart conditions during the procedure to provide more rigorous and intuitive interpretation of current understanding of the patient’s heart, which improves the accuracy and efficiency of the diagnosis and relieves the physicians from demanding low-level reasoning.
Yutong Wu, Renzhi Tang, Eunsuk Kang, Zhihao Jiang
Cite Project DOI
Model-based Clinical Assist System for Cardiac Ablation
Property-Driven Runtime Resolution of Feature Interactions
The feature interaction problem occurs when two or more features interact and possibly conflict with each other in unexpected ways, …
SG Raghavan, K Watanabe, E Kang, CW Lin, Zhihao Jiang, S Shiraishi
Cite Project Project DOI
Property-Driven Runtime Resolution of Feature Interactions
Towards Model Checking of Implantable Cardioverter Defibrillators
Ventricular Fibrillation is a disorganized electrical excitation of the heart that results in inadequate blood flow to the body. It …
H Abbas, KJ Jang, Zhihao Jiang, R Mangharam
Cite Project Project DOI
Towards Model Checking of Implantable Cardioverter Defibrillators
The Challenges of High-Confidence Medical Device Software
Bringing new safety-critical medical devices to market faces several major challenges, but modeling and formal methods can facilitate …
Zhihao Jiang, H Abbas, KJ Jang, R Mangharam
Cite DOI
The Challenges of High-Confidence Medical Device Software
High-Confidence Medical Device Software Development
Zhihao Jiang, R Mangharam
Cite Project DOI
High-Confidence Medical Device Software Development
Safety-critical medical device development using the UPP2SF model translation tool
M Pajic, Zhihao Jiang, I Lee, O Sokolsky, R Mangharam
Cite Project Project DOI
Safety-critical medical device development using the UPP2SF model translation tool
Closed-loop verification of medical devices with model abstraction and refinement
Zhihao Jiang, M Pajic, R Alur, R Mangharam
Cite Project Project DOI
Closed-loop verification of medical devices with model abstraction and refinement
From Verification to Implementation: A Model Translation Tool and a Pacemaker Case Study
M Pajic, Zhihao Jiang, I Lee, O Sokolsky, R Mangharam
Cite Project Project DOI
From Verification to Implementation: A Model Translation Tool and a Pacemaker Case Study
Modeling and Verification of a Dual Chamber Implantable Pacemaker
The design and implementation of software for medical devices is challenging due to their rapidly increasing functionality and the …
Zhihao Jiang, M Pajic, S Moarref, R Alur, R Mangharam
Cite Project Project DOI
Modeling and Verification of a Dual Chamber Implantable Pacemaker