{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T06:43:28Z","timestamp":1740120208850,"version":"3.37.3"},"reference-count":39,"publisher":"World Scientific Pub Co Pte Ltd","issue":"07","funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["62162014"],"award-info":[{"award-number":["62162014"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"name":"the Natural Science Foundation of Anhui Province","award":["2108085MF204"],"award-info":[{"award-number":["2108085MF204"]}]},{"name":"Abroad Visiting of Excellent Young Talents of Universities in Anhui Province","award":["GXGWFX2019022"],"award-info":[{"award-number":["GXGWFX2019022"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Soft. Eng. Knowl. Eng."],"published-print":{"date-parts":[[2024,7]]},"abstract":"<jats:p> Cyber-physical Systems (CPS) are widely used in all areas of life. Ensuring the correctness of CPS remains an enduring challenge during its development and design phases. One approach to ascertain the correctness of CPS is behavior equivalence based on bisimulation. However, whether the implementation development process develops in the right direction has an important impact on obtaining the correct system implementation. Especially, the development process of complex CPS often yields a multitude of implementation versions, the correlation among these versions partly signifies the correctness of the development process. This paper formalizes the relationship between the implementation versions and establishes a formal description of the development process progressing in the correct direction, leveraging the concept of a \u201climit idea.\u201d Initially, we introduce the concept of \u201climit bisimulation\u201d for CPS systems to delineate implementations acquired during the CPS development process. Specific limit bisimulations are demonstrated to represent distinct scenarios within the development process. Subsequently, the convergence mechanism of implementations is modeled through bisimulation limits, encapsulating the CPS\u2019s specification as the ultimate goal of obtained implementations during the development process. Finally, the congruence property of the bisimulation limit is proved, which accounts for the relation between specification and implementation versions can be decomposed into a refinement hierarchy. The limit theorem of bisimulation in CPS can help the designer and developer of CPS to comprehend the development course better. <\/jats:p>","DOI":"10.1142\/s0218194024500153","type":"journal-article","created":{"date-parts":[[2024,3,28]],"date-time":"2024-03-28T14:50:41Z","timestamp":1711637441000},"page":"1095-1134","source":"Crossref","is-referenced-by-count":0,"title":["The Evolution Mechanism of Correctness for Cyber-Physical System"],"prefix":"10.1142","volume":"34","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8247-3212","authenticated-orcid":false,"given":"Yanfang","family":"Ma","sequence":"first","affiliation":[{"name":"School of Computer Science and Information Engineering, Changzhou Institute of Technology, Changzhou 213032, P.\u00a0R.\u00a0China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3788-6904","authenticated-orcid":false,"given":"Liang","family":"Chen","sequence":"additional","affiliation":[{"name":"School of Mathematics, Changzhou Institute of Technology, Changzhou 213032, P.\u00a0R.\u00a0China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"219","published-online":{"date-parts":[[2024,5,16]]},"reference":[{"key":"S0218194024500153BIB001","doi-asserted-by":"publisher","DOI":"10.1016\/j.iotcps.2021.12.002"},{"key":"S0218194024500153BIB002","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-00244-2_2"},{"key":"S0218194024500153BIB003","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-25141-7_10"},{"key":"S0218194024500153BIB004","doi-asserted-by":"publisher","DOI":"10.1109\/ICIS.2018.8466527"},{"key":"S0218194024500153BIB005","doi-asserted-by":"publisher","DOI":"10.1145\/3486252"},{"key":"S0218194024500153BIB006","doi-asserted-by":"publisher","DOI":"10.34190\/iccws.17.1.74"},{"key":"S0218194024500153BIB007","first-page":"107","volume-title":"2019 IEEE 19th Int. Symp. High Assurance Systems Engineering","author":"Jarus N.","year":"2019"},{"key":"S0218194024500153BIB008","doi-asserted-by":"publisher","DOI":"10.1109\/IGCC.2016.7892611"},{"key":"S0218194024500153BIB009","doi-asserted-by":"publisher","DOI":"10.3390\/app8020221"},{"key":"S0218194024500153BIB010","doi-asserted-by":"publisher","DOI":"10.1007\/s12555-022-0415-y"},{"issue":"3","key":"S0218194024500153BIB011","first-page":"40","volume":"17","author":"Tuo M. F.","year":"2016","journal-title":"J. Airforce Eng. Univ. (Nat. Sci. Edn.)"},{"key":"S0218194024500153BIB012","first-page":"11","volume-title":"Proc. 3rd Int. Workshop Equation-Based Object-Oriented Model","author":"Lee E. A.","year":"2010"},{"key":"S0218194024500153BIB013","doi-asserted-by":"publisher","DOI":"10.1002\/smr.2301"},{"key":"S0218194024500153BIB014","first-page":"123","volume-title":"2022 26th Int. Conf. Engineering of Complex Computer Systems","author":"Li R.","year":"2022"},{"key":"S0218194024500153BIB015","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17244-1_15"},{"issue":"1","key":"S0218194024500153BIB016","first-page":"1","volume":"18","author":"Nenzi L.","year":"2022","journal-title":"Logical Methods Comput. Sci."},{"key":"S0218194024500153BIB017","doi-asserted-by":"publisher","DOI":"10.1155\/2022\/9403986"},{"key":"S0218194024500153BIB018","doi-asserted-by":"publisher","DOI":"10.1016\/j.neucom.2020.01.075"},{"key":"S0218194024500153BIB019","first-page":"59","volume":"1207","author":"Ouchani S.","year":"2020","journal-title":"Commun. Comput. Inf. Sci."},{"key":"S0218194024500153BIB020","first-page":"1252844","volume":"380","author":"Huang X.","year":"2020","journal-title":"Appl. Math. Comput."},{"key":"S0218194024500153BIB021","doi-asserted-by":"publisher","DOI":"10.1145\/3373270"},{"key":"S0218194024500153BIB022","doi-asserted-by":"publisher","DOI":"10.1109\/SMC.2018.00536"},{"key":"S0218194024500153BIB023","doi-asserted-by":"publisher","DOI":"10.1016\/j.sysarc.2020.101707"},{"key":"S0218194024500153BIB024","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2020.12.045"},{"key":"S0218194024500153BIB025","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-0123-3"},{"key":"S0218194024500153BIB026","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-53733-7_8"},{"key":"S0218194024500153BIB027","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00124-4"},{"key":"S0218194024500153BIB028","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.11.026"},{"issue":"13","key":"S0218194024500153BIB029","first-page":"2875","volume":"8","author":"Ma Y.","year":"2011","journal-title":"J. Inf. Comput. Sci."},{"issue":"3","key":"S0218194024500153BIB030","first-page":"626","volume":"50","author":"Ma Y. F.","year":"2013","journal-title":"J. Comput. Res. Dev."},{"key":"S0218194024500153BIB031","doi-asserted-by":"publisher","DOI":"10.1007\/s11390-013-1400-y"},{"key":"S0218194024500153BIB033","doi-asserted-by":"publisher","DOI":"10.1145\/3060140"},{"key":"S0218194024500153BIB034","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-021-00360-w"},{"key":"S0218194024500153BIB035","doi-asserted-by":"publisher","DOI":"10.3390\/a11090131"},{"volume-title":"General Topology","year":"1975","author":"Kelley J. L.","key":"S0218194024500153BIB036"},{"volume-title":"General Topology","year":"1977","author":"Engelking R.","key":"S0218194024500153BIB037"},{"key":"S0218194024500153BIB039","doi-asserted-by":"publisher","DOI":"10.1016\/j.ijar.2014.10.001"},{"key":"S0218194024500153BIB040","first-page":"213","volume-title":"Proc. 4th Int. Conf. Quantitative Logic and Soft Computing","author":"Ma Y.","year":"2016"},{"key":"S0218194024500153BIB041","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2017.08.007"}],"container-title":["International Journal of Software Engineering and Knowledge Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0218194024500153","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,30]],"date-time":"2024-07-30T01:59:03Z","timestamp":1722304743000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/10.1142\/S0218194024500153"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,5,16]]},"references-count":39,"journal-issue":{"issue":"07","published-print":{"date-parts":[[2024,7]]}},"alternative-id":["10.1142\/S0218194024500153"],"URL":"https:\/\/doi.org\/10.1142\/s0218194024500153","relation":{},"ISSN":["0218-1940","1793-6403"],"issn-type":[{"type":"print","value":"0218-1940"},{"type":"electronic","value":"1793-6403"}],"subject":[],"published":{"date-parts":[[2024,5,16]]}}}