{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:21:15Z","timestamp":1721892075085},"reference-count":14,"publisher":"World Scientific Pub Co Pte Lt","issue":"11n12","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Soft. Eng. Knowl. Eng."],"published-print":{"date-parts":[[2018,11]]},"abstract":"<jats:p> Software-Defined Networking (SDN) is an emerging architecture of computer networking. OpenFlow is considered as the first and currently most popular standard southbound interface of SDN. It is a communication protocol which enables the SDN controller to directly interact with the forwarding plane, which makes the network more flexible and programmable. The promising and widespread use makes the reliability of OpenFlow important. The OpenFlow bundle mechanism is a new mechanism proposed by OpenFlow protocol to guarantee the completeness and consistency of the messages transmitted between SDN devices like switches and controllers. In this paper, we use Communication Sequential Processes (CSP) to formally model the OpenFlow bundle mechanism. By adopting the models into the model checker Process Analysis Toolkit (PAT), we verify the relevant properties of the mechanism, including deadlock freeness, parallelism, atomicity, order property and schedulability. Our formalization and verification show that the mechanism can satisfy these properties, from which we can conclude that the mechanism offers a better way to guarantee the completeness and consistency. <\/jats:p>","DOI":"10.1142\/s0218194018400223","type":"journal-article","created":{"date-parts":[[2019,1,15]],"date-time":"2019-01-15T03:44:18Z","timestamp":1547523858000},"page":"1657-1677","source":"Crossref","is-referenced-by-count":2,"title":["Formalization and Verification of the OpenFlow Bundle Mechanism Using CSP"],"prefix":"10.1142","volume":"28","author":[{"given":"Huiwen","family":"Wang","sequence":"first","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, P. R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, P. R. China"},{"name":"School of Computer Science and Software Engineering, Shenzhen University, Shenzhen, Guangdong 518060, P. R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lili","family":"Xiao","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, P. R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuan","family":"Fei","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, P. R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"219","published-online":{"date-parts":[[2019,1,15]]},"reference":[{"key":"S0218194018400223BIB001","doi-asserted-by":"publisher","DOI":"10.1016\/j.comnet.2015.02.014"},{"key":"S0218194018400223BIB002","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2014.2371999"},{"key":"S0218194018400223BIB003","doi-asserted-by":"publisher","DOI":"10.1145\/1355734.1355746"},{"key":"S0218194018400223BIB004","doi-asserted-by":"publisher","DOI":"10.1109\/SURV.2013.081313.00105"},{"key":"S0218194018400223BIB008","doi-asserted-by":"publisher","DOI":"10.1145\/2534169.2486005"},{"key":"S0218194018400223BIB010","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"issue":"5","key":"S0218194018400223BIB014","first-page":"1","volume":"5","author":"Maulik J.","year":"2016","journal-title":"Glob. J. Res. Anal."},{"key":"S0218194018400223BIB018","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2016.2529058"},{"key":"S0218194018400223BIB020","volume-title":"Communicating Sequential Processes","author":"Hoare C. A. R.","year":"1985"},{"key":"S0218194018400223BIB021","doi-asserted-by":"publisher","DOI":"10.1109\/32.637148"},{"key":"S0218194018400223BIB022","doi-asserted-by":"publisher","DOI":"10.1007\/s11036-017-0812-2"},{"key":"S0218194018400223BIB023","doi-asserted-by":"publisher","DOI":"10.1016\/j.future.2015.09.007"},{"key":"S0218194018400223BIB024","doi-asserted-by":"publisher","DOI":"10.1002\/smr.1919"},{"key":"S0218194018400223BIB027","doi-asserted-by":"publisher","DOI":"10.1007\/s11704-013-3091-5"}],"container-title":["International Journal of Software Engineering and Knowledge Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0218194018400223","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,6]],"date-time":"2019-08-06T23:04:02Z","timestamp":1565132642000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0218194018400223"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,11]]},"references-count":14,"journal-issue":{"issue":"11n12","published-online":{"date-parts":[[2019,1,15]]},"published-print":{"date-parts":[[2018,11]]}},"alternative-id":["10.1142\/S0218194018400223"],"URL":"https:\/\/doi.org\/10.1142\/s0218194018400223","relation":{},"ISSN":["0218-1940","1793-6403"],"issn-type":[{"value":"0218-1940","type":"print"},{"value":"1793-6403","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,11]]}}}