A formal approach towards IoT-enabled mechanism for digital polio system using Colured Petri Net

Polio remains an extreme health challenge in numerous weak and high-risk regions such as Pakistan, Afghanistan, Nigeria mainly due to ineffective monitoring and the lack of integrated digital systems for immunization organization and management. The current Polio Vaccination System (PVS) of Pakistan faces many problems and issues while eradicating poliovirus because the current system is completely paper based where data is added to sheets manually and there is a big chance of data loss. A system is efficient that make the vaccination campaign successful and remove flaws that we have faced in the current system. This research framework presents a formal approach to design and verification with integration of IoT-enabled digital polio system using Colored Petri Nets (CPNs). Its helps to leverage the IoT devices for real-time data collection, communication, and control of field-level immunization activities. With the help of modeling the system of CPNs, we ensured the formal verification of process correctness, consistency, and deadlock-free process. The model simulates interactions amongst the key mechanisms, including health workers, supervising and observing units to enable an accurate analysis of system behaviour. Formal validation through Colored Petri Nets and state space analysis confirms the reliability, correctness and scalability of the system. The approach proposes a verifiable, adaptable and flexible solution in support of the national polio eradication programs with the help of digitation, transparency, and intelligent management. The proposed system will prove efficient and flawless as compared to the current manual system because it will use a data entry device in place of a hand-held register, the security personnel with the community health workers will move Door-to-Door to vaccinate the children. Results validate the proposed model as robust a good, reliable and complete with IoT enabled smart system along Colured Petri Net and formal method.