{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:41:50Z","timestamp":1740123710658,"version":"3.37.3"},"reference-count":21,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2018,10,25]],"date-time":"2018-10-25T00:00:00Z","timestamp":1540425600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2018,10,25]],"date-time":"2018-10-25T00:00:00Z","timestamp":1540425600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Mobile Netw Appl"],"published-print":{"date-parts":[[2019,2,15]]},"DOI":"10.1007\/s11036-018-1141-9","type":"journal-article","created":{"date-parts":[[2018,10,25]],"date-time":"2018-10-25T09:52:12Z","timestamp":1540461132000},"page":"100-114","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Modeling and Verifying Basic Modules of Floodlight"],"prefix":"10.1007","volume":"24","author":[{"given":"Shuangqing","family":"Xiang","sequence":"first","affiliation":[]},{"given":"Xi","family":"Wu","sequence":"additional","affiliation":[]},{"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[]},{"given":"Wanling","family":"Xie","sequence":"additional","affiliation":[]},{"given":"Lili","family":"Xiao","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0797-0152","authenticated-orcid":false,"given":"Phan Cong","family":"Vinh","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,10,25]]},"reference":[{"key":"1141_CR1","unstructured":"ONF. https:\/\/www.opennetworking.org"},{"key":"1141_CR2","unstructured":"Floodlight. http:\/\/www.projectfloodlight.org\/floodlight"},{"key":"1141_CR3","doi-asserted-by":"publisher","unstructured":"LLDP. IEEE Std 802.1AB-2016 (Revision of IEEE Std 802.1AB- 2009). https:\/\/doi.org\/10.1109\/IEEESTD.2016.7433915","DOI":"10.1109\/IEEESTD.2016.7433915"},{"key":"1141_CR4","doi-asserted-by":"crossref","unstructured":"Al-Shaer E, Al-Haj S (2010) Flowchecker: Configuration analysis and verification of federated openflow infrastructures. In: Proceedings of the 3rd ACM Workshop on Assurable and Usable Security Configuration, SafeConfig \u201910, pp 37\u201344","DOI":"10.1145\/1866898.1866905"},{"key":"1141_CR5","unstructured":"Canini M, Venzano D, Peres\u00edni P, Kostic D, Rexford J (2012) A Nice way to test openflow applications. In: Proceedings of the 9th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2012, San Jose, CA, USA, April 25-27, 2012, pp 127\u2013140"},{"key":"1141_CR6","volume-title":"Communicating sequential processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare CAR (1985) Communicating sequential processes. Prentice-Hall, Upper Saddle River"},{"key":"1141_CR7","doi-asserted-by":"crossref","unstructured":"Hong S, Xu L, Wang H, Gu G (2015) Poisoning network visibility in software-defined networks: New attacks and countermeasures. In: 22Nd annual network and distributed system security symposium, NDSS 2015, san diego, california, USA, February 8-11, 2015","DOI":"10.14722\/ndss.2015.23283"},{"key":"1141_CR8","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1016\/j.comnet.2014.07.004","volume":"72","author":"M Jammal","year":"2014","unstructured":"Jammal M, Singh T, Shami A, Asal R, Li Y (2014) Software defined networking: State of the art and research challenges. Comput Netw 72:74\u201398","journal-title":"Comput Netw"},{"issue":"1","key":"1141_CR9","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1109\/COMST.2016.2597193","volume":"19","author":"S Khan","year":"2017","unstructured":"Khan S, Gani A, Wahab AWA, Guizani M, Khan MK (2017) Topology discovery in software defined networks: threats, taxonomy, and state-of-the-art. IEEE Commun Surv Tutorials 19(1):303\u2013324","journal-title":"IEEE Commun Surv Tutorials"},{"issue":"1","key":"1141_CR10","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1109\/JPROC.2014.2371999","volume":"103","author":"D Kreutz","year":"2015","unstructured":"Kreutz D, Ramos FMV, Ver\u00edssimo PJE, Rothenberg CE, Azodolmolky S, Uhlig S (2015) Software-defined networking: A comprehensive survey. Proc IEEE 103(1):14\u201376","journal-title":"Proc IEEE"},{"issue":"10","key":"1141_CR11","doi-asserted-by":"publisher","first-page":"659","DOI":"10.1109\/32.637148","volume":"23","author":"G Lowe","year":"1997","unstructured":"Lowe G, Roscoe AW (1997) Using CSP to detect errors in the TMN protocol. IEEE Trans Software Eng 23(10):659\u2013669","journal-title":"IEEE Trans Software Eng"},{"key":"1141_CR12","doi-asserted-by":"crossref","unstructured":"Mai H, Khurshid A, Agarwal R, Caesar M, Godfrey B, King ST (2011) Debugging the data plane with anteater. In: Proceedings of the ACM SIGCOMM 2011 Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications, Toronto, ON, Canada, August 15-19, 2011, pp 290\u2013301","DOI":"10.1145\/2043164.2018470"},{"key":"1141_CR13","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2013.03.018","volume":"81","author":"T Mazur","year":"2014","unstructured":"Mazur T, Lowe G (2014) Csp-based counter abstraction for systems with node identifiers. Sci Comput Program 81:3\u201352","journal-title":"Sci Comput Program"},{"issue":"2","key":"1141_CR14","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/1355734.1355746","volume":"38","author":"N McKeown","year":"2008","unstructured":"McKeown N, Anderson T, Balakrishnan H, Parulkar GM, Peterson LL, Rexford J, Shenker S, Turner JS (2008) Openflow: enabling innovation in campus networks. Comput Commun Rev 38(2):69\u201374","journal-title":"Comput Commun Rev"},{"key":"1141_CR15","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-258-0","volume-title":"Understanding concurrent systems. Texts in computer science","author":"AW Roscoe","year":"2010","unstructured":"Roscoe AW (2010) Understanding concurrent systems. Texts in computer science. Springer, Berlin"},{"issue":"1","key":"1141_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s11704-013-3091-5","volume":"8","author":"Y Si","year":"2014","unstructured":"Si Y, Sun J, Liu Y, Dong JS, Pang J, Zhang SJ, Yang X (2014) Model checking with fairness assumptions using PAT. Frontiers Comput Sci 8(1):1\u201316","journal-title":"Frontiers Comput Sci"},{"key":"1141_CR17","doi-asserted-by":"crossref","unstructured":"Son S, Shin S, Yegneswaran V, Porras PA, Gu G (2013) Model checking invariant security properties in openflow. In: Proceedings of IEEE International Conference on Communications, ICC 2013, Budapest, Hungary, June 9-13, 2013, pp 1974\u20131979","DOI":"10.1109\/ICC.2013.6654813"},{"key":"1141_CR18","doi-asserted-by":"crossref","unstructured":"Sun J, Liu Y, Dong JS, Pang J (2009) PAT: towards flexible verification under fairness. In: Computer aided verification, 21st international conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings, pp 709\u2013714","DOI":"10.1007\/978-3-642-02658-4_59"},{"issue":"1","key":"1141_CR19","doi-asserted-by":"publisher","first-page":"3:1","DOI":"10.1145\/2430536.2430537","volume":"22","author":"J Sun","year":"2013","unstructured":"Sun J, Liu Y, Dong JS, Liu Y, Shi L, Andr\u0117 \u00c9 (2013) Modeling and verifying hierarchical real-time systems using stateful timed CSP. ACM Trans Softw Eng Methodol 22(1):3:1\u20133:29","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"1141_CR20","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/j.future.2015.09.007","volume":"56","author":"X Wu","year":"2016","unstructured":"Wu X, Zhu H (2016) Formalization and analysis of the REST architecture from the process algebra perspective. Future Generation Comp Syst 56:153\u2013168","journal-title":"Future Generation Comp Syst"},{"issue":"1","key":"1141_CR21","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1177\/0037549707079227","volume":"83","author":"WL Yeung","year":"2007","unstructured":"Yeung WL (2007) Csp-based verification for web service orchestration and choreography. Simulation 83(1):65\u201374","journal-title":"Simulation"}],"container-title":["Mobile Networks and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11036-018-1141-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11036-018-1141-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11036-018-1141-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,13]],"date-time":"2021-07-13T20:17:00Z","timestamp":1626207420000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11036-018-1141-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10,25]]},"references-count":21,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,2,15]]}},"alternative-id":["1141"],"URL":"https:\/\/doi.org\/10.1007\/s11036-018-1141-9","relation":{},"ISSN":["1383-469X","1572-8153"],"issn-type":[{"type":"print","value":"1383-469X"},{"type":"electronic","value":"1572-8153"}],"subject":[],"published":{"date-parts":[[2018,10,25]]},"assertion":[{"value":"25 October 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}