Formal Verification of Safety and Liveness Properties using Coloured Petri-Nets: A Flood Monitoring, Warning, and Rescue System

Abstract

Annual floods after rainy monsoon season are the most dangerous natural disaster in Pakistan that affects millions of people. It is important to specify, design, model, and implement a correct system for flood monitoring, and after-flood rescue services. The correctness of the proposed system is of vital importance. We have proposed an approach for the analysis, design, and modeling of a flood monitoring system centered on formal modeling and verification. Flood monitoring which requires the environment data starts from flood sensors, independent observers and meteorological forecasts. Information is processed to determine flood status and in real-time, this information is shared among the general public, meteorological departments and disaster management authorities. The early warning and preventions alert can minimize the aftershocks of disaster. The recommended approach uses formal modeling and verification to ensure the correctness of the system. The model takes input and systemically ensures that the liveness and safety properties hold for the proposed system. Model checking technique ensures high-quality, reliable model constructions.