{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T20:28:17Z","timestamp":1776284897516,"version":"3.50.1"},"reference-count":62,"publisher":"Wiley","license":[{"start":{"date-parts":[[2021,4,15]],"date-time":"2021-04-15T00:00:00Z","timestamp":1618444800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Scientific Programming"],"published-print":{"date-parts":[[2021,4,15]]},"abstract":"<jats:p>Floods after monsoon rains are frequent disasters that affect millions of lives in Pakistan. Human lives are lost, agriculture economies are destroyed, and livestock animals, houses, fruit farms, and crops are lost which are the major livelihoods of thousands of people in Punjab. Each year there are heavy rains in the monsoon season and, due to global warming, there is the rapid melting of snow in northern glaciers; these factors subsequently cause floods. There is also loss of life due to the spread of waterborne diseases and snake bites. Flood monitoring provides early detection of a flood and the calculation of its intensity, which results in reduced human life losses and economic losses. Most casualties are caused by the lack of timely real-time, authentic information about the high-risk areas, and flood intensity, speed, and direction. Therefore, the proposed approach is centered on formal modeling and verification of safety and liveness properties of flood monitoring perceivers. Each flood perceiver has several sensors. It requires the collection of information starting from the flood perceiver, observer, and environmental forecast. This information is processed to determine the flood intensity level. We have developed a CP-Nets\u2019 formal model and model-checked it. We have verified the safety and liveness properties of correctness by exhaustive verification of the system using model-based proof obligations (Event-B method using Rodin). Our objective in this research is to propose a correct, reliable, and efficient flood warning, monitoring, and rescue (WMR) SoS based on formal methods. We have used formal modeling and model-checking based on state-of-the-art hierarchical CP-Nets supported by exhaustive formal proof obligations of Event-B.<\/jats:p>","DOI":"10.1155\/2021\/6685978","type":"journal-article","created":{"date-parts":[[2021,4,16]],"date-time":"2021-04-16T03:18:17Z","timestamp":1618543097000},"page":"1-17","source":"Crossref","is-referenced-by-count":5,"title":["Formal Modeling, Proving, and Model Checking of a Flood Warning, Monitoring, and Rescue System-of-Systems"],"prefix":"10.1155","volume":"2021","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4855-5000","authenticated-orcid":true,"given":"Abdul","family":"Rehman","sequence":"first","affiliation":[{"name":"Department of Computer Science and IT, Virtual University of Pakistan, Lahore, 54000, Pakistan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2475-5590","authenticated-orcid":true,"given":"Nadeem","family":"Akhtar","sequence":"additional","affiliation":[{"name":"Department of Computer Science and IT, The Islamia University of Bahawalpur, Punjab 63100, Pakistan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6158-1801","authenticated-orcid":true,"given":"Omar H.","family":"Alhazmi","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Taibah University, Medina 30001, Saudi Arabia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","reference":[{"key":"1"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.14662\/IJELC2015.037"},{"key":"3","volume-title":"Safety Critical Computer Systems","author":"N. R. Storrey","year":"1996"},{"key":"4"},{"key":"5"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/8811.001.0001"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.9783642002830"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0038-x"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050021"},{"key":"10","first-page":"203","article-title":"A brief introduction to coloured petri nets","author":"K. Jensen"},{"key":"11","article-title":"Coloured petri nets. Basic concepts, analysis methods and practical use","volume-title":"Practical Use","author":"K. Jensen","year":"1997"},{"key":"12","article-title":"Coloured petri nets. Basic concepts, analysis methods and practical use","volume-title":"Analysis Methods","author":"K. Jensen","year":"1994"},{"key":"13","article-title":"Coloured petri nets. Basic concepts, analysis methods and practical use","volume-title":"Basic Concepts","author":"K. Jensen","year":"1992"},{"key":"14","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B System and Software Engineering","author":"J.-R. Abrial","year":"2010"},{"key":"15","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book","author":"J. R. Abrial","year":"1996"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0145-y"},{"key":"17","volume-title":"Rodin User\u2019s Handbook: Covers Rodin V.2.8","author":"M. Jastram","year":"2014"},{"key":"18","article-title":"Office of the deputy under secretary of defense for acquisition and technology, testimony before the house committee on armed services, subcommittee on readiness, march 13, 2008a","volume":"28","author":"C. DiPetto","year":"2010","journal-title":"As of December"},{"key":"19","doi-asserted-by":"publisher","DOI":"10.1002\/(sici)1520-6858(1998)1:4<267::aid-sys3>3.0.co;2-d"},{"key":"20","doi-asserted-by":"crossref","DOI":"10.21236\/ADA515876","volume-title":"Profiling Systems Using the Defining Characteristics of Systems of Systems (SoS)","author":"D. Firesmith","year":"2010"},{"key":"21","doi-asserted-by":"crossref","article-title":"System of systems-the meaning of of","author":"J. Boardman","DOI":"10.1109\/SYSOSE.2006.1652284"},{"key":"22","volume-title":"Ultra-Large-Scale Systems - the Software Challenge of the Future","author":"L. Northrop","year":"2006"},{"key":"23","volume-title":"Systems engineering and analysis","author":"B. S. Blanchard","year":"1990"},{"key":"24","first-page":"86","article-title":"A taxonomy-based perspective for systems of systems design methods","author":"D. A. DeLaurentis"},{"key":"25","doi-asserted-by":"crossref","DOI":"10.1002\/9781118561829","volume-title":"Formal Methods: Industrial Use from Model to the Code","author":"J.-L. Boulanger","year":"2012"},{"key":"26","volume-title":"Formal Methods Applied to Industrial Complex Systems: Implementation of the B Method","author":"Wiley","year":"2014","edition":"1st"},{"key":"27","first-page":"131","article-title":"Web-based platform for river flood monitoring","author":"A. Ribeiro"},{"key":"28","article-title":"A review on flood monitoring: design, implementation and computational modules","author":"K. P. Menon"},{"key":"29","article-title":"Vehicle traffic and flood monitoring with reroute system using Bayesian networks analysis","author":"M. I. Alipio"},{"key":"30","doi-asserted-by":"publisher","DOI":"10.1016\/j.envsoft.2014.04.007"},{"issue":"2","key":"31","article-title":"Formal architecture and verification of a smart flood monitoring system-of-systems","volume":"16","author":"N. Akhtar","year":"2018","journal-title":"The International Arab Journal of Information Technology (IAJIT)"},{"issue":"8","key":"32","first-page":"2012","article-title":"Real time wireless flood monitoring system using ultrasonic waves","volume":"3","author":"A. Rahmtalla","year":"2014","journal-title":"International Journal of Science and Research"},{"issue":"2","key":"33","first-page":"227","article-title":"Real-time flood monitoring and warning system","volume":"33","author":"J. Sunkpho","year":"2011","journal-title":"Songklanakarin Journal of Science and Technology"},{"issue":"4","key":"34","doi-asserted-by":"crossref","DOI":"10.1145\/1592434.1592436","article-title":"Formal methods and experience","volume":"16","author":"J. Woodcock","year":"2009","journal-title":"ACM Computing Surveys"},{"key":"35","volume-title":"Model Checking","author":"E. M. Clarke","year":"2018","edition":"2nd"},{"key":"36","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-10575-8","volume-title":"Handbook of Model Checking","author":"E. M. Clarke","year":"2018","edition":"1st"},{"key":"37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_1"},{"key":"38","volume-title":"Principles of Model Checking (Representation and Mind Series)","author":"C. Baier","year":"2008"},{"key":"39","volume-title":"Model Checking","author":"E. M. Clarke","year":"1999"},{"key":"40","volume-title":"Concepts, Algorithms, and Tools for Model Checking","author":"J. Katoen","year":"1999"},{"key":"41","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/BFb0028741","article-title":"Symmetry reductions in model checking,","volume":"1427","author":"E. M. Clarke","year":"1998","journal-title":"Lecture Notes in Computer Science"},{"key":"42","first-page":"77","article-title":"Exploiting symmetries in temporal logic model checking","volume-title":"Formal Methods in System Design","author":"E. M. Clarke","year":"1996"},{"key":"43","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"44","first-page":"995","article-title":"Temporal and modal logic","volume-title":"In Handbook of Theoretical Computer Science","author":"E. A. Emerson","year":"1990"},{"key":"45","doi-asserted-by":"publisher","DOI":"10.1007\/bf00709154"},{"key":"46","first-page":"332","article-title":"An automata-theoretic approach to automatic program verification (preliminary report)","author":"M. Vardi"},{"key":"47","doi-asserted-by":"publisher","DOI":"10.1145333979.333987"},{"key":"48","first-page":"130","article-title":"A partial order approach to branching time logic model checking","author":"R. Gerth"},{"key":"49","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1016\/j.entcs.2013.02.002","article-title":"Verification of model transformations: a survey of the state-of-the-art","volume":"292","author":"D. Calegari","year":"2013","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"50","volume-title":"Concurrency: State Models and Java Programs","author":"J. Magee","year":"2006","edition":"2nd"},{"key":"51","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"M. Zohar","year":"1995"},{"key":"52","volume-title":"\u201cFairness and Priority in Progress Property Analysis,\u201d Technical Report","author":"D. Giannakopoulou","year":"1999"},{"key":"53"},{"key":"54","first-page":"257","volume-title":"\u201cArchware: Architecting Evolvable Software,\u201d in European Workshop on Software Architecture","author":"F. Oquendo","year":"2004"},{"key":"55","volume-title":"The Unified Modeling Language Reference Manual","author":"J. Rumbaugh","year":"1999"},{"key":"56"},{"key":"57","article-title":"Semantics of uml 2.0 activities with data-flow","author":"S. Harald"},{"key":"58","article-title":"Formal specification and verification of multi-agent robotics software systems: a case study","author":"N. Akhtar"},{"key":"59","article-title":"Contribution to the formal specification and verification of a multi-agent robotic system","author":"N. Akhtar","year":"2010"},{"issue":"04","key":"60","first-page":"75","article-title":"Formal requirement and architecture specifications of a multi-agent robotic system","volume":"04","author":"N. Akhtar","year":"2012","journal-title":"Journal of Computing"},{"key":"61","doi-asserted-by":"publisher","DOI":"10.1109\/access.2019.2958258"},{"key":"62","first-page":"80","article-title":"Formal verification of safety and liveness properties using coloured petri-nets: a flood monitoring, warning, and rescue system","volume-title":"Journal of Information Communication Technologies and Robotics Applications (JICTRA)","author":"N. Akhtar","year":"2018"}],"container-title":["Scientific Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/downloads.hindawi.com\/journals\/sp\/2021\/6685978.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/sp\/2021\/6685978.xml","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/sp\/2021\/6685978.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,16]],"date-time":"2021-04-16T03:18:41Z","timestamp":1618543121000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.hindawi.com\/journals\/sp\/2021\/6685978\/"}},"subtitle":[],"editor":[{"given":"Tom\u00e0s","family":"Margalef","sequence":"additional","affiliation":[],"role":[{"role":"editor","vocabulary":"crossref"}]}],"short-title":[],"issued":{"date-parts":[[2021,4,15]]},"references-count":62,"alternative-id":["6685978","6685978"],"URL":"https:\/\/doi.org\/10.1155\/2021\/6685978","relation":{},"ISSN":["1875-919X","1058-9244"],"issn-type":[{"value":"1875-919X","type":"electronic"},{"value":"1058-9244","type":"print"}],"subject":[],"published":{"date-parts":[[2021,4,15]]}}}