{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:34:56Z","timestamp":1750221296029,"version":"3.41.0"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2018,12,7]],"date-time":"2018-12-07T00:00:00Z","timestamp":1544140800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGSOFT Softw. Eng. Notes"],"published-print":{"date-parts":[[2018,12,7]]},"abstract":"<jats:p>By combining communication, computation, and control (3C), Cyber-Physical Systems (CPS)0tightly couple the physical world with the cyber-world, to enable more applications, enhance performance, increase dependability and etc. Among these goals, as CPS are widely used in the safety-critical area, guaranteeing the basic dependability\/safety is after all the prerequisite and often the top concern.<\/jats:p>\n          <jats:p>However, the behavior of CPS is extremely complex. First of all, due to the existence of both discrete control modes transition and continuous real-time behavior in CPS, the behavior of CPS is a complex hybrid state space, which is difficult to understand and handle. Secondly, most CPS applications are working in the open environment and acquiring real-time data from the environment intensively to adjust their own behavior. The dynamic environment makes the behavior space more complex to reason.<\/jats:p>\n          <jats:p>When a system is too complex to analyze directly, building an abstract model of the system and then conducting analysis on the model to answer questions about the original system is an important and widely-used method. Meanwhile, a reasonable model also plays important roles in the phase of specification, design, development, testing, monitoring and so on. Therefore, it is an important topic of investigating how model-based methods can be applied in the context of CPS to increase the quality and dependability of the system.<\/jats:p>\n          <jats:p>During the past decade, our research group at Nanjing University has devoted a lot of efforts into this mission. We conducted comprehensive research in a wide spectrum of CPS including model-driven design, verification, control, monitoring, and testing. In this paper, we will make a general review of the progress we made on these directions recently.<\/jats:p>","DOI":"10.1145\/3229783.3229793","type":"journal-article","created":{"date-parts":[[2018,12,7]],"date-time":"2018-12-07T19:45:00Z","timestamp":1544211900000},"page":"6-10","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Model-based Construction and Verification of Cyber-Physical Systems"],"prefix":"10.1145","volume":"43","author":[{"given":"Lei","family":"Bu","sequence":"first","affiliation":[{"name":"Nanjing University, China"}]},{"given":"Tian","family":"Zhang","sequence":"additional","affiliation":[{"name":"Nanjing University, China"}]},{"given":"Xin","family":"Chen","sequence":"additional","affiliation":[{"name":"Nanjing University, China"}]},{"given":"Linzhang","family":"Wang","sequence":"additional","affiliation":[{"name":"Nanjing University, China"}]},{"given":"Jianhua","family":"Zhao","sequence":"additional","affiliation":[{"name":"Nanjing University, China"}]},{"given":"Xuandong","family":"Li","sequence":"additional","affiliation":[{"name":"Nanjing University, China"}]}],"member":"320","published-online":{"date-parts":[[2018,12,7]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Techniques and Roadmap","author":"Lee Edward A.","year":"2006","unstructured":"Edward A. Lee . Cyber-Physical Systems - Are Computing Foundations Adequate? Position paper for National Science Foundation workshop on Cyber-Physical Systems: Research Motivation , Techniques and Roadmap , 2006 . Edward A. Lee. Cyber-Physical Systems - Are Computing Foundations Adequate? Position paper for National Science Foundation workshop on Cyber-Physical Systems: Research Motivation, Techniques and Roadmap, 2006."},{"key":"e_1_2_1_2_1","volume-title":"Analysis and Verification Challenges for Cyber-Physical Transportation Systems. National Workshop for Research on High-Confidence Transportation Cyber-Physical Systems: Automotive, Aviation and Rail","author":"Clarke Edmund M.","year":"2008","unstructured":"Edmund M. Clarke , Bruce Krogh , Andre? Platzer, Raj Rajkumar . Analysis and Verification Challenges for Cyber-Physical Transportation Systems. National Workshop for Research on High-Confidence Transportation Cyber-Physical Systems: Automotive, Aviation and Rail , 2008 . Edmund M. Clarke, Bruce Krogh, Andre? Platzer, Raj Rajkumar. Analysis and Verification Challenges for Cyber-Physical Transportation Systems. National Workshop for Research on High-Confidence Transportation Cyber-Physical Systems: Automotive, Aviation and Rail, 2008."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOSE.2007.14"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2006.58"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-008-0052-5"},{"key":"e_1_2_1_6_1","first-page":"322","volume-title":"David L. Dill. Automata for Modeling Real-Time Systems. In Proceedings of 17th International Colloquium on Automata, Languages, and Programming (ICALP1990)","author":"Alur Rajeev","year":"1990","unstructured":"Rajeev Alur , David L. Dill. Automata for Modeling Real-Time Systems. In Proceedings of 17th International Colloquium on Automata, Languages, and Programming (ICALP1990) , Warwick University, England, Lecture Notes in Computer Science 443, Springer , pp. 322 - 335 , 1990 . Rajeev Alur, David L. Dill. Automata for Modeling Real-Time Systems. In Proceedings of 17th International Colloquium on Automata, Languages, and Programming (ICALP1990), Warwick University, England, Lecture Notes in Computer Science 443, Springer, pp.322-335, 1990."},{"key":"e_1_2_1_7_1","first-page":"417","volume-title":"Guoliang Zheng. Partial Order Path Technique for Checking Parallel Timed Automata. In Proceedings of 7th International Symposium, Formal Techniques in Realtime and Fault-Tolerant Systems (FTRTFT2002)","author":"Zhao Jianhua","year":"2002","unstructured":"Jianhua Zhao , He Xu , Xuandong Li , Tao Zheng , Guoliang Zheng. Partial Order Path Technique for Checking Parallel Timed Automata. In Proceedings of 7th International Symposium, Formal Techniques in Realtime and Fault-Tolerant Systems (FTRTFT2002) , Oldenburg, Germany, Lecture Notes in Computer Science 2469, Springer , pp. 417 - 432 , 2002 . Jianhua Zhao, He Xu, Xuandong Li, Tao Zheng, Guoliang Zheng. Partial Order Path Technique for Checking Parallel Timed Automata. In Proceedings of 7th International Symposium, Formal Techniques in Realtime and Fault-Tolerant Systems (FTRTFT2002), Oldenburg, Germany, Lecture Notes in Computer Science 2469, Springer, pp.417-432, 2002."},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Jianhua Zhao Linzhang Wang Xuandong Li. A Partial Order Reduction Technique for Parallel Timed Automaton Model Checking. In Proceedings of the Third International Symposium On Leveraging Applications of Formal Methods Verification and Validation (ISoLA2008) Porto Sani Greece Communications in Computer and Information Science 17 Springer pp.262-276 2008.  Jianhua Zhao Linzhang Wang Xuandong Li. A Partial Order Reduction Technique for Parallel Timed Automaton Model Checking. In Proceedings of the Third International Symposium On Leveraging Applications of Formal Methods Verification and Validation (ISoLA2008) Porto Sani Greece Communications in Computer and Information Science 17 Springer pp.262-276 2008.","DOI":"10.1007\/978-3-540-88479-8_19"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.12.023"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_56"},{"key":"e_1_2_1_11_1","first-page":"65","volume-title":"Xuandong Li. BACH: Bounded ReachAbility CHecker for Linear Hybrid Automata. In Proceedings of the 8th International Conference on Formal Methods in Computer Aided Design (FMCAD2008)","author":"Bu Lei","year":"2008","unstructured":"Lei Bu , You Li , Linzhang Wang , Xuandong Li. BACH: Bounded ReachAbility CHecker for Linear Hybrid Automata. In Proceedings of the 8th International Conference on Formal Methods in Computer Aided Design (FMCAD2008) , Portland, Oregon, USA, IEEE Computer Society Press , pp. 65 - 68 , 2008 . Lei Bu, You Li, Linzhang Wang, Xuandong Li. BACH: Bounded ReachAbility CHecker for Linear Hybrid Automata. In Proceedings of the 8th International Conference on Formal Methods in Computer Aided Design (FMCAD2008), Portland, Oregon, USA, IEEE Computer Society Press, pp.65-68, 2008."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/3220914.3221198"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-014-0210-3"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2014.22"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2016.2604308"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11319-2_9"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3126508"},{"key":"e_1_2_1_18_1","first-page":"4331","volume-title":"Xuandong Li. Switched Linear Multi-Robot Navigation Using Hierarchical Model Predictive Control. In Proceedings of the 26th International Joint Conference on Artificial Intelligence (IJCAI2017)","author":"Huang Chao","year":"2017","unstructured":"Chao Huang , Xin Chen , Yifan Zhang , Shengchao Qin , Yifeng Zeng , Xuandong Li. Switched Linear Multi-Robot Navigation Using Hierarchical Model Predictive Control. In Proceedings of the 26th International Joint Conference on Artificial Intelligence (IJCAI2017) , Melbourne, Australia , IJCAI Press, pp. 4331 - 4337 , 2017 . Chao Huang, Xin Chen, Yifan Zhang, Shengchao Qin, Yifeng Zeng, Xuandong Li. Switched Linear Multi-Robot Navigation Using Hierarchical Model Predictive Control. In Proceedings of the 26th International Joint Conference on Artificial Intelligence (IJCAI2017), Melbourne, Australia, IJCAI Press, pp.4331-4337, 2017."},{"key":"e_1_2_1_19_1","first-page":"3140","volume-title":"Xuandong Li. Hierarchical Model Predictive Control for Multi-Robot Navigation. In Proceedings of the 25th International Joint Conference on Artificial Intelligence (IJCAI2016)","author":"Huang Chao","year":"2016","unstructured":"Chao Huang , Xin Chen , Yifan Zhang , Shengchao Qin , Yifeng Zeng , Xuandong Li. Hierarchical Model Predictive Control for Multi-Robot Navigation. In Proceedings of the 25th International Joint Conference on Artificial Intelligence (IJCAI2016) , New York, USA , IJCAI Press, pp. 3140 - 3146 , 2016 . Chao Huang, Xin Chen, Yifan Zhang, Shengchao Qin, Yifeng Zeng, Xuandong Li. Hierarchical Model Predictive Control for Multi-Robot Navigation. In Proceedings of the 25th International Joint Conference on Artificial Intelligence (IJCAI2016), New York, USA, IJCAI Press, pp.3140-3146, 2016."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2000367.2000368"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2013.50"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509553"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2532443.2532465"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2008.64"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/bxm057"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.440"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3092703.3092724"}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3229783.3229793","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3229783.3229793","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:13:11Z","timestamp":1750212791000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3229783.3229793"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,12,7]]},"references-count":27,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2018,12,7]]}},"alternative-id":["10.1145\/3229783.3229793"],"URL":"https:\/\/doi.org\/10.1145\/3229783.3229793","relation":{},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[2018,12,7]]},"assertion":[{"value":"2018-12-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}