{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:05:51Z","timestamp":1750309551958,"version":"3.41.0"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2025,4,4]],"date-time":"2025-04-04T00:00:00Z","timestamp":1743724800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Open Research Fund of Anhui Province Engineering Laboratory for Big Data Analysis and Early Warning Technology of Coal Mine Safety, China","award":["CSBD2022-ZD05"],"award-info":[{"award-number":["CSBD2022-ZD05"]}]},{"name":"Open Research Fund of Key Laboratory of Embedded System and Service Computing (Tongji University), Ministry of Education, China","award":["ESSCKF2023-02"],"award-info":[{"award-number":["ESSCKF2023-02"]}]},{"DOI":"10.13039\/501100012226","name":"Fundamental Research Funds for the Central Universities","doi-asserted-by":"crossref","award":["GK202205039"],"award-info":[{"award-number":["GK202205039"]}],"id":[{"id":"10.13039\/501100012226","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["62477029"],"award-info":[{"award-number":["62477029"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2025,5,31]]},"abstract":"<jats:p>Many Next-Generation consumer electronic devices would be distributed hybrid electronic systems, such as UAVs (Unmanned Aerial Vehicles) and smart electronic cars. The safety and risk control are the key issues for the sustainability of such consumer electronic systems. The modeling of hybrid electronic systems is difficult to be abstracted by traditional Petri Nets. This also makes the reachable marking graph unable to be applied to Petri Nets of the hybrid electronic systems. This paper proposes a novel Petri Net to model and analyze the hybrid electronic systems. We name it a Semi-continuous Colored Petri Net (SCPN) that inherits the excellent modeling capabilities and analysis methods of Petri Nets, and can formally depict hybrid quantities. In addition, we propose the construction algorithm for an SCPN reachable marking graph and prove its finiteness. Finally, we model and analyze an Adaptive Cruise Control (ACC) system of smart electronic cars as an example to prove the validity of SCPN. We use the proposed SCPN to model and analyze the running process of an ACC system under the continuous deceleration scenario of the front vehicle. The application study shows that the ACC system has logic flaws under the constant headway strategy when the front vehicle continues to decelerate. Based on this analysis, improvements to the SCPN of the ACC system are made, effectively enhancing its safety and logical correctness.<\/jats:p>","DOI":"10.1145\/3715960","type":"journal-article","created":{"date-parts":[[2025,2,10]],"date-time":"2025-02-10T16:03:32Z","timestamp":1739203412000},"page":"1-21","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Modeling of Hybrid System Based on Semi-continuous Colored Petri Net: A Case Study of Adaptive Cruise Control System"],"prefix":"10.1145","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1037-210X","authenticated-orcid":false,"given":"Wangyang","family":"Yu","sequence":"first","affiliation":[{"name":"The School of Computer Science, Shaanxi Normal University, Xi'an, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7787-5647","authenticated-orcid":false,"given":"Qi","family":"Guo","sequence":"additional","affiliation":[{"name":"The School of Computer Science, Shaanxi Normal University, Xi'an, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-5108-8657","authenticated-orcid":false,"given":"Yumeng","family":"Cheng","sequence":"additional","affiliation":[{"name":"The School of Computer Science, Shaanxi Normal University, Xian, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1013-4507","authenticated-orcid":false,"given":"Lu","family":"Liu","sequence":"additional","affiliation":[{"name":"University of Exeter Department of Computer Science, Exeter, United Kingdom of Great Britain and Northern Ireland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-6364-7600","authenticated-orcid":false,"given":"Fei","family":"Hao","sequence":"additional","affiliation":[{"name":"The School of Computer Science, Shaanxi Normal University, Xian, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1030-8311","authenticated-orcid":false,"given":"Xiaojun","family":"Zhai","sequence":"additional","affiliation":[{"name":"University of Essex School of Computer Science and Electronic Engineering, Colchester, United Kingdom of Great Britain and Northern Ireland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6628-1421","authenticated-orcid":false,"given":"Minsi","family":"Chen","sequence":"additional","affiliation":[{"name":"University of Huddersfield School of Computing and Engineering, Huddersfield, United Kingdom of Great Britain and Northern Ireland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,4,4]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"crossref","first-page":"5881","DOI":"10.1109\/CDC.2011.6161263","volume-title":"2011 50th IEEE Conference on Decision and Control and European Control Conference","author":"Basile Francesco","year":"2011","unstructured":"Francesco Basile, Pasquale Chiacchio, and Jolanda Coppola. 2011. Colored Hybrid Petri-Nets for modeling material handling systems. In 2011 50th IEEE Conference on Decision and Control and European Control Conference. 5881\u20135886."},{"key":"e_1_3_1_3_2","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1109\/WF-IoT.2019.8767292","volume-title":"2019 IEEE 5th World Forum on Internet of Things (WF-IoT)","author":"Chakraborty Tanmay","year":"2019","unstructured":"Tanmay Chakraborty, Shingo Yamaguchi, Mohd Anuaruddin Bin Ahmadon, and Soumya Kanti Datta. 2019. Modeling ACC with Cloud, Clouldlet for autonomous vehicle platoon using Petri nets. In 2019 IEEE 5th World Forum on Internet of Things (WF-IoT). 111\u2013116."},{"key":"e_1_3_1_4_2","volume-title":"Design and Modeling of Adaptive Cruise Control System using Petri Nets with Fault Tolerance Capabilities","author":"Chandramohan Nivethitha Amudha","year":"2018","unstructured":"Nivethitha Amudha Chandramohan. 2018. Design and Modeling of Adaptive Cruise Control System using Petri Nets with Fault Tolerance Capabilities. Purdue University."},{"key":"e_1_3_1_5_2","volume-title":"Stochastic Petri Nets and System Performance Evaluation","author":"Chuang Lin","year":"2005","unstructured":"Lin Chuang. 2005. Stochastic Petri Nets and System Performance Evaluation. Beijing: Publishing House of Tingshua University."},{"key":"e_1_3_1_6_2","volume-title":"Discrete, Continuous, and Hybrid Petri Nets","author":"David Ren\u00e9","year":"2005","unstructured":"Ren\u00e9 David and Hassane Alla. 2005. Discrete, Continuous, and Hybrid Petri Nets. Vol. 1. Springer."},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2019.2892958"},{"issue":"2","key":"e_1_3_1_8_2","doi-asserted-by":"crossref","first-page":"510","DOI":"10.1109\/TITS.2015.2478602","article-title":"A deterministic and stochastic Petri net model for traffic-responsive signaling control in urban areas","volume":"17","author":"Febbraro Angela Di","year":"2016","unstructured":"Angela Di Febbraro, Davide Giglio, and Nicola Sacco. 2016. A deterministic and stochastic Petri net model for traffic-responsive signaling control in urban areas. IEEE Transactions on Intelligent Transportation Systems 17, 2 (2016), 510\u2013524.","journal-title":"IEEE Transactions on Intelligent Transportation Systems"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSMC.2017.2768586"},{"issue":"1","key":"e_1_3_1_10_2","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1109\/TASE.2013.2253606","article-title":"Freeway traffic modeling and control in a First-Order Hybrid Petri Net framework","volume":"11","author":"Fanti Maria Pia","year":"2014","unstructured":"Maria Pia Fanti, Giorgio Iacobellis, Agostino Marcello Mangini, and Walter Ukovich. 2014. Freeway traffic modeling and control in a First-Order Hybrid Petri Net framework. IEEE Transactions on Automation Science and Engineering 11, 1 (2014), 90\u2013102.","journal-title":"IEEE Transactions on Automation Science and Engineering"},{"issue":"6","key":"e_1_3_1_11_2","doi-asserted-by":"crossref","first-page":"1027","DOI":"10.1109\/TLA.2017.7932689","article-title":"Hybrid system control using discrete state space analysis","volume":"15","author":"Favela A.","year":"2017","unstructured":"A. Favela and D. Capriles. 2017. Hybrid system control using discrete state space analysis. IEEE Latin America Transactions 15, 6 (2017), 1027\u20131033.","journal-title":"IEEE Latin America Transactions"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCST.2014.2303134"},{"issue":"7","key":"e_1_3_1_13_2","doi-asserted-by":"crossref","first-page":"3092","DOI":"10.1109\/TAC.2019.2947650","article-title":"Divergence properties of labeled Petri nets and their relevance for diagnosability analysis","volume":"65","author":"Giua Alessandro","year":"2019","unstructured":"Alessandro Giua, St\u00e9phane Lafortune, and Carla Seatzu. 2019. Divergence properties of labeled Petri nets and their relevance for diagnosability analysis. IEEE Trans. Automat. Control 65, 7 (2019), 3092\u20133097.","journal-title":"IEEE Trans. Automat. Control"},{"key":"e_1_3_1_14_2","doi-asserted-by":"crossref","first-page":"2305","DOI":"10.1109\/ITSC.2019.8917017","volume-title":"2019 IEEE Intelligent Transportation Systems Conference (ITSC)","author":"G\u00f3mez-Huelamo Carlos","year":"2019","unstructured":"Carlos G\u00f3mez-Huelamo, Luis M. Bergasa, Rafael Barea, Elena L\u00f3pez-Guill\u00e9n, Felipe Arango, and Pablo S\u00e1nchez. 2019. Simulating use cases for the UAH autonomous electric car. In 2019 IEEE Intelligent Transportation Systems Conference (ITSC). IEEE, 2305\u20132311."},{"issue":"3","key":"e_1_3_1_15_2","first-page":"1271","article-title":"Modeling and analysis of cyber\u2013physical system based on Object-Oriente Generalized Stochastic Petri net","volume":"70","author":"Hu Haiyang","year":"2020","unstructured":"Haiyang Hu, Jiawei Yu, Zhongjin Li, Jie Chen, and Hua Hu. 2020. Modeling and analysis of cyber\u2013physical system based on Object-Oriente Generalized Stochastic Petri net. IEEE Transactions on Reliability 70, 3 (2020), 1271\u20131285.","journal-title":"IEEE Transactions on Reliability"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/TITS.2018.2841967"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/b95112"},{"key":"e_1_3_1_18_2","doi-asserted-by":"crossref","first-page":"2499","DOI":"10.1109\/CAC.2018.8623507","volume-title":"2018 Chinese Automation Congress (CAC)","author":"Jiang Lei","year":"2018","unstructured":"Lei Jiang, EnLiang Liu, Ding Lui, and Jia Zhai. 2018. Modeling and control of BUCK circuit based on hybrid automata. In 2018 Chinese Automation Congress (CAC). 2499\u20132502."},{"issue":"4","key":"e_1_3_1_19_2","doi-asserted-by":"crossref","first-page":"921","DOI":"10.1109\/TR.2012.2221031","article-title":"A multistate physics model of component degradation based on stochastic Petri nets and simulation","volume":"61","author":"Li Yan-Fu","year":"2012","unstructured":"Yan-Fu Li, Enrico Zio, and Yan-Hui Lin. 2012. A multistate physics model of component degradation based on stochastic Petri nets and simulation. IEEE Transactions on Reliability 61, 4 (2012), 921\u2013931.","journal-title":"IEEE Transactions on Reliability"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2011.231"},{"key":"e_1_3_1_21_2","first-page":"89","volume-title":"2011 IEEE 3rd International Conference on Communication Software and Networks","author":"Lu Xiao-li","year":"2011","unstructured":"Xiao-li Lu, Yun-wei Dong, Bo Sun, and Hong-bin Zhao. 2011. Research of embedded software testing method based on AADL modes. In 2011 IEEE 3rd International Conference on Communication Software and Networks. IEEE, 89\u201392."},{"issue":"6","key":"e_1_3_1_22_2","first-page":"2662","article-title":"Computation of admissible marking sets in weighted synchronization-free Petri nets by dynamic programming","volume":"65","author":"Ma Ziyue","year":"2019","unstructured":"Ziyue Ma, Guanghui Zhu, Zhiwu Li, and Alessandro Giua. 2019. Computation of admissible marking sets in weighted synchronization-free Petri nets by dynamic programming. IEEE Trans. Automat. Control 65, 6 (2019), 2662\u20132669.","journal-title":"IEEE Trans. Automat. Control"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2017.2772787"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSMC.2018.2861718"},{"issue":"3","key":"e_1_3_1_25_2","first-page":"1208","article-title":"A control approach based on Colored Hybrid Petri nets and (Max, +) algebra: Application to multimodal transportation systems","volume":"17","author":"Outafraout Karima","year":"2020","unstructured":"Karima Outafraout, Ahmed Nait-Sidi-Moh, and El Houcine Chakir El Alaoui. 2020. A control approach based on Colored Hybrid Petri nets and (Max, +) algebra: Application to multimodal transportation systems. IEEE Transactions on Automation Science and Engineering 17, 3 (2020), 1208\u20131220.","journal-title":"IEEE Transactions on Automation Science and Engineering"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exn070"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSMC.2018.2837643"},{"key":"e_1_3_1_28_2","doi-asserted-by":"crossref","first-page":"245","DOI":"10.23919\/MIXDES49814.2020.9155806","volume-title":"2020 27th International Conference on Mixed Design of Integrated Circuits and System (MIXDES)","author":"Szmuc Tomasz","year":"2020","unstructured":"Tomasz Szmuc and Wojciech Szmuc. 2020. Consistency preserving development of embedded systems using AADL. In 2020 27th International Conference on Mixed Design of Integrated Circuits and System (MIXDES). 245\u2013248."},{"issue":"9","key":"e_1_3_1_29_2","doi-asserted-by":"crossref","first-page":"1231","DOI":"10.1109\/TSMC.2014.2387097","article-title":"Stochastic hybrid approximations of Markovian Petri nets","volume":"45","author":"Vazquez Carlos R.","year":"2015","unstructured":"Carlos R. Vazquez and Manuel Silva. 2015. Stochastic hybrid approximations of Markovian Petri nets. IEEE Transactions on Systems, Man, and Cybernetics: Systems 45, 9 (2015), 1231\u20131244.","journal-title":"IEEE Transactions on Systems, Man, and Cybernetics: Systems"},{"key":"e_1_3_1_30_2","first-page":"1726","volume-title":"2018 Eighth International Conference on Instrumentation Measurement, Computer, Communication and Control (IMCCC)","author":"Wang Bohan","year":"2018","unstructured":"Bohan Wang, Wenjun Ke, Jianwei Zhang, Xinrui Gao, Jing Chen, Kunlong Wang, Yuting Yang, and Yifei Da. 2018. A method of software system security verification and evaluation based on extension of AADL model. In 2018 Eighth International Conference on Instrumentation Measurement, Computer, Communication and Control (IMCCC). 1726\u20131731."},{"key":"e_1_3_1_31_2","first-page":"481","volume-title":"2019 12th IEEE Conference on Software Testing, Validation and Verification (ICST)","author":"Wei Xiaomin","year":"2019","unstructured":"Xiaomin Wei. 2019. AADL-based safety analysis approaches for safety-critical systems. In 2019 12th IEEE Conference on Software Testing, Validation and Verification (ICST). 481\u2013482."},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSMC.2013.2248358"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSMC.2016.2598287"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2014.2362819"},{"issue":"1","key":"e_1_3_1_35_2","doi-asserted-by":"crossref","first-page":"154","DOI":"10.21629\/JSEE.2019.01.15","article-title":"Useful life prediction using a stochastic hybrid automata model for an ACS multi-gyro subsystem","volume":"30","author":"Yuehua Cheng","year":"2019","unstructured":"Cheng Yuehua, Jiang Liang, Jiang Bin, and Lu Ningyun. 2019. Useful life prediction using a stochastic hybrid automata model for an ACS multi-gyro subsystem. Journal of Systems Engineering and Electronics 30, 1 (2019), 154\u2013166.","journal-title":"Journal of Systems Engineering and Electronics"},{"key":"e_1_3_1_36_2","doi-asserted-by":"crossref","first-page":"4121","DOI":"10.1109\/CCDC.2018.8407840","volume-title":"2018 Chinese Control and Decision Conference (CCDC)","author":"Zhao Zhen","year":"2018","unstructured":"Zhen Zhao, Jun Zhang, Yigang Sun, and Zhexu Liu. 2018. Modeling of avionic display system for civil aircraft based on AADL. In 2018 Chinese Control and Decision Conference (CCDC). 4121\u20134126."},{"key":"e_1_3_1_37_2","unstructured":"Wu Zhehui. 2006. Petri net introduction. Beijing China Machine Process."}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3715960","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3715960","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:18:49Z","timestamp":1750295929000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3715960"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,4]]},"references-count":36,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,5,31]]}},"alternative-id":["10.1145\/3715960"],"URL":"https:\/\/doi.org\/10.1145\/3715960","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2025,4,4]]},"assertion":[{"value":"2024-05-20","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-04","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}