Heart failure (HF) is a prevalent life-threatening chronic condition requiring continuous, patient-specific management. Digital twin (DT) technology offers real-time patient state modeling and predictive decision support. However, current HF DT frameworks lack formal guarantees of safety, timing, reliability, and provide limited coordination between edge devices and cloud analytics-Undermining clinical trust and deployment. We present HEDA-HF, a formally verified hybrid edge–cloud DT architecture for HF management. HEDA-HF provides design-time mathematical guarantees that all safety, liveness, and timing requirements hold across every modeled execution scenario. Every data-driven inference, alert, and synchronization event is verified at design-time against rigorously defined temporal properties before influencing patient care at the deployment time, ensuring strict adherence to safety and timing constraints. HEDA-HF explicitly embeds formal verification in the DT pipeline. The architecture is modeled as a network of timed automata and exhaustively verified in UPPAAL against Computation Tree Logic (CTL) and Timed CTL specifications. We validate HEDA-HF across five canonical HF-monitoring scenarios, confirming all functional properties across the full reachable state space. Furthermore, statistical model checking shows that critical alerts meet clinically acceptable deadlines with probability above 0.99%. By integrating mathematically proven guarantees at design time, HEDA-HF establishes a robust foundation for trustworthy clinically dependable HF DTs.
Ramdani et al. (Sun,) studied this question.