{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,7]],"date-time":"2026-03-07T17:57:46Z","timestamp":1772906266389,"version":"3.50.1"},"reference-count":15,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2011,6,1]],"date-time":"2011-06-01T00:00:00Z","timestamp":1306886400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100002920","name":"Research Grants Council, University Grants Committee, Hong Kong","doi-asserted-by":"publisher","award":["A-PK46"],"award-info":[{"award-number":["A-PK46"]}],"id":[{"id":"10.13039\/501100002920","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002920","name":"Research Grants Council, University Grants Committee, Hong Kong","doi-asserted-by":"publisher","award":["PolyU 5245\/09E"],"award-info":[{"award-number":["PolyU 5245\/09E"]}],"id":[{"id":"10.13039\/501100002920","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004377","name":"Hong Kong Polytechnic University","doi-asserted-by":"publisher","award":["A-PJ68"],"award-info":[{"award-number":["A-PJ68"]}],"id":[{"id":"10.13039\/501100004377","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["9.08E+23"],"award-info":[{"award-number":["9.08E+23"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002855","name":"Ministry of Science and Technology of the People's Republic of China","doi-asserted-by":"publisher","award":["2009CB320702"],"award-info":[{"award-number":["2009CB320702"]}],"id":[{"id":"10.13039\/501100002855","id-type":"DOI","asserted-by":"publisher"}]},{"name":"National S&T Major Project","award":["2009z01036-001-001-3"],"award-info":[{"award-number":["2009z01036-001-001-3"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGBED Rev."],"published-print":{"date-parts":[[2011,6]]},"abstract":"<jats:p>Many<jats:italic>Cyber-Physical Systems<\/jats:italic>(CPS) are highly nondeterministic. This often makes it impractical to model and predict the complete system behavior. To address this problem, we propose that instead of offline modeling and verification, many CPS systems should be modeled and verified online, and we shall focus on the system's<jats:italic>time-bounded behavior in short-run future<\/jats:italic>, which is more describable and predictable. Meanwhile, as the system model is generated\/updated online, the verification has to be fast. It is meaningless to tell an online model is unsafe when it is already out-dated. To demonstrate the feasibility of our proposal, we study two cases of our ongoing projects, one on the modeling and verification of a train control system, and the other on a<jats:italic>Medical Device Plug-and-Play<\/jats:italic>(MDPnP) application. Both cases are about safety-critical CPS systems. Through these two cases, we exemplify how to build online models that describe the time-bounded short-run behavior of CPS systems; and we show that fast online modeling and verification is possible.<\/jats:p>","DOI":"10.1145\/2000367.2000368","type":"journal-article","created":{"date-parts":[[2011,6,28]],"date-time":"2011-06-28T17:31:10Z","timestamp":1309282270000},"page":"7-10","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":44,"title":["Toward online hybrid systems model checking of cyber-physical systems' time-bounded short-run behavior"],"prefix":"10.1145","volume":"8","author":[{"given":"Lei","family":"Bu","sequence":"first","affiliation":[{"name":"Nanjing University, Nanjing, Jiangsu, P. R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qixin","family":"Wang","sequence":"additional","affiliation":[{"name":"The Hong Kong Polytechnic University, Hung Hom, Kowloon, Hong Kong"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xin","family":"Chen","sequence":"additional","affiliation":[{"name":"Nanjing University, Nanjing, Jiangsu, P. R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Linzhang","family":"Wang","sequence":"additional","affiliation":[{"name":"Nanjing University, Nanjing, Jiangsu, P. R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tian","family":"Zhang","sequence":"additional","affiliation":[{"name":"Nanjing University, Nanjing, Jiangsu, P. R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jianhua","family":"Zhao","sequence":"additional","affiliation":[{"name":"Nanjing University, Nanjing, Jiangsu, P. R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xuandong","family":"Li","sequence":"additional","affiliation":[{"name":"Nanjing University, Nanjing, Jiangsu, P. R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2011,6]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Techniques and Roadmap","author":"Lee E.","year":"2006"},{"key":"e_1_2_1_2_1","volume-title":"MIT Press","author":"Clarke E.","year":"1999"},{"key":"e_1_2_1_3_1","volume-title":"Springer","author":"Tabuada P.","year":"2009"},{"key":"e_1_2_1_4_1","doi-asserted-by":"crossref","unstructured":"T. Henzinger \"The theory of hybrid automata \" Proc. of LICS'96 pp. 278--292 1996. T. Henzinger \"The theory of hybrid automata \" Proc. of LICS'96 pp. 278--292 1996.","DOI":"10.1109\/LICS.1996.561342"},{"key":"e_1_2_1_5_1","volume-title":"Aviation and Rail","author":"Clarke E.","year":"2008"},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","unstructured":"B. I. Silva O. Stursberg B. H. Krogh and S. Engell \"An assessment of the current status of algorithmic approaches to the verification of hybrid systems \" Proc. of CDC'01 vol. 3 pp. 2867--2874 Dec. 2001. B. I. Silva O. Stursberg B. H. Krogh and S. Engell \"An assessment of the current status of algorithmic approaches to the verification of hybrid systems \" Proc. of CDC'01 vol. 3 pp. 2867--2874 Dec. 2001.","DOI":"10.1109\/CDC.2001.980711"},{"key":"e_1_2_1_7_1","first-page":"4","article-title":"Collecting statistics over runtime executions","volume":"70","author":"Finkbeiner B.","year":"2002","journal-title":"ENTCS"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10373-5_13"},{"key":"e_1_2_1_9_1","unstructured":"L. Bu X. Chen L. Wang and X. Li Online Verification of Control Parameter Calculations in Communication Based Train Control System. {Online}. Available: {http:\/\/arxiv.org\/abs\/1101.4271} L. Bu X. Chen L. Wang and X. Li Online Verification of Control Parameter Calculations in Communication Based Train Control System . {Online}. Available: {http:\/\/arxiv.org\/abs\/1101.4271}"},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","unstructured":"L. Bu Y. Li L. Wang X. Chen and X. Li \" BACH 2: Bounded ReachAbility CHecker for Compositional Linear Hybrid Systems \" Proc. of DATE'10 pp. 1512--1517 2010. L. Bu Y. Li L. Wang X. Chen and X. Li \" BACH 2: Bounded ReachAbility CHecker for Compositional Linear Hybrid Systems \" Proc. of DATE'10 pp. 1512--1517 2010.","DOI":"10.1109\/DATE.2010.5457051"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0163-9"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1795194.1795214"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1213\/01.ane.0000265557.73688.32"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1795194.1795215"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31954-2_17"}],"container-title":["ACM SIGBED Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2000367.2000368","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2000367.2000368","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T11:00:00Z","timestamp":1750244400000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2000367.2000368"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,6]]},"references-count":15,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2011,6]]}},"alternative-id":["10.1145\/2000367.2000368"],"URL":"https:\/\/doi.org\/10.1145\/2000367.2000368","relation":{},"ISSN":["1551-3688"],"issn-type":[{"value":"1551-3688","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,6]]},"assertion":[{"value":"2011-06-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}