Abstract In a flood situation, forecast of necessary information and an effective evacuation plan are vital. Smart Flood Monitoring System-of-Systems(SoS) is a flood monitoring and rescue system. It collects information from weather forecast, flood onlookers and observers. This information is processed and then made available as alerts to the clients. The system also maintains continuous communication with the authorities for disaster management, social services, and emergency responders. Smart Flood Monitoring System-of-System synchronizes the support offered by emergency responders with the community needs. This paper presents the architecture specification and formal verification of the proposed Smart Flood Monitoring SoS. The formal model of this SoS is specified to ensure the correctness properties of safety and liveness.

References

[1] Akhtar N., “Requirements, Formal Verification and Model Transformations of an Agent-based System: A Case Study,” Computer Engineering and Intelligent Systems, vol. 5, no. 3, pp. 1-16, 2014.

[2] Akhtar N. and Missen M., “Contribution to the Formal Specification and Verification of a Multi- Agent Robotic System,” European Journal of Scientific Research, vol. 117, no. 1, pp. 35-55, 2014.

[3] Akhtar N. and Missen M., “Practical Application of a Light-weight Formal Implementation for Specifying a Multi-AgentRobotic System,” International Journal of Computer Science Issues, vol. 11, no. 1, pp. 247-255, 2014.

[4] Akhtar N., Guyadec Y., and Oquendo F., “Formal Specification and Verification of Multi- Agent Robotics Software Systems: A Case Study,” in Proceedings of 1st International Conference on Agents and Artificial Intelligence, Porto, pp. 475-482, 2009.

[5] Blanchard B. and Fabrycky W., Systems Engineering and Analysis, Prentice Hall, 1998.

[6] Berthomieu B. and Diaz M., “Modeling and Verification of Time Dependent Systems Using Time Petri Nets,” IEEE Transactions on 216 The International Arab Journal of Information Technology, Vol. 16, No. 2, March 2019 Software Engineering, vol. 17, no. 3, pp. 259- 273, 1991.

[7] Clarke E., Grumberg O., and Peled D., Model Checking, MIT press, 1999.

[8] Clarke E., Emerson E., and Sistla A., “Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications,” ACM Transactions on Programming Languages and Systems, vol. 8, no. 2, pp. 244-263, 1986.

[9] Clarke E., Grumberg O., and Long D., “Model Checking and Abstraction,” ACM Transactions on Programming Languages and Systems, vol. 16, no. 5, pp. 1512-1542, 1994.

[10] Clarke E., Grumberg O., Jha S., Lu Y., and Veith H., “Counter Example-Guided Abstraction Refinement for Symbolic Model Checking,” Journal ACM, vol. 50, no. 5, pp. 752-794, 2003.

[11] CPN Tools website, 2012.

[Online]. Available: http://www.cpntools.org. Last Visited, 2015.

[12] Denaro G. and Pezze M., “Petri Nets and Software Engineering,” Lecture Notes in Computer Science, Berlin, pp. 439-466, 2004.

[13] He X. and Murata T., High-level Petri nets Extensions, Analysis, and Applications, Elsevier Academic Press, 2005.

[14] Jensen K., Colored Petri Nets Basic Concepts, Analysis Methods and Practical Use, Springer- Verlag, 1997.

[15] Jensen K., Kristensen L., and Wells J., “Coloured Petri Nets and CPN Tools for Modeling and Validation of Concurrent Systems,” International Journal on Software Tools for Technology Transfer, vol. 9, no. 3, pp. 213-254, 2007.

[16] MacDonald M., Guidelines for Climate Compatible Construction and Disaster Risk Reduction in Rural Punjab, 2013.

[Online]. Available: http://cdkn.org/wp- content/uploads/2012/09/Climate-Compatible- Construction-Guidelines_Final.pdf, Last Visited, 2014.

[17] Magee J. and Kramer J., Concurrency-State Models and Java Programs, John Wiley and Sons, 2006.

[18] Merlin P. and Farber D., “Recoverability of Communication Protocols,” IEEE Transactions on Communications, vol. 24, no. 4, pp. 1036- 1043, 1976.

[19] Quielle J. and Sifakis J., “Specification and Verification of Concurrent Systems in CESAR,” in Proceedings of the 5th International Symposium on Programming, Berlin, pp. 337- 350, 1982.

[20] Wells L., Performance Analysis Using Coloured Petri Nets, PhD, University of Aarhus, 2002.

[21] Xudong H., “A Comprehensive Survey of Petri Net Modeling in Software Engineering,” International Journal of Software Engineering and Knowledge Engineering, vol. 23, no. 5, pp. 589-625, 2013. Nadeem Akhtar is working as Assistant Professor at the Department of Computer Science & IT, The Islamia University of Bahawalpur (IUB), PAKISTAN. He has a PhD from the Laboratory VALORIA of Computer Science, University of South Brittany (UBS), FRANCE with the highest honour “Tres Honorable”. He has aMasters with specialization in Information System Archite Institut Universitaire Professionnalisé Vannes, FRANCE. He is the recipient of a number of awards, scholarships and research grants i.e. Study in France 2004 French Embassy scholarship for Master studies, HEC in France, Teaching assistant for ENSIBS=million, research award in year 2014 from The Directorate of Research and Development, The Islamia University of Bahawalpur. His multi-agent systems, system-of-systems and self. Saima Khan is pursuing her MS Her research work is focused on presenting and formally verifying a SoS based model for Smart Flood Monitoring. She studied MCS from Quaid working as an Assistant Professo Women Rahim Yar Khan, Pakistan for the last 4 years. She has 12 years of teaching experience and one year experience of software development and quality assurance. She has received many certificates and medals for throughout an outstanding academic career. Above all is the President Award given to her by the President of Islamic Republic of Pakistan for her outstanding academics. Aside from teaching, she is determined for education reforms and character building of the students. Her interests include: Software Engineering, Databases, Project Management, Analysis and Design Tools.