{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T06:05:30Z","timestamp":1784268330950,"version":"3.55.0"},"reference-count":31,"publisher":"IEEE","license":[{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026,5,18]]},"DOI":"10.1109\/icstw72326.2026.00036","type":"proceedings-article","created":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T21:47:20Z","timestamp":1784238440000},"page":"129-138","source":"Crossref","is-referenced-by-count":0,"title":["Verifying an Elevator Scheduling Control System"],"prefix":"10.1109","author":[{"given":"Huan","family":"Zhang","sequence":"first","affiliation":[{"name":"Maynooth University,Computer Science Department,Maynooth,Ireland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Haoyang","family":"Lu","sequence":"additional","affiliation":[{"name":"Maynooth University,Computer Science Department,Maynooth,Ireland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Long","family":"Cheng","sequence":"additional","affiliation":[{"name":"North China Electric Power University,School of Control and Computer Engineering,Beijing,China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hao","family":"Wu","sequence":"additional","affiliation":[{"name":"Maynooth University,Computer Science Department,Maynooth,Ireland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-031-72044-4_6","article-title":"Cyclone: A new tool for verifying\/testing graph-based structures","volume-title":"18th International Conference on Tests and Proofs","author":"Wu"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-75698-9_6"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/GCAT62922.2024.10924029"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/ICCS56273.2022.9988440"},{"key":"ref5","article-title":"Verification of real-time devs models","volume-title":"Proceedings of the 2009 Spring Simulation Multiconference","author":"Saadawi"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1016\/j.enbuild.2013.07.069"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07847-1"},{"key":"ref8","article-title":"The Satisfiability Modulo Theories Library (SMT-LIB)","author":"Barrett","year":"2016"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-33163-3_13"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"ref13","first-page":"547","article-title":"Opensmt2: An smt solver for multi-core and cloud computing","volume-title":"International Conference on Theory and Applications of Satisfiability Testing","author":"Hyv\u00a8arinen"},{"key":"ref14","article-title":"The Math-SAT5 SMT Solver","volume-title":"Proceedings of TACAS","volume":"7795","author":"Cimatti"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_52"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37703-7_1"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190123"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1145\/226295.226322"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/s00521-013-1391-1"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/9.376063"},{"key":"ref21","article-title":"Modeling elevator system with coloured petri nets","volume-title":"M.A.Sc. Thesis","author":"Assiri","year":"2015"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/ICSMC.2010.5642411"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/s00450-007-0032-2"},{"issue":"4","key":"ref24","first-page":"94","article-title":"Modeling distributed real-time elevator system by three model checkers","volume":"14","author":"Qian","year":"2018","journal-title":"International Journal of Online Engineering (iJOE)"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/1879021.1879024"},{"key":"ref26","article-title":"Improving elevator performance using reinforcement learning","volume":"8","author":"Crites","year":"1995","journal-title":"Advances in neural information processing systems"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1038\/s41598-024-69173-1"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2024.3417254"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-43681-9_1"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1016\/j.dam.2006.03.034"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1609\/icaps.v27i1.13799"}],"event":{"name":"2026 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW)","location":"Daejeon, Korea, Republic of","start":{"date-parts":[[2026,5,18]]},"end":{"date-parts":[[2026,5,22]]}},"container-title":["2026 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/11600400\/11600402\/11600414.pdf?arnumber=11600414","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T05:25:21Z","timestamp":1784265921000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/11600414\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,5,18]]},"references-count":31,"URL":"https:\/\/doi.org\/10.1109\/icstw72326.2026.00036","relation":{},"subject":[],"published":{"date-parts":[[2026,5,18]]}}}