Deadlock Verification of the Room Allocation Workflow in an EHR System Using UPPAAL
TL;DR
This study proposes a rigorous formal verification methodology based on a triple-constraint framework to prove system reliability prior to the implementation phase, and firmly establishes the proposed methodology as a highly robust and practically viable solution for evaluating complex, resource-contended clinical workflows.
Abstract
: A systematic approach is necessary to address concurrency issues, timing violations, and logical safety breaches in healthcare systems, as traditional empirical testing often fails to uncover non-deterministic flaws that can endanger patient safety. This study proposes a rigorous formal verification methodology based on a triple-constraint framework to prove system reliability prior to the implementation phase. The patient room allocation workflow was modeled as a network of Timed Automata (TA) within the UPPAAL model checker, allowing for the formal evaluation of concurrent processes and shared resources. Our methodology follows three core phases: (1) Formalization, where critical requirements are translated into Timed Computation Tree Logic (TCTL) properties targeting three pillars: temporal bounds, safety invariants (e.g., category matching), and deadlock-freedom guarantees (e.g., A ◻ ¬ deadlock ); (2) Iterative Formal Refinement, a systematic algorithm that utilizes UPPAAL to identify and eliminate design flaws by dynamically refining automata components—such as location invariants, transition guards, and synchronization channels—based on counter-example traces; and (3) Artifact Generation, where the verified formal model is systematically translated into reliable software engineering blueprints. The iterative refinement process culminated in a final TA model mathematically proven to be free from deadlocks, timelocks, and unsafe states, which was successfully scaled under high queueing loads via Statistical Model Checking (SMC). This verified mathematical blueprint was then synthesized into Unified Modeling Language (UML) design artifacts, specifically class, sequence, and state machine diagrams. By integrating a triple-constraint formal verification at the design stage, this methodology proactively prevents concurrency failures, bridging mathematical guarantees with practical software engineering. Furthermore, the comparative performance evaluation reveals that while exact state-space verification triggers Out-of-Memory (OOM) failures at merely N ≥ 6 concurrent processes due to state-space explosion, the proposed TA-SMC framework successfully neutralizes this limitation. By bridging the gap between lightweight simulation and formal rigor, our approach smoothly scales up to N = 25 concurrent processes, maintaining a strictly constant peak memory footprint of ≈ 14 MB, while simultaneously guaranteeing ≥ 99% statistical confidence for critical safety invariants. These quantitative results firmly establish the proposed methodology as a highly robust and practically viable solution for evaluating complex, resource-contended clinical workflows.