In Punjab Pakistan, a river flood event is the most important natural disasters that every year causes high human casualties as well as heavy economic losses. A safety-critical system should be correct, reliable, complete, consistent, and unambiguous for accurate and precise flood monitoring, prediction, as well as emergency and rescue services during or after a flood event. System correctness must be ensured in every phase of the development of a safety-critical Flood Monitoring, Prediction, and Rescue (FMPR) system. Correctness is a functional property related to the behavior of the system having sub-properties of safety and liveness. These sub-properties must also be correct, complete, consistent, and unambiguous. Rigorous mathematical based software engineering methods like formal methods are suitable for the specification, design, modeling, verification, and validation of an FMPR safety-critical system. The proposed safety-critical system for FMPR is distributed as it is based on multi-agents. This system is specified, analyzed and designed by using Gaia multi-agent methodology, which is based on organizational abstractions. Gaia role model-based agent roles are specified, regular expression based liveness properties are specified, and first-order predicate calculus based safety properties are specified. Thus, safety and liveness properties are formally specified. After the detailed design phase, the system is formally modeled and verified by Hierarchical Coloured-Petri Nets (CP-Nets). As a result, a novel formal system for the specification, analysis, design, modeling, and verification of the FMPR system is proposed. This safety-critical system is distributed based on multi-agents.
