{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,15]],"date-time":"2024-09-15T23:28:53Z","timestamp":1726442933426},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2017,9,13]],"date-time":"2017-09-13T00:00:00Z","timestamp":1505260800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2017,9,13]],"date-time":"2017-09-13T00:00:00Z","timestamp":1505260800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Complex Adapt Syst Model"],"published-print":{"date-parts":[[2017,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Wireless sensor and actors networks (WSANs) have become an important research area due to its large number of applications in safety, security and mission-critical systems. Natural disasters such as earthquakes and floods have distressing effects on human lives, economy and environment particularly in the developing countries due to their high population and lack of infrastructure. Earthquake is one of the major such disasters which causes a huge loss in terms of deaths, environment damages and loss of property because of its unpredictable nature. There exists much work on earthquake prediction, disaster mitigation and management but mostly is based on simulation and testing techniques which have certain limitations. Formal methods are mathematical approaches which assure correctness of systems to overcome limitations of simulation and testing techniques. That is why a formal system of earthquake disaster mitigation and management using formal methods and WSANs is proposed. Sensors and actors are deployed in the earthquakes vulnerable areas in the form of subnets which increase energy efficiency of the network as the processing becomes localized at a subnet level. Firstly, graph theory is used to represent subnet-based model which is then transformed into a formal model. Vienna Development Method-Specification Language (VDM-SL) is used to describe and prove correctness of the formal specification. The developed specification is then validated and verified through VDM-SL Toolbox facilities by analyzing the pre\/post conditions and invariants over the formal system.<\/jats:p>","DOI":"10.1186\/s40294-017-0049-8","type":"journal-article","created":{"date-parts":[[2017,9,13]],"date-time":"2017-09-13T12:21:22Z","timestamp":1505305282000},"update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Formal model of earthquake disaster mitigation and management system"],"prefix":"10.1186","volume":"5","author":[{"given":"Nazir Ahmad","family":"Zafar","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hamra","family":"Afzaal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,9,13]]},"reference":[{"key":"49_CR1","doi-asserted-by":"crossref","unstructured":"Afzaal H, Zafar NA (2016a) Towards formalism of earthquake detection and disaster reduction using WSANs. In: 14th IEEE international conference on frontiers of information technology (FIT), pp 147\u2013152","DOI":"10.1109\/FIT.2016.035"},{"issue":"1","key":"49_CR2","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1186\/s40294-016-0037-4","volume":"4","author":"H Afzaal","year":"2016","unstructured":"Afzaal H, Zafar NA (2016b) Formal analysis of subnet-based failure recovery algorithm in wireless sensor and actor and network. Complex Adapt Syst Model 4(1):27","journal-title":"Complex Adapt Syst Model"},{"key":"49_CR3","doi-asserted-by":"crossref","unstructured":"Afzaal H, Zafar NA (2016c) Robot-based forest fire detection and extinguishing model. In: 2nd IEEE international conference on\u00a0robotics and artificial intelligence (ICRAI), pp 112\u2013117","DOI":"10.1109\/ICRAI.2016.7791238"},{"key":"49_CR4","first-page":"16","volume":"34","author":"N Ahmad","year":"2011","unstructured":"Ahmad N, Riaz N, Hussain M (2011) Ad hoc wirelesses sensor network architecture for disaster survivor detection. Int J Adv Sci Technol 34:16","journal-title":"Int J Adv Sci Technol"},{"issue":"4","key":"49_CR5","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1016\/j.adhoc.2004.04.003","volume":"2","author":"IF Akyildiz","year":"2004","unstructured":"Akyildiz IF, Kasimoglu IH (2004) Wireless sensor and actor networks: research challenges. Ad Hoc Netw 2(4):351\u2013367","journal-title":"Ad Hoc Netw"},{"key":"49_CR6","first-page":"55","volume":"3","author":"I Aldasouqi","year":"2009","unstructured":"Aldasouqi I, Shaout A (2009) Earthquake monitoring system using ranger seismometer sensor. Int J Geol 3:55\u201359","journal-title":"Int J Geol"},{"key":"49_CR7","doi-asserted-by":"publisher","first-page":"140973","DOI":"10.1155\/2014\/140973","volume":"10","author":"M Alnuem","year":"2014","unstructured":"Alnuem M, Zafar NA, Imran M, Ullah S, Fayed M (2014) Formal specification and validation of a localized algorithm for segregation of critical\/noncritical nodes in MAHSNs. Int J Distrib Sens Netw 10:140973","journal-title":"Int J Distrib Sens Netw"},{"issue":"1","key":"49_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1186\/s40294-016-0038-3","volume":"4","author":"AB Altamimi","year":"2016","unstructured":"Altamimi AB, Ramadan RA (2016) Towards internet of things modeling: a gateway approach. Complex Adapt Syst Model 4(1):1\u201325","journal-title":"Complex Adapt Syst Model"},{"key":"49_CR9","doi-asserted-by":"publisher","DOI":"10.1016\/j.future.2017.03.014","author":"F Al-Turjman","year":"2017","unstructured":"Al-Turjman F (2017) Cognitive routing protocol for disaster-inspired internet of things. Future Gener Comput Syst. doi:10.1016\/j.future.2017.03.014","journal-title":"Future Gener Comput Syst"},{"issue":"5","key":"49_CR10","doi-asserted-by":"publisher","first-page":"1463","DOI":"10.1109\/JSAC.2016.2520238","volume":"34","author":"S Avallone","year":"2016","unstructured":"Avallone S, Banchs A (2016) A channel assignment and routing algorithm for energy harvesting multiradio wireless mesh networks. IEEE J Sel Areas Commun 34(5):1463\u20131476","journal-title":"IEEE J Sel Areas Commun"},{"key":"49_CR11","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1016\/j.eswa.2015.09.008","volume":"44","author":"A Bahareh","year":"2016","unstructured":"Bahareh A, Saeed J (2016) Towards modelling and runtime verification of self-organizing systems. Expert Syst Appl 44:230\u2013244","journal-title":"Expert Syst Appl"},{"issue":"1","key":"49_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1186\/s40294-017-0043-1","volume":"5","author":"K Batool","year":"2017","unstructured":"Batool K, Niazi MA (2017) Modeling the internet of things: a hybrid modeling approach using complex networks and agent-based models. Complex Adapt Syst Model 5(1):1\u20134","journal-title":"Complex Adapt Syst Model"},{"key":"49_CR13","doi-asserted-by":"crossref","unstructured":"Benkhelifa I, Nouali-Taboudjemat N, Moussaoui S (2014) Disaster management projects using wireless sensor networks: an overview. In: 28th international conference on\u00a0advanced information networking and applications workshops (WAINA), pp 605\u2013610","DOI":"10.1109\/WAINA.2014.99"},{"key":"49_CR14","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1016\/j.scico.2011.09.003","volume":"78","author":"C Carlos","year":"2012","unstructured":"Carlos C, Javier C, Gwen S (2012) Structural reconfiguration of systems under behavioral adaptation. Sci Comput Program 78:46\u201384","journal-title":"Sci Comput Program"},{"key":"49_CR15","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1016\/j.measurement.2016.11.013","volume":"97","author":"N Carreras","year":"2017","unstructured":"Carreras N, Moure D, Gom\u00e1riz S, Mihai D, M\u00e0nuel A, Ortiz R (2017) Design of a smart and wireless seismometer for volcanology monitoring. Measurement 97:174\u2013185","journal-title":"Measurement"},{"issue":"3","key":"49_CR16","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/s11276-006-5684-5","volume":"13","author":"E Cayirci","year":"2007","unstructured":"Cayirci E, Coplu T (2007) SENDROM: sensor networks for disaster relief operations management. Wireless Netw 13(3):409\u2013423","journal-title":"Wireless Netw"},{"issue":"1","key":"49_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1186\/s40294-015-0009-0","volume":"3","author":"QA Chaudhry","year":"2015","unstructured":"Chaudhry QA (2015) A Gaussian function model for simulation of complex environmental sensing. Complex Adapt Syst Model 3(1):1\u20134","journal-title":"Complex Adapt Syst Model"},{"key":"49_CR18","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1016\/j.jnca.2016.10.010","volume":"78","author":"CF Cheng","year":"2017","unstructured":"Cheng CF, Li LH (2017) Data gathering problem with the data importance consideration in Underwater Wireless Sensor Networks. J Net Comput Appl 78:300\u2013312","journal-title":"J Net Comput Appl"},{"key":"49_CR19","doi-asserted-by":"publisher","DOI":"10.4995\/Thesis\/10251\/11038","volume-title":"Dynamic evolution and reconfiguration of software architectures through aspects","author":"SC Costa","year":"2011","unstructured":"Costa SC (2011) Dynamic evolution and reconfiguration of software architectures through aspects. Department of Information System and Computation, University of Politecnica DeValencia, Valencia"},{"key":"49_CR20","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1016\/j.ijdrr.2016.01.001","volume":"16","author":"M Erd","year":"2016","unstructured":"Erd M, Schaeffer F, Kostic M, Reindl LM (2016) Event monitoring in emergency scenarios using energy efficient wireless sensor nodes for the disaster information management. Int J Disaster Risk Reduct 16:33\u201342","journal-title":"Int J Disaster Risk Reduct"},{"key":"49_CR21","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/j.comnet.2017.05.021","volume":"124","author":"M Erdelj","year":"2017","unstructured":"Erdelj M, Kr\u00f3l M, Natalizio E (2017) Wireless sensor networks and multi-UAV systems for natural disaster management. Comput Netw 124:72\u201376","journal-title":"Comput Netw"},{"key":"49_CR22","unstructured":"Faulkner M, Olson M, Chandy R, Krause J, Chandy KM, Krause A (2011) The next big one: detecting earthquakes and other rare events from community-based sensors. In: 10th international conference on\u00a0information processing in sensor networks (IPSN), pp 13\u201324"},{"key":"49_CR23","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1016\/j.future.2016.12.033","volume":"76","author":"CG Garc\u00eda","year":"2017","unstructured":"Garc\u00eda CG, Meana-Llori\u00e1n D, G-Bustelo BCP, Lovelle JMC, Garcia-Fernandez N (2017) Midgar: detection of people through computer vision in the internet of things scenarios to improve the security in smart cities, smart towns, and smart homes. Future Gener Comput Syst 76:301\u2013313","journal-title":"Future Gener Comput Syst"},{"issue":"3","key":"49_CR24","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1109\/MCOM.2010.5434384","volume":"48","author":"SM George","year":"2010","unstructured":"George SM, Zhou W, Chenji H, Won M, Lee Y, Pazarloglou A, Stoleru R, Barooah P (2010) DistressNet: a wireless ad hoc and sensor network architecture for situation management in disaster response. IEEE Commun Mag 48(3):128\u2013136","journal-title":"IEEE Commun Mag"},{"issue":"1","key":"49_CR25","first-page":"25","volume":"7","author":"N Hadj-Kacem","year":"2009","unstructured":"Hadj-Kacem N, Kacem AH, Drira K (2009) A formal model of a multi-step coordination protocol for self-adaptive software using coloured petri nets. IJCIS 7(1):25\u201339","journal-title":"IJCIS"},{"issue":"1","key":"49_CR26","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/s12559-013-9219-y","volume":"6","author":"A Hussain","year":"2014","unstructured":"Hussain A, Niazi M (2014) Toward a formal, visual framework of emergent cognitive development of scholars. Cogn Comput 6(1):113\u2013124","journal-title":"Cogn Comput"},{"key":"49_CR27","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/s11276-015-0962-8","volume":"22","author":"M Imran","year":"2016","unstructured":"Imran M, Zafar NA, Alnuem MA, Aksoy MS, Vasilakos AV (2016) Formal verification and validation of a movement control actor relocation algorithm for safety\u2014critical applications. Wireless Netw 22:247\u2013265","journal-title":"Wireless Netw"},{"issue":"1","key":"49_CR28","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s11424-006-0001-z","volume":"19","author":"HH John","year":"2006","unstructured":"John HH (2006) Studying complex adaptive systems. J Syst Sci Complex 19(1):1\u20138","journal-title":"J Syst Sci Complex"},{"issue":"8","key":"49_CR29","doi-asserted-by":"publisher","first-page":"1188","DOI":"10.1109\/LGRS.2016.2574960","volume":"13","author":"F Kahraman","year":"2016","unstructured":"Kahraman F, Imamoglu M, Ates HF (2016) Disaster damage assessment of buildings using adaptive self-similarity descriptor. IEEE Geosci Remote Sens Lett 13(8):1188\u20131192","journal-title":"IEEE Geosci Remote Sens Lett"},{"key":"49_CR30","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2011.09.004","volume":"78","author":"N Khakpour","year":"2012","unstructured":"Khakpour N, Jalili S, Talcott C, Sirjani M, Mousavi M (2012) Formal modelling of evolving self-adaptive systems. Sci Comput Program 78:3\u201326","journal-title":"Sci Comput Program"},{"key":"49_CR31","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1016\/j.comnet.2016.01.011","volume":"98","author":"EK Lee","year":"2016","unstructured":"Lee EK, Viswanathan H, Pompili D (2016) RescueNet: reinforcement-learning-based communication framework for emergency networking. Comput Netw 98:14\u201328","journal-title":"Comput Netw"},{"issue":"1","key":"49_CR32","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1186\/s40294-015-0013-4","volume":"4","author":"MA Niazi","year":"2016","unstructured":"Niazi MA (2016) Introduction to the modeling and analysis of complex systems: a review. Complex Adapt Syst Model 4(1):1\u20133","journal-title":"Complex Adapt Syst Model"},{"issue":"2","key":"49_CR33","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1109\/JSEN.2010.2068044","volume":"11","author":"M Niazi","year":"2011","unstructured":"Niazi M, Hussain A (2011) A novel agent-based simulation framework for sensing in complex adaptive environments. IEEE Sens J 11(2):404\u2013412","journal-title":"IEEE Sens J"},{"key":"49_CR34","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1016\/j.procs.2016.05.184","volume":"85","author":"M Rahman","year":"2016","unstructured":"Rahman M, Rahman S, Mansoor S, Deep V, Aashkaar M (2016) Implementation of ICT and wireless sensor networks for earthquake alert and disaster management in earthquake prone areas. Procedia Comput Sci 85:92\u201399","journal-title":"Procedia Comput Sci"},{"issue":"2","key":"49_CR35","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/s11227-009-0266-9","volume":"52","author":"S Sarmad","year":"2010","unstructured":"Sarmad S, Alade R, Arshad A, Hafiz FA, Hiroki S (2010) Modelling high assurance agent-based earthquake management system using formal techniques. J Supercomput 52(2):97\u2013118","journal-title":"J Supercomput"},{"key":"49_CR36","unstructured":"SCSK Corporation (2013) VDM Tools, User Manual, Version 9.0.2"},{"key":"49_CR37","unstructured":"SCSK Corporation (2013) VDM Tools, Language Manual, Version 9.0.2"},{"issue":"1","key":"49_CR38","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1186\/s40294-015-0007-2","volume":"3","author":"MA Shah","year":"2015","unstructured":"Shah MA, Abbas G, Dogar AB, Halim Z (2015) Scaling hierarchical clustering and energy aware routing for sensor networks. Complex Adapt Syst Model (CASM) 3(1):1\u201323","journal-title":"Complex Adapt Syst Model (CASM)"},{"key":"49_CR39","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/j.jnca.2017.02.007","volume":"84","author":"G Solmaz","year":"2017","unstructured":"Solmaz G, Turgut D (2017) Tracking pedestrians and emergent events in disaster areas. J Netw Comput Appl 84:55\u201367","journal-title":"J Netw Comput Appl"},{"key":"49_CR40","doi-asserted-by":"crossref","unstructured":"Spalazzi L, Taccari G, Bernardini A (2014) An internet of things ontology for earthquake emergency evaluation and response. In: IEEE international conference on\u00a0collaboration technologies and systems, pp 528\u2013534","DOI":"10.1109\/CTS.2014.6867619"},{"key":"49_CR41","doi-asserted-by":"crossref","unstructured":"Suzuki M, Saruwatari S, Kurata N, Morikawa H (2007) A high density earthquake monitoring system using wireless sensor networks. In: International conference on embedded network sensor system","DOI":"10.1145\/1322263.1322301"},{"key":"49_CR42","doi-asserted-by":"crossref","unstructured":"Tan R, Xing G, Chen J, Song WZ, Huang R (2010) Quality driven volcanic earthquake detection using wireless sensor network. In: Proceedings on real time system symposium","DOI":"10.1109\/RTSS.2010.21"},{"issue":"22","key":"49_CR43","doi-asserted-by":"publisher","first-page":"5226","DOI":"10.1109\/JLT.2016.2607171","volume":"34","author":"PN Tran","year":"2016","unstructured":"Tran PN, Saito H (2016) Enhancing physical network robustness against earthquake disasters with additional links. J Lightwave Technol 34(22):5226\u20135238","journal-title":"J Lightwave Technol"},{"issue":"10","key":"49_CR44","doi-asserted-by":"publisher","first-page":"2105","DOI":"10.1109\/49.957326","volume":"19","author":"H Wu","year":"2001","unstructured":"Wu H, Qiao C, De S, Tonguz O (2001) Integrated cellular and ad hoc relaying systems: icar. IEEE J Sel Areas Commun 19(10):2105\u20132115","journal-title":"IEEE J Sel Areas Commun"},{"issue":"3","key":"49_CR45","doi-asserted-by":"publisher","first-page":"868","DOI":"10.1109\/JSTARS.2016.2616511","volume":"10","author":"W Yang","year":"2017","unstructured":"Yang W, Qi W (2017) Spatial-temporal dynamic monitoring of vegetation recovery after the wenchuan earthquake. IEEE J Sel Topics Appl Earth Observ Remote Sens 10(3):868\u2013876","journal-title":"IEEE J Sel Topics Appl Earth Observ Remote Sens"},{"issue":"3","key":"49_CR46","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1134\/S0361768814030074","volume":"40","author":"AV Zhozhikashvili","year":"2014","unstructured":"Zhozhikashvili AV (2014) Monads for the formalization of a pattern matching procedure. Progr Comput Softw 40(3):117\u2013127","journal-title":"Progr Comput Softw"}],"container-title":["Complex Adaptive Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1186\/s40294-017-0049-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1186\/s40294-017-0049-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1186\/s40294-017-0049-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,30]],"date-time":"2021-07-30T06:51:07Z","timestamp":1627627867000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1186\/s40294-017-0049-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9,13]]},"references-count":46,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,12]]}},"alternative-id":["49"],"URL":"https:\/\/doi.org\/10.1186\/s40294-017-0049-8","relation":{},"ISSN":["2194-3206"],"issn-type":[{"type":"electronic","value":"2194-3206"}],"subject":[],"published":{"date-parts":[[2017,9,13]]},"assertion":[{"value":"18 July 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 August 2017","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 September 2017","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"10"}}