{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T10:07:48Z","timestamp":1767262068284,"version":"3.37.3"},"reference-count":52,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2022,2,10]],"date-time":"2022-02-10T00:00:00Z","timestamp":1644451200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,2,10]],"date-time":"2022-02-10T00:00:00Z","timestamp":1644451200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61972193"],"award-info":[{"award-number":["61972193"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2022,8]]},"DOI":"10.1007\/s10270-022-00980-8","type":"journal-article","created":{"date-parts":[[2022,2,10]],"date-time":"2022-02-10T05:04:28Z","timestamp":1644469468000},"page":"1321-1338","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Improving timing analysis effectiveness for scenario-based specifications by combining SAT and LP techniques"],"prefix":"10.1007","volume":"21","author":[{"given":"Longlong","family":"Lu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Minxue","family":"Pan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tian","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xuandong","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,2,10]]},"reference":[{"key":"980_CR1","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/3-540-61042-1_37","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Alur","year":"1996","unstructured":"Alur, R., Holzmann Gerard, J., Peled, D.: An analyzer for message sequence charts. In: Margaria, T., Steffen, B. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 35\u201348. Springer, Berlin (1996)"},{"key":"980_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Yannakakis, M.: Model checking of message sequence charts. In: Proceedings of the 10th International Conference on Concurrency Theory, CONCUR \u201999, pp. 114\u2013129. Springer, London (1999)","DOI":"10.1007\/3-540-48320-9_10"},{"key":"980_CR3","unstructured":"Andoni, A., Daniliuc, D., Khurshid, S., Marinov, D.: Evaluating the \u201csmall scope hypothesis\u201d. Technical report, MIT CSAIL (2003)"},{"issue":"5","key":"980_CR4","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1002\/smr.260","volume":"14","author":"L Andrade","year":"2002","unstructured":"Andrade, L., Fiadeiro, J.L., Gouveia, J., Koutsoukos, G.: Separating computation, coordination and configuration. J. Softw. Maint. Evol. Res. Pract. 14(5), 353\u2013369 (2002)","journal-title":"J. Softw. Maint. Evol. Res. Pract."},{"key":"980_CR5","doi-asserted-by":"crossref","unstructured":"Auer, M., Meyer, L., Biffl, S.: Explorative UML modeling-comparing the usability of UML tools. In: ICEIS (3), pp. 466\u2013473 (2007)","DOI":"10.5220\/0002351804660473"},{"key":"980_CR6","doi-asserted-by":"crossref","unstructured":"Auer, M., Tschurtschenthaler, T., Biffl, S.: A flyweight UML modelling tool for software development in heterogeneous environments. In: Proceedings of the 29th Conference on EUROMICRO, EUROMICRO \u201903, p. 267. IEEE Computer Society, Washington, DC, USA (2003). http:\/\/dl.acm.org\/citation.cfm?id=942796.943259","DOI":"10.1109\/EURMIC.2003.1231600"},{"key":"980_CR7","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-319-10575-8_11","volume-title":"Handbook of Model Checking","author":"C Barrett","year":"2018","unstructured":"Barrett, C., Tinelli, C.: Satisfiability modulo theories. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 305\u2013343. Springer, Berlin (2018)"},{"key":"980_CR8","doi-asserted-by":"crossref","unstructured":"Ben-Abdallah, H., Leue, S.: Timing constraints in message sequence chart specifications. In: Mizuno, T., Shiratori, N., Higashino, T., Togashi, A. (eds.) Formal Description Techniques and Protocol Specification, Testing and Verification, pp. 91\u2013106. Springer (1997)","DOI":"10.1007\/978-0-387-35271-8_6"},{"issue":"11","key":"980_CR9","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y., et al.: Bounded model checking. Adv. Comput. 58(11), 117\u2013148 (2003)","journal-title":"Adv. Comput."},{"key":"980_CR10","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511814068","volume-title":"Random Graphs","author":"B Bollob\u00e1s","year":"2001","unstructured":"Bollob\u00e1s, B., B\u00e9la, B.: Random Graphs, vol. 73. Cambridge University Press, Cambridge (2001)"},{"key":"980_CR11","doi-asserted-by":"crossref","unstructured":"Bouabana-Tebibel, T.: UML 2 interaction overview diagram validation. In: 2009 Fourth International Conference on Dependability of Computer Systems, pp. 11\u201316. IEEE (2009)","DOI":"10.1109\/DepCoS-RELCOMEX.2009.47"},{"key":"980_CR12","volume-title":"Propositional Logic: Deduction and Algorithms","author":"HK B\u00fcning","year":"1999","unstructured":"B\u00fcning, H.K., Lettmann, T.: Propositional Logic: Deduction and Algorithms, vol. 48. Cambridge University Press, Cambridge (1999)"},{"key":"980_CR13","doi-asserted-by":"publisher","unstructured":"Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: an interpolating SMT solver. In: Donaldson, A.F., Parker, D. (eds.) Model Checking Software\u201419th International Workshop, SPIN 2012, Oxford, UK, July 23\u201324, 2012. Proceedings, Lecture Notes in Computer Science, vol. 7385, pp. 248\u2013254. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31759-0_19","DOI":"10.1007\/978-3-642-31759-0_19"},{"key":"980_CR14","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Mover, S., Tonetta, S.: Efficient scenario verification for hybrid automata. In: Proceedings of the 23rd International Conference on Computer Aided Verification, CAV\u201911, pp. 317\u2013332. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_25"},{"issue":"1","key":"980_CR15","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.: SMT-based scenario verification for hybrid systems. Form. Methods Syst. Des. 42(1), 46\u201366 (2013)","journal-title":"Form. Methods Syst. Des."},{"key":"980_CR16","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"issue":"9","key":"980_CR17","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/1995376.1995394","volume":"54","author":"L De Moura","year":"2011","unstructured":"De Moura, L., Bj\u00f8rner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69\u201377 (2011)","journal-title":"Commun. ACM"},{"key":"980_CR18","doi-asserted-by":"crossref","unstructured":"Dutertre, B.: Yices 2.2. In: International Conference on Computer Aided Verification, pp. 737\u2013744. Springer (2014)","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"980_CR19","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible sat-solver. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 502\u2013518. Springer (2003)","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"980_CR20","doi-asserted-by":"crossref","unstructured":"Fiadeiro, J.L.: Separating distribution from coordination and computation as architectural dimensions. In: International Conference on Formal Methods for Open Object-Based Distributed Systems, pp. 17\u201317. Springer (2006)","DOI":"10.1007\/11768869_2"},{"issue":"4","key":"980_CR21","doi-asserted-by":"publisher","first-page":"1141","DOI":"10.1214\/aoms\/1177706098","volume":"30","author":"EN Gilbert","year":"1959","unstructured":"Gilbert, E.N.: Random graphs. Ann. Math. Stat. 30(4), 1141\u20131144 (1959)","journal-title":"Ann. Math. Stat."},{"key":"980_CR22","doi-asserted-by":"crossref","unstructured":"Haugen, \u00d8.: Comparing UML 2.0 interactions and MSC-2000. In: International Workshop on System Analysis and Modeling, pp. 65\u201379. Springer (2004)","DOI":"10.1007\/978-3-540-31810-1_5"},{"key":"980_CR23","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/978-3-540-31810-1_5","volume-title":"System Analysis and Modeling","author":"\u00d8 Haugen","year":"2005","unstructured":"Haugen, \u00d8.: Comparing uml 2.0 interactions and msc-2000. In: Amyot, D., Williams, A.W. (eds.) System Analysis and Modeling, pp. 65\u201379. Springer, Berlin (2005)"},{"key":"980_CR24","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: Inan, M.K., et al. (eds.) Verification of Digital and Hybrid Systems, pp. 265\u2013292. Springer, Berlin (2000)","DOI":"10.1007\/978-3-642-59615-5_13"},{"key":"980_CR25","unstructured":"ITU-TS: ITU-TS Recommendation Z.120: Message Sequence Chart (MSC). ITU-TS, Geneva (2011)"},{"key":"980_CR26","doi-asserted-by":"crossref","unstructured":"Jackson, P., Sheridan, D.: Clause form conversions for boolean circuits. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 183\u2013198. Springer (2004)","DOI":"10.1007\/11527695_15"},{"key":"980_CR27","doi-asserted-by":"crossref","unstructured":"Kluge, O.: Modelling a railway crossing with message sequence charts and petri nets. In: Petri Net Technology for Communication-Based Systems, pp. 197\u2013218. Springer (2003)","DOI":"10.1007\/978-3-540-40022-6_10"},{"key":"980_CR28","doi-asserted-by":"crossref","unstructured":"Knapp, A., Wuttke, J.: Model checking of uml 2.0 interactions. In: K\u00fchne, T. (ed.) Models in Software Engineering, pp. 42\u201351. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-69489-2_6"},{"issue":"2","key":"980_CR29","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/s10601-018-9281-x","volume":"23","author":"P Laborie","year":"2018","unstructured":"Laborie, P., Rogerie, J., Shaw, P., Vil\u00edm, P.: Ibm ilog cp optimizer for scheduling. Constraints 23(2), 210\u2013250 (2018)","journal-title":"Constraints"},{"key":"980_CR30","volume-title":"Interpreting Message Sequence Charts","author":"PB Ladkin","year":"1992","unstructured":"Ladkin, P.B., Leue, S.: Interpreting Message Sequence Charts. IBM Thomas J, Watson Research Division, Albany (1992)"},{"issue":"2","key":"980_CR31","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1002\/stv.434","volume":"22","author":"X Li","year":"2012","unstructured":"Li, X., Pan, M., Bu, L., Wang, L., Zhao, J.: Timing analysis of scenario-based specifications using linear programming. Softw. Test. Verif. Reliab. 22(2), 121\u2013143 (2012). https:\/\/doi.org\/10.1002\/stv.434","journal-title":"Softw. Test. Verif. Reliab."},{"key":"980_CR32","first-page":"205","volume":"3","author":"A Louati","year":"2013","unstructured":"Louati, A., Jerad, C., Barkaoui, K., Saint-Martin, P.: Formalization and verification of hierarchical use of interaction overview diagrams using timing diagrams. Int. J. Soft Comput. Softw. Eng. 3, 205\u2013211 (2013)","journal-title":"Int. J. Soft Comput. Softw. Eng."},{"key":"980_CR33","volume-title":"Automated Theorem Proving: A Logical Basis","author":"DW Loveland","year":"2016","unstructured":"Loveland, D.W.: Automated Theorem Proving: A Logical Basis. Elsevier, Amsterdam (2016)"},{"key":"980_CR34","doi-asserted-by":"publisher","unstructured":"Nguyen, M.C., Jee, E., Choi, J., Bae, D.H.: Automatic construction of timing diagrams from UML\/MARTE models for real-time embedded software. In: Inan, M.K., et al. (eds.) Proceedings of the 29th Annual ACM Symposium on Applied Computing, SAC \u201914, pp. 1140\u20131145. ACM (2014). https:\/\/doi.org\/10.1145\/2554850.2555011","DOI":"10.1145\/2554850.2555011"},{"issue":"6","key":"980_CR35","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving sat and sat modulo theories: from an abstract Davis\u2013Putnam\u2013Logemann\u2013Loveland procedure to dpll (t). J. ACM: JACM 53(6), 937\u2013977 (2006)","journal-title":"J. ACM: JACM"},{"key":"980_CR36","doi-asserted-by":"crossref","unstructured":"Nobari, S., Lu, X., Karras, P., Bressan, S.: Fast random graph generation. In: Proceedings of the 14th International Conference on Extending Database Technology, pp. 331\u2013342 (2011)","DOI":"10.1145\/1951365.1951406"},{"issue":"3","key":"980_CR37","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/s10601-008-9064-x","volume":"14","author":"O Ohrimenko","year":"2009","unstructured":"Ohrimenko, O., Stuckey, P.J., Codish, M.: Propagation via lazy clause generation. Constraints 14(3), 357\u2013391 (2009)","journal-title":"Constraints"},{"key":"980_CR38","doi-asserted-by":"publisher","first-page":"689","DOI":"10.1007\/978-3-642-02658-4_56","volume-title":"Computer Aided Verification","author":"M Pan","year":"2009","unstructured":"Pan, M., Bu, L., Li, X.: Tass: timing analyzer of scenario-based specifications. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification, pp. 689\u2013695. Springer, Berlin (2009)"},{"issue":"6","key":"980_CR39","doi-asserted-by":"publisher","first-page":"639","DOI":"10.1007\/s10009-012-0239-9","volume":"14","author":"M Pan","year":"2012","unstructured":"Pan, M., Li, X.: Timing analysis of msc specifications with asynchronous concatenation. Int. J. Softw. Tools Technol. Transf. 14(6), 639\u2013651 (2012). https:\/\/doi.org\/10.1007\/s10009-012-0239-9","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"1","key":"980_CR40","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/BF02284626","volume":"17","author":"M Parker","year":"1996","unstructured":"Parker, M., Ryan, J.: Finding the minimum weight IIS cover of an infeasible system of linear inequalities. Ann. Math. Artif. Intell. 17(1), 107\u2013126 (1996)","journal-title":"Ann. Math. Artif. Intell."},{"key":"980_CR41","doi-asserted-by":"crossref","unstructured":"Pearce, R., Gokhale, M., Amato, N.M.: Multithreaded asynchronous graph traversal for in-memory and semi-external memory. In: SC\u201910: Proceedings of the 2010 ACM\/IEEE International Conference for High Performance Computing, Networking, Storage and Analysis, pp. 1\u201311. IEEE (2010)","DOI":"10.1109\/SC.2010.34"},{"key":"980_CR42","volume-title":"Software Reliability Methods","author":"DA Peled","year":"2013","unstructured":"Peled, D.A.: Software Reliability Methods. Springer, Berlin (2013)"},{"key":"980_CR43","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4899-7687-1","volume-title":"Encyclopedia of Machine Learning and Data Mining","author":"C Sammut","year":"2017","unstructured":"Sammut, C., Webb, G.I.: Encyclopedia of Machine Learning and Data Mining. Springer Publishing Company, Incorporated (2017)"},{"issue":"3\u20134","key":"980_CR44","first-page":"141","volume":"3","author":"R Sebastiani","year":"2007","unstructured":"Sebastiani, R.: Lazy satisfiability modulo theories. J. Satisf. Boolean Model. Comput. 3(3\u20134), 141\u2013224 (2007)","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"980_CR45","doi-asserted-by":"crossref","unstructured":"Seemann, J., von Gudenberg, J.W.: Extension of UML sequence diagrams for real-time systems. In: International Conference on the Unified Modeling Language, pp. 240\u2013252. Springer (1998)","DOI":"10.1007\/978-3-540-48480-6_19"},{"key":"980_CR46","unstructured":"Specification, O.A.: Omg unified modeling language (omg uml), superstructure, v2. 1.2, vol. 70. Object Management Group (2007)"},{"key":"980_CR47","unstructured":"Sridhar, S., Wright, S., Re, C., Liu, J., Bittorf, V., Zhang, C.: An approximate, efficient lp solver for lp rounding. In: Burges, C.J.C., Bottou, L., Welling, M., Ghahramani, Z., Weinberger, K.Q. (eds.) Advances in Neural Information Processing Systems, pp. 2895\u20132903 (2013)"},{"key":"980_CR48","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1016\/j.protcy.2012.10.017","volume":"6","author":"RK Swain","year":"2012","unstructured":"Swain, R.K., Panthi, V., Behera, P.K.: Test case design using slicing of UML interaction diagram. Procedia Technol. 6, 136\u2013144 (2012)","journal-title":"Procedia Technol."},{"issue":"1","key":"980_CR49","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1016\/j.ejor.2010.04.019","volume":"207","author":"MW Tanner","year":"2010","unstructured":"Tanner, M.W., Ntaimo, L.: Iis branch-and-cut for joint chance-constrained programs with random technology matrices. Eur. J. Oper. Res. 207(1), 290\u2013296 (2010)","journal-title":"Eur. J. Oper. Res."},{"key":"980_CR50","unstructured":"Tassey, G.: The Economic Impacts of Inadequate Infrastructure for Software Testing. National Institute of Standards and Technology, RTI Project, vol. 7007, no. 011, pp. 429\u2013489 (2002)"},{"key":"980_CR51","volume-title":"Boolean Algebra and Its Applications","author":"JE Whitesitt","year":"2012","unstructured":"Whitesitt, J.E.: Boolean Algebra and Its Applications. Courier Corporation, Chelmsford (2012)"},{"issue":"1","key":"980_CR52","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/s10703-014-0210-3","volume":"45","author":"D Xie","year":"2014","unstructured":"Xie, D., Bu, L., Zhao, J., Li, X.: SAT\u2013lP\u2013IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata. Form. Methods Syst. Des. 45(1), 42\u201362 (2014)","journal-title":"Form. Methods Syst. Des."}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-022-00980-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-022-00980-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-022-00980-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,18]],"date-time":"2024-09-18T06:32:26Z","timestamp":1726641146000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-022-00980-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,2,10]]},"references-count":52,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2022,8]]}},"alternative-id":["980"],"URL":"https:\/\/doi.org\/10.1007\/s10270-022-00980-8","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"type":"print","value":"1619-1366"},{"type":"electronic","value":"1619-1374"}],"subject":[],"published":{"date-parts":[[2022,2,10]]},"assertion":[{"value":"11 April 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 January 2022","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 January 2022","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 February 2022","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}