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

  • Nadeem Akhtar Department of Computer Science and IT, The Islamia University of Bahawalpur, Pakistan
  • Abdul Rehman Department of Computer Science and IT, Virtual University of Pakistan
  • Dost Muhammad Khan Department of Computer Science and IT, The Islamia University of Bahawalpur, Pakistan
Keywords: Flood monitoring, Formal modeling, Formal verification, Safety property, Liveness property, Coloured Petri Nets (CPNs), Event-B, Rodin

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.

Published
2018-06-30
How to Cite
[1]
N. Akhtar, A. Rehman, and D. M. Khan, “Formal Verification of Safety and Liveness Properties using Coloured Petri-Nets: A Flood Monitoring, Warning, and Rescue System”, jictra, pp. 80-88, Jun. 2018.
Section
Original Articles