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.
