{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T03:49:04Z","timestamp":1760586544158},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"2-3","license":[{"start":{"date-parts":[[2010,11,26]],"date-time":"2010-11-26T00:00:00Z","timestamp":1290729600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2010,12]]},"DOI":"10.1007\/s10703-010-0103-z","type":"journal-article","created":{"date-parts":[[2010,11,25]],"date-time":"2010-11-25T05:45:18Z","timestamp":1290663918000},"page":"200-264","source":"Crossref","is-referenced-by-count":14,"title":["Scenario-based verification of real-time systems using Uppaal"],"prefix":"10.1007","volume":"37","author":[{"given":"Shuhao","family":"Li","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sandie","family":"Balaguer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexandre","family":"David","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kim G.","family":"Larsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Brian","family":"Nielsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Saulius","family":"Pusinskas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,11,26]]},"reference":[{"key":"103_CR1","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/BFb0054177","volume-title":"Proc 4th international conference on tools and algorithms for construction and analysis of systems (TACAS\u201998)","author":"L Aceto","year":"1998","unstructured":"Aceto L, Burgue\u00f1o A, Larsen KG (1998) Model checking via reachability testing for timed automata. In: Proc 4th international conference on tools and algorithms for construction and analysis of systems (TACAS\u201998), pp\u00a0263\u2013280"},{"issue":"2","key":"103_CR2","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur R, Dill DL (1994) A theory of timed automata. Theor Comput Sci 126(2):183\u2013235","journal-title":"Theor Comput Sci"},{"issue":"1\u20132","key":"103_CR3","doi-asserted-by":"crossref","first-page":"86","DOI":"10.1007\/s100090050007","volume":"1","author":"R Alur","year":"1997","unstructured":"Alur R, Henzinger TA (1997) Real-time system = discrete system + clock variables. Softw Tools Technol Transf (STTT) 1(1\u20132):86\u2013109","journal-title":"Softw Tools Technol Transf (STTT)"},{"issue":"2","key":"103_CR4","first-page":"70","volume":"17","author":"R Alur","year":"1996","unstructured":"Alur R, Holzmann GJ, Peled D (1996) An analyzer for message sequence charts. Softw, Concepts Tools 17(2):70\u201377","journal-title":"Softw, Concepts Tools"},{"key":"103_CR5","unstructured":"Balaguer S (2009) Specification of properties using live sequence charts\u2014theory and implementation. Master\u2019s thesis, \u00c9cole Centrale de Nantes, Nantes, France, September 2009"},{"key":"103_CR6","unstructured":"Balaguer S, David A, Larsen KG, Li S Live sequence chart specification and verification in Uppaal (under submission)"},{"key":"103_CR7","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"SFM","author":"G Behrmann","year":"2004","unstructured":"Behrmann G, David A, Larsen KG (2004) A tutorial on Uppaal. In: Bernardo M, Corradini F (eds) SFM. Lecture notes in computer science, vol\u00a03185. Springer, Berlin, pp\u00a0200\u2013236"},{"key":"103_CR8","unstructured":"Bontemps Y (2005) Relating inter-agent and intra-agent specifications\u2014the case of live sequence charts. PhD thesis, University of Namur, Namur, Belgium"},{"issue":"2","key":"103_CR9","doi-asserted-by":"crossref","first-page":"252","DOI":"10.1016\/j.jal.2005.12.013","volume":"5","author":"Y Bontemps","year":"2007","unstructured":"Bontemps Y, Schobbens P-Y (2007) The computational complexity of scenario-based agent verification and design. J Appl Log 5(2):252\u2013276","journal-title":"J Appl Log"},{"issue":"4","key":"103_CR10","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/s10009-004-0145-x","volume":"7","author":"A Bunker","year":"2005","unstructured":"Bunker A, Gopalakrishnan G, Slind K (2005) Live sequence charts applied to hardware requirements specification and verification. Softw Tools Technol Transf (STTT) 7(4):341\u2013350","journal-title":"Softw Tools Technol Transf (STTT)"},{"issue":"2","key":"103_CR11","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1007\/s10270-007-0069-5","volume":"7","author":"P Combes","year":"2008","unstructured":"Combes P, Harel D, Kugler H (2008) Modeling and verification of a telecommunication application using live sequence charts and the play-engine tool. Softw Syst Model 7(2):157\u2013175","journal-title":"Softw Syst Model"},{"issue":"1","key":"103_CR12","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1023\/A:1011227529550","volume":"19","author":"W Damm","year":"2001","unstructured":"Damm W, Harel D (2001) LSCs: Breathing life into message sequence charts. Form Methods Syst Des 19(1):45\u201380. Preliminary version in: P\u00a0Ciancarini, A\u00a0Fantechi, R\u00a0Gorrieri (eds) Proc 3rd IFIP int conf on formal methods for open object-based distributed systems\/(FMOODS\u201999). Kluwer Academic (1999), pp\u00a0293\u2013312","journal-title":"Form Methods Syst Des"},{"issue":"2","key":"103_CR13","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1023\/A:1011279932612","volume":"19","author":"W Damm","year":"2001","unstructured":"Damm W, Klose J (2001) Verification of a radio-based signaling system using the statemate verification environment. Form Methods Syst Des 19(2):121\u2013141","journal-title":"Form Methods Syst Des"},{"key":"103_CR14","first-page":"225","volume-title":"Program analysis and compilation, theory and practice, essays dedicated to Reinhard Wilhelm on the occasion of his 60th birthday","author":"W Damm","year":"2006","unstructured":"Damm W, Toben T, Westphal B (2006) On the expressive power of live sequence charts. In: Program analysis and compilation, theory and practice, essays dedicated to Reinhard Wilhelm on the occasion of his 60th birthday, pp\u00a0225\u2013246"},{"key":"103_CR15","doi-asserted-by":"crossref","unstructured":"Firley T, Huhn M, Diethers K, Gehrke T, Goltz U (1999) Timed sequence diagrams and tool-based analysis\u2014a case study. In: Proc 2nd international conference on the unified modeling language (UML\u201999), pp\u00a0645\u2013660","DOI":"10.1007\/3-540-46852-8_45"},{"key":"103_CR16","doi-asserted-by":"crossref","unstructured":"Genest B, Minea M, Muscholl A, Peled D (2004) Specifying and verifying partial order properties using template MSCs. In: Proc 7th international conference on foundations of software science and computation structures (FoSSaCS\u201904), pp\u00a0195\u2013210","DOI":"10.1007\/978-3-540-24727-2_15"},{"issue":"1","key":"103_CR17","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1142\/S0129054102000935","volume":"13","author":"D Harel","year":"2002","unstructured":"Harel D, Kugler H (2002) Synthesizing state-based object systems from LSC specifications. Int J Found Comput Sci 13(1):5\u201351","journal-title":"Int J Found Comput Sci"},{"key":"103_CR18","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-19029-2","volume-title":"Come, let\u2019s play: scenario-based programming using LSCs and the play-engine","author":"D Harel","year":"2003","unstructured":"Harel D, Marelly R (2003) Come, let\u2019s play: scenario-based programming using LSCs and the play-engine. Springer, New York"},{"key":"103_CR19","doi-asserted-by":"crossref","unstructured":"Harel D, Kugler H, Marelly R, Pnueli A (2002) Smart play-out of behavioral requirements. In: Proc 4th international conference on formal methods in computer-aided design (FMCAD\u201902), pp\u00a0378\u2013398","DOI":"10.1007\/3-540-36126-X_23"},{"key":"103_CR20","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1007\/3-540-48778-6_17","volume-title":"Proc 5th international AMAST workshop on formal methods for real-time and probabilistic systems (ARTS\u201999)","author":"K Havelund","year":"1999","unstructured":"Havelund K, Larsen KG, Skou A (1999) Formal verification of a power controller using the real-time model checker Uppaal. In: Proc 5th international AMAST workshop on formal methods for real-time and probabilistic systems (ARTS\u201999), pp\u00a0277\u2013298"},{"key":"103_CR21","unstructured":"ITU-T (1999) Message Sequence Charts\u2014MSC-2000, ITU-T recommendation z.120"},{"key":"103_CR22","unstructured":"Jaghoori MM, Chothia T (2010) Timed automata semantics for analyzing Creol. arXiv:1007.5095"},{"issue":"5","key":"103_CR23","doi-asserted-by":"crossref","first-page":"402","DOI":"10.1016\/j.jlap.2009.02.009","volume":"78","author":"MM Jaghoori","year":"2009","unstructured":"Jaghoori MM, de Boer FS, Chothia T, Sirjani M (2009) Schedulability of asynchronous real-time concurrent objects. J Log Algebr Program 78(5):402\u2013416","journal-title":"J Log Algebr Program"},{"key":"103_CR24","unstructured":"Klose J (2003) Live sequence charts: a graphical formalism for the specification of communication behavior. PhD thesis, Carl von Ossietzky Universit\u00e4t Oldenburg"},{"key":"103_CR25","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1007\/3-540-45319-9_35","volume-title":"Proc 7th international conference on tools and algorithms for the construction and analysis of systems (TACAS\u201901)","author":"J Klose","year":"2001","unstructured":"Klose J, Wittke H (2001) An automata based interpretation of live sequence charts. In: Proc 7th international conference on tools and algorithms for the construction and analysis of systems (TACAS\u201901), pp\u00a0512\u2013527"},{"key":"103_CR26","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/11817963_22","volume-title":"Proc 18th international conference on computer aided verification (CAV\u201906)","author":"J Klose","year":"2006","unstructured":"Klose J, Toben T, Westphal B, Wittke H (2006) Check it out: on the efficient formal verification of live sequence charts. In: Proc 18th international conference on computer aided verification (CAV\u201906), pp\u00a0219\u2013233"},{"key":"103_CR27","doi-asserted-by":"crossref","first-page":"445","DOI":"10.1007\/978-3-540-31980-1_29","volume-title":"Proc 11th international conference on tools and algorithms for the construction and analysis of systems (TACAS\u201905)","author":"H Kugler","year":"2005","unstructured":"Kugler H, Harel D, Pnueli A, Lu Y, Bontemps Y (2005) Temporal logic for scenario-based specifications. In: Proc 11th international conference on tools and algorithms for the construction and analysis of systems (TACAS\u201905), pp\u00a0445\u2013460"},{"key":"103_CR28","unstructured":"Lahtinen J (2008) Model checking timed safety instrumented systems. Master\u2019s thesis, Helsinki University of Technology, Espoo, Finland, June 2008. Research Report TKK-ICS-R3"},{"key":"103_CR29","first-page":"676","volume-title":"Proc 16th int\u2019l symposium on formal methods (FM\u201909)","author":"KG Larsen","year":"2009","unstructured":"Larsen KG, Li S, Nielsen B, Pusinskas S (2009) Verifying real-time systems against scenario-based requirements. In: Proc 16th int\u2019l symposium on formal methods (FM\u201909), pp\u00a0676\u2013691"},{"key":"103_CR30","first-page":"447","volume-title":"Proc 13th conference on design, automation, and test in Europe (DATE\u201910)","author":"KG Larsen","year":"2010","unstructured":"Larsen KG, Li S, Nielsen B, Pusinskas S (2010) Scenario-based analysis and synthesis of real-time systems using Uppaal. In: Proc 13th conference on design, automation, and test in Europe (DATE\u201910), pp\u00a0447\u2013452"},{"key":"103_CR31","doi-asserted-by":"crossref","unstructured":"Larsen KG, Li S, Nielsen B, Pusinskas S (2010) Scenario-based verification of real-time systems using Uppaal. Technical report, Aalborg University Department of Computer Science, Aalborg, Denmark. Available http:\/\/www.cs.aau.dk\/~li\/papers\/ScenarioVeriUppaalTR.pdf","DOI":"10.1109\/DATE.2010.5457164"},{"key":"103_CR32","first-page":"317","volume-title":"Proc 4th int conference on the unified modeling language (UML\u201901)","author":"M Lettrari","year":"2001","unstructured":"Lettrari M, Klose J (2001) Scenario-based monitoring and testing of real-time UML models. In: Proc 4th int conference on the unified modeling language (UML\u201901), pp\u00a0317\u2013328"},{"issue":"2\u20133","key":"103_CR33","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1016\/0167-6423(95)00017-8","volume":"25","author":"KVS Prasad","year":"1995","unstructured":"Prasad KVS (1995) A calculus of broadcasting systems. Sci Comput Program 25(2\u20133):285\u2013327","journal-title":"Sci Comput Program"},{"key":"103_CR34","unstructured":"Pusinskas S (2010) Capturing and testing behavioral requirements by means of live sequence charts. PhD thesis, Aalborg University, Aalborg, Denmark"},{"key":"103_CR35","unstructured":"Rye-Andersen JG, Jensen M, Goettler R, Jakobsen M (2004) PEEL: property extraction engine for LSCs. Master\u2019s thesis, Aalborg University, Aalborg, Denmark"},{"key":"103_CR36","first-page":"174","volume-title":"Proc 2nd international conference on software engineering and formal methods (SEFM\u201904)","author":"I Schinz","year":"2004","unstructured":"Schinz I, Toben T, Mrugalla C, Westphal B (2004) The Rhapsody UML verification environment. In: Proc 2nd international conference on software engineering and formal methods (SEFM\u201904), pp\u00a0174\u2013183"},{"key":"103_CR37","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1145\/587051.587077","volume-title":"Proc 10th ACM SIGSOFT symposium on foundations of software engineering (SIGSOFT FSE\u201902)","author":"B Sengupta","year":"2002","unstructured":"Sengupta B, Cleaveland R (2002) Triggered message sequence charts. In: Proc 10th ACM SIGSOFT symposium on foundations of software engineering (SIGSOFT FSE\u201902), pp\u00a0167\u2013176"},{"key":"103_CR38","doi-asserted-by":"crossref","first-page":"529","DOI":"10.1109\/ICECCS.2005.60","volume-title":"Proc 10th international conference on engineering of complex computer systems (ICECCS\u201905)","author":"J Sun","year":"2005","unstructured":"Sun J, Dong JS (2005) Model checking live sequence charts. In: Proc 10th international conference on engineering of complex computer systems (ICECCS\u201905), pp\u00a0529\u2013538"},{"key":"103_CR39","unstructured":"The Uppaal Team (2009) Uppaal 4.0.8 online help document. Available at http:\/\/www.uppaal.com"},{"key":"103_CR40","doi-asserted-by":"crossref","first-page":"178","DOI":"10.1007\/978-3-540-24836-1_13","volume-title":"Proc 6th international on practical aspects of declarative languages (PADL\u201904)","author":"T Wang","year":"2004","unstructured":"Wang T, Roychoudhury A, Yap RHC, Choudhary SC (2004) Symbolic execution of behavioral requirements. In: Proc 6th international on practical aspects of declarative languages (PADL\u201904), pp\u00a0178\u2013192"},{"key":"103_CR41","first-page":"243","volume-title":"Proc 7th IFIPWG6.1 international conference on formal description techniques (FORTE\u201995)","author":"W Yi","year":"1994","unstructured":"Yi W, Pettersson P, Daniels M (1994) Automatic verification of real-time communicating systems by constraint-solving. In: Proc 7th IFIPWG6.1 international conference on formal description techniques (FORTE\u201995), pp\u00a0243\u2013258"},{"issue":"1\u20132","key":"103_CR42","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/s100090050009","volume":"1","author":"S Yovine","year":"1997","unstructured":"Yovine S (1997) Kronos: A verification tool for real-time systems. Softw Tools Technol Transf (STTT) 1(1\u20132):123\u2013133","journal-title":"Softw Tools Technol Transf (STTT)"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-010-0103-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-010-0103-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-010-0103-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,6]],"date-time":"2019-06-06T10:51:02Z","timestamp":1559818262000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-010-0103-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,11,26]]},"references-count":42,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[2010,12]]}},"alternative-id":["103"],"URL":"https:\/\/doi.org\/10.1007\/s10703-010-0103-z","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,11,26]]}}}