Formal Verification of the Health Code System for Quarantine Management: A Case Study in China

Abstract

The Novel Coronavirus (COVID-19), which emerged in late 2019, was first identified in Wuhan, China. It rapidly escalated into a global pandemic, affecting millions and causing unprecedented social and economic disruptions. In response, countries worldwide adopted various containment strategies, including lockdowns, social distancing, and mandatory masks. Notably, China's rigorous Quarantine Management System (QMS) was instrumental in curbing the virus's spread. This system enforced mandatory quarantines, utilized contact tracing, and established centralized quarantine facilities for confirmed cases. Technological advancements, such as health QR codes and facial recognition, were pivotal in monitoring individuals and ensuring adherence to quarantine protocols. The system's effectiveness in containing the virus was notable and was widely mentioned in media worldwide. To ensure the reliability and effectiveness of the health code app, formal verification methods such as model checking were employed. The PRISM model checker, a state-of the-art probabilistic model checker was utilized to perform formal verification of the app's algorithms. This process involved creating a detailed mathematical model of the app's behavior and using PRISM to verify that the app adhered to the desired properties of accuracy and efficiency. The use of PRISM allowed for a rigorous analysis of the health code app, ensuring that it functioned correctly within the QMS.