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, 江智浩
引用 项目 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, 江智浩
引用 项目 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, 江智浩, S Shiraishi
引用 项目 项目 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, 江智浩, R Mangharam
引用 项目 项目 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 …
江智浩, H Abbas, KJ Jang, R Mangharam
引用 DOI
The Challenges of High-Confidence Medical Device Software
High-Confidence Medical Device Software Development
This survey examines the challenges of developing high-confidence software for implantable medical devices, especially under …
江智浩, R Mangharam
引用 项目 DOI
High-Confidence Medical Device Software Development
Safety-critical medical device development using the UPP2SF model translation tool
This paper presents UPP2SF, a model-translation tool for turning verified UPPAAL models into Simulink/Stateflow models that can be …
M Pajic, 江智浩, I Lee, O Sokolsky, R Mangharam
引用 项目 项目 DOI
Safety-critical medical device development using the UPP2SF model translation tool
Closed-loop verification of medical devices with model abstraction and refinement
This paper studies closed-loop verification of medical devices in stochastic physiological environments using a dual-chamber pacemaker …
江智浩, M Pajic, R Alur, R Mangharam
引用 项目 项目 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
This paper presents UPP2SF, a model-translation tool that links formally verified UPPAAL models to Simulink/Stateflow models for …
M Pajic, 江智浩, I Lee, O Sokolsky, R Mangharam
引用 项目 项目 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 …
江智浩, M Pajic, S Moarref, R Alur, R Mangharam
引用 项目 项目 DOI
Modeling and Verification of a Dual Chamber Implantable Pacemaker