Modelling and Verification of Quarantine Management System

Muhammad Ahmed

Quarantine facilities are being used for restricting the people who are exposed to the contagious disease during any pandemic situations, such as the famous Coronavirus disease (Covid-19). For the isolation of these people in such scenarios, a management system is of utmost importance that handles various tasks related to the isolation. In this paper, we propose a conceptual model of the Quarantine Management System (QMS) that includes its various components, such as registration, disease analysis, admission, discharge and home referral. Moreover, to perform an exhaustive analysis of the system before its actual implementation, we propose to use model checking for formal modeling and verification of the QMS. In particular, we develop formal models of its various components, such as, registration, disease diagnosis, home referral, and formally verify its various important properties regarding bed allocation, isolation completion, condition stability and discharge using the PRISM model checker.


Contact Information

Muhammad Ahmed is a MS student at NUST-SEECS, under the supervision of Dr. Rabia Irfan and Dr. Adnan Rashid.