{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,27]],"date-time":"2026-06-27T16:05:39Z","timestamp":1782576339555,"version":"3.54.5"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T00:00:00Z","timestamp":1769904000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T00:00:00Z","timestamp":1769904000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2026,2]]},"DOI":"10.1007\/s10703-026-00492-x","type":"journal-article","created":{"date-parts":[[2026,2,25]],"date-time":"2026-02-25T15:33:48Z","timestamp":1772033628000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Verifying hybrid automata networks guided by task scenarios"],"prefix":"10.1007","volume":"68","author":[{"given":"Longlong","family":"Lu","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yufei","family":"Shi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Minxue","family":"Pan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xuandong","family":"Li","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,2,25]]},"reference":[{"key":"492_CR1","doi-asserted-by":"crossref","unstructured":"Henzinger TA (1996) The theory of hybrid automata. In: Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996. IEEE Computer Society, pp 278\u2013292","DOI":"10.1109\/LICS.1996.561342"},{"issue":"1","key":"492_CR2","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1109\/TETC.2013.2273219","volume":"1","author":"X Deng","year":"2013","unstructured":"Deng X, Yang Y (2013) Communication synchronization in cluster-based sensor networks for cyber-physical systems. IEEE Trans Emerging Top Comput 1(1):98\u2013110","journal-title":"IEEE Trans Emerging Top Comput"},{"issue":"2","key":"492_CR3","doi-asserted-by":"publisher","first-page":"621","DOI":"10.1016\/j.cirp.2016.06.005","volume":"65","author":"L Monostori","year":"2016","unstructured":"Monostori L, K\u00e1d\u00e1r B, Bauernhansl T, Kondoh S, Kumara S, Reinhart G, Sauer O, Schuh G, Sihn W, Ueda K (2016) Cyber-physical systems in manufacturing. Cirp Ann 65(2):621\u2013641","journal-title":"Cirp Ann"},{"issue":"5","key":"492_CR4","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"EM Clarke","year":"1994","unstructured":"Clarke EM, Grumberg O, Long DE (1994) Model checking and abstraction. ACM Trans Program Lang Syst (TOPLAS) 16(5):1512\u20131542","journal-title":"ACM Trans Program Lang Syst (TOPLAS)"},{"key":"492_CR5","doi-asserted-by":"crossref","unstructured":"Bu L, Cimatti A, Li X, Mover S, Tonetta S (2010) Model checking of hybrid systems using shallow synchronization. In: Formal techniques for distributed systems. Springer, pp 155\u2013169","DOI":"10.1007\/978-3-642-13464-7_13"},{"key":"492_CR6","doi-asserted-by":"crossref","unstructured":"Frehse G, Le Guernic C, Donz\u00e9 A, Cotton S, Ray R, Lebeltel O, Ripado R, Girard A, Dang T, Maler O (2011) SpaceEx: scalable verification of hybrid systems. In: International Conference on Computer Aided Verification. Springer, pp 379\u2013395","DOI":"10.1007\/978-3-642-22110-1_30"},{"key":"492_CR7","doi-asserted-by":"crossref","unstructured":"Cimatti A, Griggio A, Mover S, Tonetta S (2015) HyComp: an SMT-based model checker for hybrid systems. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, pp 52\u201367","DOI":"10.1007\/978-3-662-46681-0_4"},{"key":"492_CR8","doi-asserted-by":"crossref","unstructured":"Bombardelli A, Tonetta S (2022) Asynchronous composition of local interface LTL properties. In: NASA Formal Methods Symposium. Springer, pp 508\u2013526","DOI":"10.1007\/978-3-031-06773-0_27"},{"issue":"6","key":"492_CR9","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1007\/s10009-022-00665-z","volume":"24","author":"J Lee","year":"2022","unstructured":"Lee J, Bae K, \u00d6lveczky PC, Kim S, Kang M (2022) Modeling and formal analysis of virtually synchronous cyber-physical systems in aadl. Int J Softw Tools Technol Transfer 24(6):911\u2013948","journal-title":"Int J Softw Tools Technol Transf"},{"key":"492_CR10","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti A, Clarke EM, Strichman O, Zhu Y (2003) Bounded model checking","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"492_CR11","doi-asserted-by":"crossref","unstructured":"Grosu R, Huang X, Smolka SA, Tan W, Tripakis S (2006) Deep random search for efficient model checking of timed automata. In: Monterey Workshop. Springer, pp 111\u2013124","DOI":"10.1007\/978-3-540-77419-8_7"},{"key":"492_CR12","doi-asserted-by":"crossref","unstructured":"Tripakis S, Dang T (2018) Modeling, verification, and testing using timed and hybrid automata. In: Model-Based Design for Embedded Systems. CRC Press, pp 407\u2013460","DOI":"10.1201\/9781315218823-23"},{"key":"492_CR13","doi-asserted-by":"publisher","first-page":"771","DOI":"10.1016\/j.procir.2015.12.129","volume":"41","author":"R Ahmad","year":"2016","unstructured":"Ahmad R, Plapper P (2016) Safe and automated assembly process using vision assisted robot manipulator. Procedia Cirp 41:771\u2013776","journal-title":"Procedia Cirp"},{"issue":"1","key":"492_CR14","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"EA Emerson","year":"1986","unstructured":"Emerson EA, Halpern JY (1986) \u201cSometimes\u201d and \u201cnot never\u201d revisited: on branching versus linear time temporal logic. J ACM (JACM) 33(1):151\u2013178","journal-title":"J ACM (JACM)"},{"key":"492_CR15","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti A, Clarke E, Zhu Y (1999) Symbolic model checking without BDDs. In: Tools and Algorithms for the Construction and Analysis of Systems: 5th International Conference, TACAS\u201999 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS\u201999 Amsterdam, The Netherlands, March 22\u201328, 1999 Proceedings 5, Springer, pp 193\u2013207","DOI":"10.1007\/3-540-49059-0_14"},{"key":"492_CR16","doi-asserted-by":"crossref","unstructured":"De Moura L, Bj\u00dfrner N (2008) Z3: an efficient SMT solver. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"492_CR17","doi-asserted-by":"crossref","unstructured":"Hutchinson J, Whittle J, Rouncefield M, Kristoffersen S (2011) Empirical assessment of mde in industry. In: Proceedings of the 33rd International Conference on Software Engineering, pp. 471\u2013480","DOI":"10.1145\/1985793.1985858"},{"key":"492_CR18","doi-asserted-by":"crossref","unstructured":"Li X, Liu Z, Jifeng H (2004) A formal semantics of uml sequence diagram. In: 2004 Australian Software Engineering Conference. Proceedings. IEEE, pp. 168\u2013177","DOI":"10.1109\/ASWEC.2004.1290469"},{"key":"492_CR19","doi-asserted-by":"crossref","unstructured":"Harel D, Maoz S (2006) Assert and negate revisited: modal semantics for uml sequence diagrams. In: Proceedings of the 2006 International Workshop on Scenarios and State Machines: Models, Algorithms, and Tools, pp 13\u201320","DOI":"10.1145\/1138953.1138958"},{"key":"492_CR20","doi-asserted-by":"crossref","unstructured":"Pan M, Chen S, Pei Y, Zhang T, Li X (2019) Easy modelling and verification of unpredictable and preemptive interrupt-driven systems. In: 2019 IEEE\/ACM 41st International Conference on Software Engineering (ICSE). IEEE, pp 212\u2013222","DOI":"10.1109\/ICSE.2019.00037"},{"key":"492_CR21","unstructured":"St\u00f6rrle H (2004) Trace semantics of interactions in uml 2.0. J Visual Lang Comput"},{"key":"492_CR22","volume-title":"A mathematical introduction to logic","author":"HB Enderton","year":"2001","unstructured":"Enderton HB (2001) A mathematical introduction to logic. Elsevier"},{"issue":"4","key":"492_CR23","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1145\/267580.267590","volume":"29","author":"H Zhu","year":"1997","unstructured":"Zhu H, Hall PA, May JH (1997) Software unit test coverage and adequacy. Acm Comput Surv (csur) 29(4):366\u2013427","journal-title":"Acm Comput Surv (csur)"},{"key":"492_CR24","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/s10009-004-0175-4","volume":"8","author":"H Chockler","year":"2006","unstructured":"Chockler H, Kupferman O, Vardi M (2006) Coverage metrics for formal verification. Int J Softw Tools Technol Transf 8:373\u2013386","journal-title":"Int J Softw Tools Technol Transf"},{"key":"492_CR25","doi-asserted-by":"crossref","unstructured":"Auer M, Tschurtschenthaler T, Biffl S (2003) A flyweight UML modelling tool for software development in heterogeneous environments. In: 29th EUROMICRO Conference 2003, New Waves in System Architecture, 3\u20135 September 2003, Belek-Antalya, Turkey, IEEE Computer Society, pp 267\u2013272","DOI":"10.1109\/EURMIC.2003.1231600"},{"issue":"2","key":"492_CR26","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/j.entcs.2008.04.079","volume":"198","author":"L Moura","year":"2008","unstructured":"Moura L, Bj\u00dfrner N (2008) Model-based theory combination. Electron Notes Theor Comput Sci 198(2):37\u201349","journal-title":"Electron Notes Theor Comput Sci"},{"key":"492_CR27","doi-asserted-by":"crossref","unstructured":"Ge Y, De Moura L (2009) Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: International Conference on Computer Aided Verification. Springer, pp 306\u2013320","DOI":"10.1007\/978-3-642-02658-4_25"},{"key":"492_CR28","doi-asserted-by":"crossref","unstructured":"Fehnker A, Ivan\u010di\u0107 F (2004) Benchmarks for hybrid systems verification. In: International Workshop on Hybrid Systems: Computation and Control. Springer, pp 326\u2013341","DOI":"10.1007\/978-3-540-24743-2_22"},{"key":"492_CR29","doi-asserted-by":"crossref","unstructured":"Fidge C, Cook P (2005) Model checking interrupt-dependent software. In: 12th Asia-Pacific Software Engineering Conference (APSEC\u201905). IEEE, p 8","DOI":"10.1109\/APSEC.2005.80"},{"key":"492_CR30","doi-asserted-by":"crossref","unstructured":"Regehr J (2005) Random testing of interrupt-driven software. In: Proceedings of the 5th ACM International Conference on Embedded Software, pp 290\u2013298","DOI":"10.1145\/1086228.1086282"},{"key":"492_CR31","unstructured":"Kotker J, Sadigh D, Seshia SA (2011) Timing analysis of interrupt-driven programs under context bounds. In: 2011 Formal Methods in Computer-Aided Design (FMCAD). IEEE, pp 81\u201390"},{"key":"492_CR32","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/j.procir.2016.05.064","volume":"54","author":"Z Kem\u00e9ny","year":"2016","unstructured":"Kem\u00e9ny Z, Nacsa J, Erd\u0151s G, Glawar R, Sihn W, Monostori L, Ilie-Zudor E (2016) Complementary research and education opportunities\u2014a comparison of learning factory facilities and methodologies at tu wien and mta sztaki. Procedia Cirp 54:47\u201352","journal-title":"Procedia Cirp"},{"key":"492_CR33","doi-asserted-by":"crossref","unstructured":"Cortes LA, Eles P, Peng Z (2000) Formal coverification of embedded systems using model checking. In: Proceedings of the 26th Euromicro Conference. EUROMICRO 2000. Informatics: Inventing the Future, vol. 1. IEEE, pp 106\u2013113","DOI":"10.1109\/EURMIC.2000.874622"},{"key":"492_CR34","doi-asserted-by":"crossref","unstructured":"Cimatti A, Mover S, Tonetta S (2011) Hydi: a language for symbolic hybrid systems with discrete interaction. In: 2011 37th EUROMICRO Conference on Software Engineering and Advanced Applications. IEEE, pp 275\u2013278","DOI":"10.1109\/SEAA.2011.49"},{"issue":"1","key":"492_CR35","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/s10703-012-0158-0","volume":"42","author":"A Cimatti","year":"2013","unstructured":"Cimatti A, Mover S, Tonetta S (2013) Smt-based scenario verification for hybrid systems. Formal Meth Syst Des 42(1):46\u201366","journal-title":"Formal Methods System Des"},{"key":"492_CR36","unstructured":"International Telecommunication Union (1996) ITU-T Recommendation Z.120: Message Sequence Chart (MSC), vol 27. ITU-T, Geneva"},{"key":"492_CR37","doi-asserted-by":"crossref","unstructured":"Jovanovi\u0107 D, Dutertre B (2016) Property-directed k-induction. In: 2016 Formal Methods in Computer-Aided Design (FMCAD). IEEE, pp 85\u201392","DOI":"10.1109\/FMCAD.2016.7886665"},{"key":"492_CR38","doi-asserted-by":"crossref","unstructured":"Cimatti A, Mover S, Tonetta S (2012) Smt-based verification of hybrid systems. In: Twenty- Sixth AAAI Conference on Artificial Intelligence","DOI":"10.1007\/s10703-012-0158-0"},{"key":"492_CR39","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/978-3-319-48989-6_28","volume-title":"FM2016: formal methods","author":"P Kong","year":"2016","unstructured":"Kong P, Li Y, Chen X, Sun J, Sun M, Wang J (2016) Towards concolic testing for hybrid systems. In: Fitzgerald J, Heitmeyer C, Gnesi S, Philippou A (eds) FM2016: formal methods. Springer, Cham, pp 460\u2013478"},{"key":"492_CR40","doi-asserted-by":"crossref","unstructured":"Wang X, Sun J, Chen Z, Zhang P, Wang J, Lin Y (2018) Towards optimal concolic testing. In: Proceedings of the 40th International Conference on Software Engineering. ICSE\u201918. Association for Computing Machinery, New York, NY, USA, pp 291\u2013302","DOI":"10.1145\/3180155.3180177"},{"key":"492_CR41","doi-asserted-by":"crossref","unstructured":"Mihail M, Papadimitriou CH (1994) On the random walk method for protocol testing. In: Computer Aided Verification: 6th International Conference, CAV\u201994 Stanford, California, USA, June 21\u201323, 1994 Proceedings 6, Springer, pp 132\u2013141","DOI":"10.1007\/3-540-58179-0_49"},{"key":"492_CR42","doi-asserted-by":"crossref","unstructured":"Kuehlmann A, McMillan KL, Brayton RK (1999) Probabilistic state space search. In: 1999 IEEE\/ACM International Conference on Computer-Aided Design. Digest of Technical Papers (Cat. No. 99CH37051), IEEE, pp 574\u2013579","DOI":"10.1109\/ICCAD.1999.810713"},{"key":"492_CR43","doi-asserted-by":"crossref","unstructured":"Shyam S, Bertacco V (2006) Distance-guided hybrid verification with guido. In: Proceedings of the Design Automation & Test in Europe Conference, vol. 1. IEEE, pp 1\u20136","DOI":"10.1109\/DATE.2006.244050"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-026-00492-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-026-00492-x","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-026-00492-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T09:11:57Z","timestamp":1772788317000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-026-00492-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,2]]},"references-count":43,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,2]]}},"alternative-id":["492"],"URL":"https:\/\/doi.org\/10.1007\/s10703-026-00492-x","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,2]]},"assertion":[{"value":"7 June 2025","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 February 2026","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 February 2026","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"5"}}