{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T10:58:28Z","timestamp":1769943508036,"version":"3.49.0"},"reference-count":32,"publisher":"Wiley","issue":"11","license":[{"start":{"date-parts":[[2022,7,31]],"date-time":"2022-07-31T00:00:00Z","timestamp":1659225600000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"content-domain":{"domain":["onlinelibrary.wiley.com"],"crossmark-restriction":true},"short-container-title":["Softw Pract Exp"],"published-print":{"date-parts":[[2022,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Microservices architecture provides a promising solution for developing sustainable cyber\u2010physical systems (CPSs). However, checking the compatibility of CPSs over a set of microservices communicating asynchronously via unbounded buffers are undecidable due to their infinite state spaces. In this article, we propose a new approach for checking the compatibility of CPSs with infinite state spaces without restricting the size of buffers or the number of communication cycles. First, we integrate CPSs with microservice architecture and design the system architecture for building CPSs over a set of cyber\u2010physical microservices with unbounded buffers. Second, we model CPSs composed of asynchronously communicating cyber\u2010physical microservices via FIFO buffers as labelled transition systems. Third, we adopt the stability notion and present a sufficient condition for checking the unspecified receptions of CPSs through stability checking. Finally, we implement our approach in Process Analysis Toolkit for automatic compatibility checking and conduct experiments to show our approach is effective and efficient.<\/jats:p>","DOI":"10.1002\/spe.3131","type":"journal-article","created":{"date-parts":[[2022,7,31]],"date-time":"2022-07-31T22:55:56Z","timestamp":1659308156000},"page":"2393-2410","update-policy":"https:\/\/doi.org\/10.1002\/crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Compatibility checking for cyber\u2010physical systems based on microservices"],"prefix":"10.1002","volume":"52","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6469-357X","authenticated-orcid":false,"given":"Fei","family":"Dai","sequence":"first","affiliation":[{"name":"School of Big Data and Intelligent Engineering Southwest Forestry University  Kunming China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guozhi","family":"Liu","sequence":"additional","affiliation":[{"name":"School of Big Data and Intelligent Engineering Southwest Forestry University  Kunming China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4879-9803","authenticated-orcid":false,"given":"Xiaolong","family":"Xu","sequence":"additional","affiliation":[{"name":"School of Computer and Software Nanjing University of Information Science and Technology  Nanjing China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qi","family":"Mo","sequence":"additional","affiliation":[{"name":"School of Software Yunnan University  Kunming China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhenping","family":"Qiang","sequence":"additional","affiliation":[{"name":"School of Big Data and Intelligent Engineering Southwest Forestry University  Kunming China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhihong","family":"Liang","sequence":"additional","affiliation":[{"name":"School of Big Data and Intelligent Engineering Southwest Forestry University  Kunming China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","published-online":{"date-parts":[[2022,7,31]]},"reference":[{"key":"e_1_2_13_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/COMST.2016.2627399"},{"key":"e_1_2_13_3_1","doi-asserted-by":"crossref","unstructured":"LeeEA.Cyber physical systems: design challenges. Proceedings of the 2008 11th IEEE International Symposium on Object and Component\u2010Oriented Real\u2010Time Distributed Computing (ISORC);2008:363\u2010369; IEEE.","DOI":"10.1109\/ISORC.2008.25"},{"key":"e_1_2_13_4_1","doi-asserted-by":"publisher","DOI":"10.3897\/jucs.70325"},{"key":"e_1_2_13_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2018.2887384"},{"key":"e_1_2_13_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSC.2019.2919823"},{"key":"e_1_2_13_7_1","doi-asserted-by":"crossref","unstructured":"OuederniM Sala\u00fcnG BultanT.Compatibility checking for asynchronously communicating software. Proceedings of the International Workshop on Formal Aspects of Component Software;2013:310\u2010328.","DOI":"10.1007\/978-3-319-07602-7_19"},{"key":"e_1_2_13_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSC.2019.2961346"},{"key":"e_1_2_13_9_1","unstructured":"DahmaniD BoukalaMC MountassirH ChoualiS.Compatibility control of asynchronous communicating systems with unbounded buffers. PNSE@ Petri Nets;2017:69\u201084."},{"key":"e_1_2_13_10_1","doi-asserted-by":"crossref","unstructured":"BasuS BultanT.Automatic verification of interactions in asynchronous systems with unbounded buffers. Proceedings of the 29th ACM\/IEEE International Conference on Automated Software Engineering;2014:743\u2010754.","DOI":"10.1145\/2642937.2643016"},{"key":"e_1_2_13_11_1","doi-asserted-by":"crossref","unstructured":"DarondeauP GenestB ThiagarajanP YangS.Quasi\u2010static scheduling of communicating tasks;2008:310\u2010324; Springer.","DOI":"10.1007\/978-3-540-85361-9_26"},{"key":"e_1_2_13_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2005.09.007"},{"key":"e_1_2_13_13_1","doi-asserted-by":"crossref","unstructured":"Deni\u00e9louPM YoshidaN.Buffered communication analysis in distributed multiparty sessions. Proceedings of the International Conference on Concurrency Theory;2010:343\u2010357; Springer.","DOI":"10.1007\/978-3-642-15375-4_24"},{"key":"e_1_2_13_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-013-0276-z"},{"key":"e_1_2_13_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSUSC.2017.2717807"},{"key":"e_1_2_13_16_1","doi-asserted-by":"crossref","unstructured":"WuM WangJ DeshmukhJ WangC.Shield synthesis for real: enforcing safety in cyber\u2010physical systems. Proceedings of the 2019 Formal Methods in Computer Aided Design (FMCAD);2019:129\u2010137; IEEE.","DOI":"10.23919\/FMCAD.2019.8894264"},{"key":"e_1_2_13_17_1","doi-asserted-by":"crossref","unstructured":"BringsJ.Verifying cyber\u2010physical system behavior in the context of cyber\u2010physical system\u2010networks;2017:556\u2010561; IEEE.","DOI":"10.1109\/RE.2017.45"},{"key":"e_1_2_13_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2018.2854762"},{"key":"e_1_2_13_19_1","doi-asserted-by":"publisher","DOI":"10.3390\/su13147606"},{"key":"e_1_2_13_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2160910.2160915"},{"key":"e_1_2_13_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2016.09.023"},{"key":"e_1_2_13_22_1","article-title":"Automatic analysis of complex interactions in microservice systems","volume":"2020","author":"Dai F","year":"2020","journal-title":"Complexity"},{"key":"e_1_2_13_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2020.2980891"},{"key":"e_1_2_13_24_1","doi-asserted-by":"crossref","unstructured":"ThramboulidisK VachtsevanouDC SolanosA.Cyber\u2010physical microservices: an IoT\u2010based framework for manufacturing systems. Proceedings of the 2018 IEEE Industrial Cyber\u2010Physical Systems (ICPS);2018:232\u2010239; IEEE.","DOI":"10.1109\/ICPHYS.2018.8387665"},{"key":"e_1_2_13_25_1","doi-asserted-by":"crossref","unstructured":"CanalC Sala\u00fcnG.Stability\u2010based adaptation of asynchronously communicating software. Proceedings of the International Conference on Software Engineering and Formal Methods;2016:321\u2010336; Springer.","DOI":"10.1007\/978-3-319-41591-8_22"},{"key":"e_1_2_13_26_1","doi-asserted-by":"crossref","unstructured":"SunJ LiuY DongJS PangJ.PAT: towards flexible verification under fairness. Proceedings of the International Conference on Computer Aided Verification;2009:709\u2010714; Springer.","DOI":"10.1007\/978-3-642-02658-4_59"},{"key":"e_1_2_13_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2011.03.009"},{"key":"e_1_2_13_28_1","doi-asserted-by":"crossref","unstructured":"BordeauxL Sala\u00fcnG BerardiD MecellaM.When are two web services compatible? Proceedings of the International Workshop on Technologies for E\u2010Services;2004:15\u201028; Springer.","DOI":"10.1007\/978-3-540-31811-8_2"},{"key":"e_1_2_13_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-017-0285-8"},{"key":"e_1_2_13_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.07.004"},{"key":"e_1_2_13_31_1","doi-asserted-by":"crossref","unstructured":"G\u00fcdemannM Sala\u00fcnG OuederniM.Counterexample guided synthesis of monitors for realizability enforcement. Proceedings of the International Symposium on Automated Technology for Verification and Analysis;2012:238\u2010253; Springer.","DOI":"10.1007\/978-3-642-33386-6_20"},{"key":"e_1_2_13_32_1","doi-asserted-by":"crossref","unstructured":"PoizatP Sala\u00fcnG.Checking the realizability of BPMN 2.0 choreographies. Proceedings of the 27th Annual ACM Symposium on Applied Computing;2012:1927\u20101934.","DOI":"10.1145\/2245276.2232095"},{"key":"e_1_2_13_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSC.2011.9"}],"container-title":["Software: Practice and Experience"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/spe.3131","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/full-xml\/10.1002\/spe.3131","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/spe.3131","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,22]],"date-time":"2023-08-22T10:26:20Z","timestamp":1692699980000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/spe.3131"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,7,31]]},"references-count":32,"journal-issue":{"issue":"11","published-print":{"date-parts":[[2022,11]]}},"alternative-id":["10.1002\/spe.3131"],"URL":"https:\/\/doi.org\/10.1002\/spe.3131","archive":["Portico"],"relation":{},"ISSN":["0038-0644","1097-024X"],"issn-type":[{"value":"0038-0644","type":"print"},{"value":"1097-024X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,7,31]]},"assertion":[{"value":"2020-09-08","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-07-14","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-07-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}